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

[Chung-chieh Shan]

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

  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