[Haskell] Re: A question about fundeps <-> GADT interaction

[oleg at pobox.com]

Tomasz Zielonka wrote:
> I tried to implement another function:
>
>   mapChildren :: (forall a. Term f a -> Term f a) -> Term f b -> Term f b
>   mapChildren fun t@(Lit x) = t
>   mapChildren fun (IsZero t) = IsZero (fun t)
>   mapChildren fun (Succ t) = Succ (fun t)
>   mapChildren fun (If c t e) = If (fun c) (fun t) (fun e)
>
> It is supposed to be similar to gmapT from Data.Generics - apply 'fun'
> to every immediate Expr child of the node. Unfortunately, I don't know
> how to make it compile. I tried a couple of different type signatures.


the following works

> data MT f = MT (forall a. Term f a -> Term f a)
>
> mapChildren _ t@(Lit x) = t
> mapChildren (MT fun) (IsZero t) = IsZero (fun t)
> mapChildren (MT fun) (Succ t) = Succ (fun t)
> mapChildren (MT fun) (If c t e) = If (fun c) (fun t) (fun e)
>
> testm = showt $ mapChildren (MT id) ex1'
>
> showt :: Term f a -> String
> showt (Lit x) = show x
> showt (Succ x) = "(S " ++ (showt x) ++ ")"
> showt (IsZero x) = "(Z? " ++ (showt x) ++ ")"
> showt (If t c a) = unwords ["(If",showt t, showt c, showt a, ")"]

but it is useless. But one can hardly write any transformer of the type
|Term f a -> Term f a| aside from 'id' or 'undefined'. This is because
any attempt to pattern-match on Lit x, for example, will bring up a
constraint F f Int a, which must somehow be resolved or
propagated. Also, the current incarnation of GADT is apt to lift the
constraints, so one can write a seemingly well-typed term which cannot
be used because its constraints are contradictory.

It seems a different approach is more fruitful, described in the next
message. It attempts to be more idiomatic.