- A+

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 `