[CST-2] Types: Ex 4.3.2

Sam Staton ss368@cam.ac.uk
Fri, 31 May 2002 14:12:03 +0100 (BST)


> > let x = ((\x.x) (\x.x)) in (x 5)

No, that's not good enough because A can be {} for (x 5) to type (I
try enterring it to an ML interpretter (which should be essentially
ML+ref) then it does compile.

I think Mat's example is ideal (assuming application isnt a value),
although Pitts hasnt introduced numbers (or addition) in ML or ML+ref!

-- 
sam

On Fri, 31 May 2002, Tom Puverle wrote:

> > let x = ((\x.x) (\x.x)) in (x 5)
> >
> > Since A != {} and M1 is an application...
>
> That's what I thought originally but I guess it
> depends on whether you do the Beta reduction
> before *or* after the assignment to x.
>
>
>
> _______________________________________________
> CST-2 mailing list
> CST-2@srcf.ucam.org
> http://www.srcf.ucam.org/mailman/listinfo/cst-2
>