[Haskell-cafe] Trouble understanding records and existential types

[Roberto Zunino]

Brian Hulley wrote:
> Chris Kuklewicz wrote:
>> This is how I would write getLeaves, based on your GADT:
>>
>>> data IsLeaf
>>> data IsBranch
>>>
>>> newtype Node = Node { getNode :: (forall c. ANode c) }
[snip]
> Thanks Chris - that's really neat!
> I see it's the explicit wrapping and unwrapping of the existential that 
> solves the typechecking problem,

Actually, Node is universally quantified. This makes it not inhabitated 
given the ANode GADT.  So, you can consume a Node, but you can not 
produce a non-bottom one.

Existential quantification version:

data IsLeaf
data IsBranch

data Node = forall c . Node ( ANode c )

data ANode :: * -> * where
     Branch :: String -> String -> (ANode a,ANode b) -> [Node] -> ANode 
IsBranch
     Leaf :: String -> String -> ANode IsLeaf

getLeaves :: ANode a -> [ANode IsLeaf]
getLeaves (Branch _ _ (l1,l2) rest) = getLeaves l1 ++ getLeaves l2 ++
                                       concatMap getLeaves' rest
getLeaves x@(Leaf {}) = [x]

getLeaves' :: Node -> [ANode IsLeaf]
getLeaves' (Node x) = getLeaves x


Regards,
Zun.