Y-Combinator in FT EDSL

Question

Hi all,

I'm trying to figure out how to express the Y-Combitor in this Finally Tagless EDSL:

class Symantics exp where
    lam :: (exp a -> exp b) -> exp (exp a -> exp b)
    app :: exp (exp a -> exp b) -> exp a -> exp b

    fix :: ...
    fix f = .....

I'm not certain but I think a default implementation of the Y-Combinator should be possible using "lam" and "app".

Anybody know how? My first attempts fail because of the "cannot construct the infinite type" thingy.

Cheers, Günther

Answer 1

If you introduce let, you can provide a default implementation. But you can't do so with lam and app alone, for the same reason you can't write it directly in Haskell without let. Your target here is an extension of the simply typed lambda calculus, and that term just won't type in it.

Answer 2

As sclv points out, you'll need to introduce a primitive fixed point form into the language. Think about how it is defined in Haskell:

fix :: (a -> a) -> a
fix f = let x = f x in x

A suitable 'let' binding form will get you there. A good reference for this kind of foundational stuff is Barendregt chapters 1 and 2, which might be at your library -- though I believe it is out of print (can anyone confirm?). A close second is http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.9283