Talk:Letrec

From The Twelf Project

[edit] Different formalism?

The formalism on the current page is probably the right thing to do for "real-world binding", since it's closest to the actual syntax that people will have in mind.

However, it looks a little funny to me to have projection from an object as a language construct, without the objects themselves being first class. Would it be better to do a version with objects and define letrec as syntactic sugar for an object that you immediately split? I guess that doesn't show off the binding issues as well, since an object only binds one name and the components are accessed by projection.

Maybe at the end of this case study, we can say that letrec doesn't need to primitive, and elaborate it as letrec x1 = e1 ... in e

translates to

let o = obj x is (e1[pi_1 o/x1], ...) in let x1 = pi_1 o in

   ...

in e

Drl 15:22, 16 October 2007 (EDT)