[TYPES] types

[Antti-Juhani Kaijanaho]

On Mon, May 12, 2014 at 05:40:43PM -0400, Prof Robert Harper wrote:
> 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.

There's too little proper historical research on the history of programming
languages.  I did some digging for a section on the history of types in my
PhLic thesis manuscript (to be submitted, hopefully, very soon), but since it
was a side issue, I too did not use a proper historical research approach on
it.  However, the following notes are based on what I found.

FORTRAN appears to be the first language to use a compile-time mechanism to
distinguish between integers and floating point values.  ALGOL 58 introduced
the idea of type declarations for variables (types were still only used to
distinguish between integers and floats).  Note that in ALGOL 58 and ALGOL 60,
arrays were not included in the type concept.  In the meanwhile, FLOW-MATIC
pioneered the idea of separating data description from the algorithm, which
directly influenced the data description capabilities of COBOL and through it
PL/I.  

The key paper in my opinion is Hoare's "Record handling" (ALGOL Bulletin 21,
1965, http://dl.acm.org/citation.cfm?id=1061041).  In prior compiled languages,
types were just a way to distinguish between integers and floats (them having
different representations and thus needed to be distinguished for the
compiler's convenience), but Hoare combined the ideas of structured values and
reference values into the now-familiar idea of record types (and also mentions
tagged union types as a possible extension).  This paper directly influenced at
least ALGOL 68, PASCAL, and, I believe, the class concept of SIMULA 67.

On Tue, May 13, 2014 at 11:43:25AM +0100, Philip Wadler wrote:
> Vladimir's intriguing question reminds me of a related question: Why do we
> call them 'types' at all?. That is, how did the concept named by Russell
> end up as a term in computing? Perhaps someone on this list knows the
> answer.
> 
> Turing published papers on type theory, so we know Turing read Russell
> (citation available), and we know Backus used 'type' in FORTRAN (citation
> required---I just tried scanning for an early FORTRAN paper to confirm it
> uses the word 'type', but did not succeed in ten minutes). What is the line
> between these two? Did Turing use the term 'type' in connection with
> computers? Did von Neumann or the other early architects? What source or
> sources influenced Backus?

Backus et al considered the design of FORTRAN 0 an easy problem and did not
spend much time on it.  I doubt they considered formal logic much.  The
following quote from the HOPL I paper (p. 32 in the book) is, I think,
illuminating:

  "In our naive unawareness of language design problems – of course we knew
  nothing of many issues which were later thought to be important, e.g., block
  structure, conditional expressions, type declarations – it seemed to us that
  once one had the notions of the assignment statement, the subscripted
  variable, and the DO statement in hand (and these were among our earliest
  ideas), then the remaining problems of language design were trivial"

The October 1956 manual for FORTRAN uses the word "type" a lot, talking about
"[t]wo types of constant" (p. 9) and "[t]wo types of variable" (p.9; in both
cases, integer and floating point) but also of "32 types of statement" (p. 8)
including "IF-type [and] GO TO-type" (p. 21).  It seems to me their use of type
follows from ordinary English, not from the theory of types in logic.

The programming language community did not seem to be aware of the development
of logic in general much, at least until the end of the 1970s.  McCarthy was
aware of the lambda calculus when he came up with LISP but had not studied it
in detail.  Landin (1965, doi:10.1145/ 363744.363749) used an untyped lambda
calculus to describe Algol 60, which is typed.  The first use of the simply
typed lambda calculus I have been able to find was in Morris' PhD thesis (1969,
http://dspace.mit.edu/handle/1721.1/64850), which does not cite any literature
on it; I get the impression he was not aware of the previous work and
independently rediscovered it.  Reynolds (1974, doi:10.1007/3-540-06859-7_148)
cited Morris for the idea of a typed lambda calculus and no source from the
logic side of things so far as I can see.  Milner (1978) did not cite Girard
although he did cite Reynolds; his only citation from the logic side is to
Hindley, unknown to him while he was working on the ideas of the paper (and
Scott, if one counts him as being on the logic side).	

-- 
Antti-Juhani Kaijanaho