[CST-2] Types: Ex 4.3.2

[Matej Pfajfar]

Well it must violate the new side condition that x is non-expansive, i.e.
either A=0 or M_1 is a value.

Try let p = (fn x.x) (fn x.x) in
  let u = p (fn y.y+1) in
    p 3

(fn x.x) (fn x.x) is not a value so we have to type
let u = p (fn y.y+1) in p 3 in the environment a,p:a->a.

This fails because the two instance of p have type int->int and (int->int)
-> (int->int), and remember than a is not universally quantified.

I am a bit confused as to whether (fn x.x) (fn x.x) is a value or not ...
help!!

On Fri, 31 May 2002, R. Bansal wrote:

> Give an example of a let-expression not involving references which is
> typeable in the ML type system of Section 2.3, but not in the ML+ref of
> section 4.2??
>
> Can't figure out the right example.
>
> Reena
> ----
>
>
>
> _______________________________________________
> CST-2 mailing list
> CST-2@srcf.ucam.org
> http://www.srcf.ucam.org/mailman/listinfo/cst-2
>

--
Matej Pfajfar
St John's College, University of Cambridge, UK

GPG Public Keys @ http://matejpfajfar.co.uk/keys
WARNING: THIS E-MAIL ACCOUNT WILL BE DELETED ON
         15/07/2002. PLEASE USE mp@cantab.net.