[TYPES] types

[Prof Robert Harper]

hi vladimir,

i think the main thing we took from russell is the principle that "a type is the range of significance of a variable".  their focus was, i think, on the avoidance of paradoxes such as russell had found in frege's system, and it was thought that some form of stratification would be necessary to avoid "vicious circles".  russell was, in particular, critical of impredicative definitions of any kind, exactly because of their quasi-circular nature.

reynolds's dictum pertaining to types for programming languages is that "a type system is a syntactic discipline for enforcing levels of abstraction".  i like this definition, because it emphasizes that the power of a type system arises from its strictures, which can be selectively relaxed, not its affordances, which sacrifice the ability to draw sharp distinctions.  the limiting case of the latter are uni-typed languages whose one type is better viewed as one of many types in a richer language.  by using the one distinguished type among many possibilities in a multi-typed language, one can recover the freedoms of the uni-typed setting, but not the other way around.  a similar situation obtains with respect to laziness: if all types are pointed, then there are no unpointed types, but a pointed type is an example of a (not necessarily pointed) type.

as to the first use of types in a programming language, i suspect one could argue for algol-60, but i am not a historian of these topics, so perhaps there were earlier examples. even fortran had types (for different numbers and for arrays), but algol took them a lot more seriously, it seems to me.  much later, pascal popularized the use of types, but many regarded it as a backward step because the type system was so primitive (though rather advanced for its time) that it could be hard to manage.  similar ideas were used in simula, which later led to languages such as java, and in algol-68, which made an impressive use of types, but which was not very successful in practice.

the big breakthrough came with the discovery/invention of type inference, milner's algorithm being the classic result in this area, which showed that in a purely functional language of considerable expressive power one could write typed programs without ever mentioning a type.  this was the game-changer, because it eliminated fruitless arguments about the "clutter" and "annoyance" of having to write down types all the time, and focused attention on the role of types in the semantics of the situation.

although it wasn't considered such at the time (afaik), lisp was in fact one of the first practical typed languages that greatly increased the expressive power available to programmers by having a sufficiently rich type that included symbols, pairing, and a form of higher-order functions (the early dialects didn't get this quite right, but it was on the right track).  it was at the time almost magical that one could just write down a list and manipulate it without having to worry about how it would be allocated in memory.

martin-loef's paper "constructive mathematics and computer programming" was the first paper to draw the explicit connection between type theory (viewed as a formulation of constructive mathematics) and programming.  it is one of the most influential papers ever written in computer science for that reason.  it directly inspired nuprl, coq, alf, agda, and numerous other languages and provers.

best,
bob harper

On May 12, 2014, at 13:47, Vladimir Voevodsky <vladimir at ias.edu> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Hello,
> 
> I am reading Russell's texts and the more I investigate them the more it seems to me that the concept of types as we use it today has very little with how types where perceived by Russell or Church.
> 
> 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."
> 
> The types which we use today are a constructive tool. For example, types in Ocaml are a device without which writing many programs would be extremely inconvenient.
> 
> I am looking for a historic advice - when and where did types appear in programming languages which were enabling rather than forbidding in nature?
> 
> Vladimir.
> 
> 
> 
> 
>