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

[Robert Atkey]

On Mon, 2009-10-05 at 22:06 -0400, Chung-chieh Shan wrote:
> Robert Atkey <bob.atkey at ed.ac.uk> wrote in article <1254778973.3675.42.camel at 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.