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.