Robert Atkey
To implement the translation of embedded language types to Haskell types in Haskell we use type families.
This type-to-type translation is indeed the crux of the trickiness. By the way, Section 4.3 of our (JFP) paper describes how to follow such a translation without type families. If I were to avoid type families in Haskell, I would make Symantics into a multiparameter type class class HOAS repr arrow int where lam :: (repr a -> repr b) -> repr (arrow a b) app :: repr (arrow a b) -> repr a -> repr b fix :: (repr a -> repr a) -> repr a let_ :: repr a -> (repr a -> repr b) -> repr b int :: int -> repr int add :: repr int -> repr int -> repr int sub :: repr int -> repr int -> repr int mul :: repr int -> repr int -> repr int
The underlying problem with the implementation of 'lam' is that you have to pick an evaluation order for the side effects you want in the semantics of your embedded language. The two obvious options are call-by-name and call-by-value.
(Section 5 of our (JFP) paper addresses both CBN and CBV.) -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig Here's a souvenir of it. He made me write this down so I'd remember to get this book and read it. Transcendent Speculations on Apparent Design in the Fate of the Individual, that's a mouthful isn't it. I wrote this down at gun-point. - Gaddis