Existential type as return value

Question

Consider the following data structure, representing a tree with levels which increase but are not necessarily consecutive:

data MyTree (n :: T) where
    MyLeaf :: MyTree n
    MyNode :: Plus n m z => [MyTree ('Succ z)] -> MyTree n

where T represents the Peano numbers at the type level, defined as

class Plus (n :: T) (m :: T) (r :: T) | r n -> m
instance Plus 'Zero m m
instance Plus n m r => Plus ('Succ n) m ('Succ r)

It is pretty easy to construct trees like

myTreeOne :: MyTree ('Succ 'Zero)
myTreeOne = MyNode ([ MyLeaf ] :: [MyTree ('Succ ('Succ 'Zero))])

myTree :: MyTree 'Zero
myTree = MyNode [ MyLeaf, myTreeOne ]

or

myLeafTwo :: MyTree ('Succ ('Succ 'Zero))
myLeafTwo = MyLeaf

myOtherTree :: MyTree 'Zero
myOtherTree = MyNode [ myLeafTwo ]

Now I would like to define the following function:

myTreeComponents MyLeaf              = []
myTreeComponents (MyNode components) = components

which just extracts the list of immediate subnodes of the tree, but I'm not able to write it's correct type.

This is the error I get

    • Couldn't match expected type ‘p’                                                                                │
                  with actual type ‘[MyTree ('Succ z)]’                                                               │
        because type variable ‘z’ would escape its scope                                                              │
      This (rigid, skolem) type variable is bound by                                                                  │
        a pattern with constructor:                                                                                   │
          MyNode :: forall (n :: T) (m :: T) (z :: T).                                                                │
                    Plus n m z =>                                                                                     │
                    [MyTree ('Succ z)] -> MyTree n,                                                                   │
        in an equation for ‘myTreeComponents’                                                                         │
        at src/Model.hs:159:19-35                                                                                     │
    • In the expression: components                                                                                   │
      In an equation for ‘myTreeComponents’:                                                                          │
          myTreeComponents (MyNode components) = components                                                           │
    • Relevant bindings include                                                                                       │
        components :: [MyTree ('Succ z)] (bound at src/Model.hs:159:26)                                               │
        myTreeComponents :: MyTree n -> p (bound at src/Model.hs:158:1)                                               │
    |                                                                                                                 │
159 | myTreeComponents (MyNode components) = components                                                               │
    |                                        ^^^^^^^^^^

With dependent type languages it should be something like

exists m. Plus n m z => MyTree n -> [ MyTree ('Succ z) ]

Is it possible to write such a type in Haskell? Otherwise how should I write my function?

Answer 1

This is an adaptation of your code with a Proxy added, so to "remember" the number m.

{-# LANGUAGE GADTs, KindSignatures, DataKinds, TypeFamilies, 
    MultiParamTypeClasses, FunctionalDependencies,
    FlexibleInstances, UndecidableInstances #-}
{-# OPTIONS -Wall #-}

import Data.Proxy

data T = Zero | Succ T

class Plus (n :: T) (m :: T) (z :: T) | n m -> z where

instance Plus n 'Zero n
instance Plus n m z => Plus n ('Succ m) ('Succ z)

data MyTree (n :: T) where
    MyLeaf :: MyTree n
    MyNode :: Plus n m z => ! (Proxy m) -> [MyTree ('Succ z)] -> MyTree n

myTreeOne :: MyTree ('Succ 'Zero)
myTreeOne = MyNode (Proxy :: Proxy 'Zero) ([ MyLeaf ] :: [MyTree ('Succ ('Succ 'Zero))])

myTree :: MyTree 'Zero
myTree = MyNode (Proxy :: Proxy 'Zero) [ MyLeaf, myTreeOne ]

myLeafTwo :: MyTree ('Succ ('Succ 'Zero))
myLeafTwo = MyLeaf

myOtherTree :: MyTree 'Zero
myOtherTree = MyNode (Proxy :: Proxy ('Succ 'Zero)) [ myLeafTwo ]

To be able to write the final function myTreeComponents, we need a custom existential type:

data Nodes (n :: T) where
    Nodes :: Plus n m z => ! (Proxy m) -> [MyTree ('Succ z)] -> Nodes n

This is essentially MyTree with only the second constructor. Finally, pattern matching now suffices.

myTreeComponents :: MyTree n -> Nodes n
myTreeComponents MyLeaf                = Nodes (Proxy :: Proxy 'Zero) []
myTreeComponents (MyNode p components) = Nodes p components

Answer 2

You can usually use CPS to encode existentials.

exists a. f a

can be represented as

(forall a. f a -> r) -> r

However, I don't think your

exists m. Plus n m z => MyTree n -> [ MyTree ('Succ z) ]

is the type you want. First, the exists is in the wrong place -- there does not exist a single global type m, but rather for each MyTree n there is a possibly distinct such m.

MyTree n -> exists m. Plus n m z => [ MyTree ('Succ z) ]

Here the caller gets to choose z, and, given evidence that n + m = z, can extract the list of children. That is consistent, but such evidence might be hard to come by. I think you actually want a double existential:

MyTree n -> exists m z. Plus n m z & [ MyTree ('Succ z) ]

and I'm using & as the dual to =>, a type which comes packed with a dictionary rather than requiring it as an argument.

type a & b = (Dict a, b)

So this says, for any tree at level n, there is some z >= n (witnessed by addition with m) such that there is a list of children at level 'Succ z. Yes, I think that's right. So now let's CPS encode it to:

MyTree n -> (forall m z. Plus n m z => [ MyTree ('Succ z) ] -> r) -> r

Answer 3

I like chi's fix, because using Proxys to store types is a nice trick to have under your belt. In his answer, the Proxy is used to disambiguate what m to use in the Plus n m z constraint when calling the Nodes constructor. (There's a Plus n m z constraint in scope at that point, but without the proxy, there's no way to tell the compiler to choose it.)

Besides Proxy, there's another way to fix ambiguous types: eliminate the ambiguous type. In this case, that's m. So, instead of a Plus n m z class, we'll have a LE n z class that has all the same instances but doesn't mention m anywhere. So:

{-# LANGUAGE GADTs, KindSignatures, DataKinds, TypeFamilies, 
    MultiParamTypeClasses, FunctionalDependencies,
    FlexibleInstances, UndecidableInstances, ScopedTypeVariables #-}
{-# OPTIONS -Wall #-}

data T = Zero | Succ T

class LE (n :: T) (z :: T)
instance LE 'Zero n
instance LE n z => LE ('Succ n) ('Succ z)

There's one wrinkle. In chi's answer, he uses a slightly modified definition of Plus that gives a Plus n 'Zero n instance for free, but in your formulation that's not available, and consequently LE n n does not come for free. So we'll have to decorate our leaves a little bit.

data MyTree (n :: T) where
    MyLeaf :: LE n n => MyTree n
    MyNode :: LE n z => [MyTree ('Succ z)] -> MyTree n

All the concrete trees are just as they were before (no extra Proxy needed).

myTreeOne :: MyTree ('Succ 'Zero)
myTreeOne = MyNode [ MyLeaf :: MyTree ('Succ ('Succ 'Zero)) ]

myTree :: MyTree 'Zero
myTree = MyNode [ MyLeaf, myTreeOne ]

myLeafTwo :: MyTree ('Succ ('Succ 'Zero))
myLeafTwo = MyLeaf

myOtherTree :: MyTree 'Zero
myOtherTree = MyNode [ myLeafTwo ]

And the only difference in myTreeComponents compared to chi's answer (besides erasing the Proxy) is that we need to bring a type variable into scope for use in the body.

data Nodes (n :: T) where
    Nodes :: LE n z => [MyTree ('Succ z)] -> Nodes n

myTreeComponents :: forall n. MyTree n -> Nodes n
myTreeComponents MyLeaf              = Nodes ([] :: [MyTree ('Succ n)])
myTreeComponents (MyNode components) = Nodes components

Answer 4

something like (I don't know if such type allowed, and cannot check it now)

MyNode n -> forall z .Plus n m z => [MyTree ('Succ z)]

z type is not exposed so it is allowed to be any. If z's type were exposed by myTreeComponents, the caller could specify a concrete type for it, which it must not be able to do