[CST-2] Types: Ex 4.3.2

[Andrew Rogers]

On Fri, 31 May 2002, Sam Staton wrote:

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

So we should use booleans instead.  For a proof of the validity of the
typing in Pitt's ML, see:

http://marvin.chu.cam.ac.uk/~adr26/types.pdf

Clearly this typing does not hold in ML+ref because both instances of the
(let) rule use applications, so the (letv) rule could not be substituted.
Anyone who says I should be revising and not drawing inference trees in
LaTeX is probably right!

Andrew

-- 
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