[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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.
