[TYPES] types

[Jamie Andrews]

Coming a little late to the party, with apologies.

My impression is that the early use of types in programming languages, 
in languages such as Fortran, Cobol, PL/I and the Algols, mostly 
concentrated on distinctions between primitive types, such as integers 
and floating-point numbers, and on arrays.  By the early 1970s, with B, 
BCPL, C and Pascal, this had expanded to pointers and "structs" 
("records" in Pascal).  "Type" here was just a natural English word to 
apply to this concept, as it had been for Russell to apply to a somewhat 
different concept.

Note that none of these kinds of types has much in common with the types 
that had been studied in type theory up to that point. Church's T system 
was built on a set of base types, which play the role that primitive 
types play in programming languages, but I don't think that the type 
theorists gave them much thought.  The types that they worked with most 
were types of functions, predicates, connectives and so on.

Independent of programming languages and preceding them, the genesis of 
types seems to be Russell's use of types to resolve the set-theoretic 
paradoxes.  This led (after some false starts) to Church's T system.  
 From there, the chain of discoveries seems to go as follows.  Dana 
Scott's PPLAMBDA paper does not refer explicitly to Church, but I think 
it's safe to assume from the paper that he knew about system T.  Milner 
et al., in their Edinburgh LCF book, refer to the PPLAMBDA paper as the 
source of the idea of types being applied to classify functions.  From 
there, Church-style types (usefully extended) made their way into ML.

It was only after ML that people started really trying to unify the old 
Pascal-style types and the type theory-based types.  I think of 
Cardelli's name in this context, and I believe that he had a lot to do 
with it, but that he wasn't the only one.  "structs" correspond to 
products and "unions" to sums; if we want to pass around functions, or 
objects "containing" functions, then we need to assign types to 
functions; and so on.  Cardelli's big monograph "Type Systems" contains 
(for me) the clearest exposition of those ideas.

It is interesting that Christopher Strachey knew Dana Scott, and was 
involved in the development of B and BCPL in the late 1960s, but (to my 
knowledge) did not make the connection between type-theoretic types and 
programming-language types.  But I might just not be familiar with all 
the evidence in that regard.  I imagine that some smart people at the 
interface between type theory and programming languages must have 
noticed a connection in a general way, but they don't seem to have made 
any solid progress until ML came on the scene.

cheers
--Jamie.