# Existential type as return value

• A+
Category：Languages

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?

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 ``