A conclusion? [CST-2] Types: Ex 4.3.2

[Andrew Rogers]

On Fri, 31 May 2002, Matej Pfajfar wrote:

> > let x = ((\x.x) (\x.x)) in (x 5)
> >
> > Since A != {} and M1 is an application...
>
> I think this types OK in both?

Maybe it bears explanation why this doesn't work and the example I gave
does.  The (letv) rule may be applied when either:

i)  M1 is a value, or
ii) A = {}

Thus we may _not_ use (letv) when:

i)  M1 is not a value, _and_
ii) M1's type is not a ground type (i.e. A != {})

But |- (\x.x)(\x.x) : int -> int in our extended ML system, so that A = {}
and |- let x = ((\x.x)(\x.x) in (x 5) : int.

So to generate a counter-example, we need both M1 not to be a value (e.g.
an application as above) and we need M1 not to be a ground type, i.e. it
has to be used polymorphically.  The only way to do this is for M1 to be a
function as was suggested, but it must be applied to (at least) two
different types, otherwise M1 may be simply typed at a ground type using
(var >), thus giving A = {}.

I was looking through my Types notes when I got back in yesterday evening,
and as Pitts says, the introduction of (letv) is not a significant
hindrance to the use of ML, because we can turn an application into a
lambda-extraction by visiting our favourite takeaway...*, e.g.

((\x.x)(\x.x)) => \y.((\x.x)(\x.x))y

so that my example:

let x = ((\x.x)(\x.x)) in (let y = x(\y.y) in x true)

becomes:

let x = \a.((\x.x)(\x.x))a in (let y = \b.(x(\y.y))b in x true)

Which is typeable in both ML and ML+ref.  I also happened to note down
Pitt's own example, as he seems to love bool lists...

let f = (\x.x)(\x.x) in (f true)::(f nil)

which is of course typeable as bool list in his ML but not ML+ref.  The
fix is, as above:

let f = \y.(\x.x)(\x.x)y in (f true)::(f nil)

so that M1 is a value.  I hope this may help some people understand at
least some of the threads on this list...

|- cst2 : long list

Yours,



Andrew

*: I'm a CompSci, I have to make jokes about Curry...

-- 
Andrew D. Rogers     |                      | "For it is by grace you have
126 Huntingdon Road  | Phone: 01223 523198  |  been saved, through faith..
Cambridge            |    ICQ: 65332411     |  it is the gift of God"
CB3 OHL              |                      |               Eph 2:8-9