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.