Re: [Haskell-cafe] Re: Finally tagless - stuck with implementation of?"lam"

On Mon, 2009-10-05 at 22:06 -0400, Chung-chieh Shan wrote:

Robert Atkey wrote in article <1254778973.3675.42.camel@bismuth> in gmane.comp.lang.haskell.cafe:

...

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

Yes, this is another way to do it. I prefer having an explicit representation of the types of the embedded language though. For one, the multi-parameter type classes get a bit unwieldy if you have lots of types in your embedded language. Also, sometimes you might want to do special things with the denotations of each type. For instance, I did an embedding of Levy's CBPV, where the type system is split into value types and computation types. For the computation types X there is always an algebra map of type m [[ X ]] -> [[ X ]]. To define this I needed a term level representative of the type, and also the type family to give the semantics of the embedded type. I don't know if this is easily done using multi-parameter type classes.

...

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.)

Yes, thanks for reminding me. I vaguely remembered when I went to bed after posting that you had done something via Plotkin's CPS transformations. I rather like the direct approach though; sometimes it is nice not to have to solve every problem by hitting it with the continuations hammer ;). Bob -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.