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 

Comment

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen: