Y-Combinator in FT EDSL

Question

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

Don Stewart

138k36 gold badges372 silver badges472 bronze badges

asked Jun 23, 2010 at 16:32

sclv 39k7 gold badges102 silver badges208 bronze badges · 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.

answered Jun 23, 2010 at 17:11

sclv

39k7 gold badges102 silver badges208 bronze badges

Comments

Don Stewart 138k36 gold badges372 silver badges472 bronze badges · Answer 2 · 2010-06-23T18:16:42.933Z+00:00

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

Comments

2 Comments