[TYPES] types

[Uday S Reddy]

Vladimir Voevodsky writes:

> For them types were a restriction mechanism. As Russell and Whitehead
> write:
> 
> "It should be observed that the whole effect of the doctrine of types is
> negative: it forbids certain inferences which would otherwise be valid,
> but does not permit any which would otherwise be invalid."

I am afraid the situation was very much the same in early programming
language theory as well.  Milner's "theory of type polymorphism in
programming", which was mentioned by somebody earlier, defines an untyped
calculus and then a typed version of it (ML) as a restriction of the untyped
calculus.  The selling point is that the programs that belong to the typed
subset don't go "wrong".

The first place where I have seen a contrary view was in:

    Dana Scott, Relating theories of the lambda calculus, in "To H.B. Curry:
    Essays in Combinator Logic, Lambda Calculus and Formalism", Hindley and
    Seldin (eds), Academic Press, 1980.

Here, Scott argues that the typed lambda calculus is conceptually prior to
the untyped calculus, and that the untyped calculus is just a special case
of the typed calculus with a single type.  That was quite remarkable to me
at that time, coming as it did from the master of the untyped lambda
calculus himself!

I don't know how widely this paper was read, but when I went to the
"Semantics of Data Types" conference in 1984, I noticed that almost
everybody was talking about typed calculi without worrying much about the
untyped lambda calculus.

By 1984, the polymorphic lambda calculus (System F) was a hot topic
(frequently called the "Girard-Reynolds calculus" at that time).  Both
Girard and Reynolds defined their calculus without any reference to any
untyped calculus.  So, all other people that worked with the polymorphic
lambda calculus also followed the same approach.

So, it seems to me that Scott, Girard and Reynolds, somehow jointly killed
the untyped lambda calculus as a foundation by 1984.

Cheers,
Uday