Thank you for your rich responses. Indeed I think I miss some thinks in my DSL, that would make things easier to deal with lists and first class functions. I don't really know what for now. Perhaps a List Constructor? Or a constructor on functions like yours Ryan? EAp :: Exp ref (a -> b) -> Exp ref a -> Exp ref b It's from which DSL? It is accessible on the net? Chris suggested me that I can only define the Foldr constructor and deduce Map from it. But maybe I have to add a List constructor for that. But in the suggestions from Ryan and Brandon I don't understand why I should add an extra type parameter and what it is! Steffen: Wow nice. I'll integrate that ;) I'm also looking at the Atom's DSL to get inspiration. Something I don't understand in it is that it has two languages, on typed: data E a where VRef :: V a -> E a Const :: a -> E a Cast :: (NumE a, NumE b) => E a -> E b Add :: NumE a => E a -> E a -> E a etc. And, along with it, an untyped counterpart: -- | An untyped term. data UE = UVRef UV | UConst Const | UCast Type UE | UAdd UE UE etc. What that for? What's the use of having beautiful GADT if you have to maintain an untyped ADT aside?? Corentin