[Haskell-cafe] Trouble understanding records and existential types

[Brian Hulley]

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) }
>>
>> 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.getNode) rest
>> getLeaves x@(Leaf {}) = [x]

Thanks Chris - that's really neat!
I see it's the explicit wrapping and unwrapping of the existential that 
solves the typechecking problem, and the use of newtype ensures there's no 
run-time penalty for this.
Also the wrapping of the existential allowed higher order functions to be 
used making the code much neater.
Regarding the question of why in the original example the typechecker was 
trying to match (forall b.ANode b) against (ANode a) and not (ANode IsLeaf), 
I think the answer is probably that the typechecker first finds the MGU of 
the types occupying the same position in all the left hand sides first, then 
it tries to match this against the declared type at that position, whereas 
for the original example to have typechecked it would have to treat each 
equation separately. Anyway it's now an irrelevant point given the clarity 
of your solution which compiles fine,

Best regards, Brian.
-- 
http://www.metamilk.com