[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 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? Generally speaking, Bob Harper might have answered this question by saying: > i think the main thing we took from russell is the principle that "a type is > the range of significance of a variable". but it would be interesting to find a reference. Vladimir. PS The precise quote from Russell 1908 is: > A type is defined as the range of significance of a propositional function, > i.e., > as the collection of arguments for which the said function has values. On May 13, 2014, at 12:43 PM, Philip Wadler <[email protected]> wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > 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? > > Yours, -- P > > . \ Philip Wadler, Professor of Theoretical Computer Science > . /\ School of Informatics, University of Edinburgh > . / \ http://homepages.inf.ed.ac.uk/wadler/ > > > On 13 May 2014 05:10, Gershom Bazerman <[email protected]> wrote: > >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list] >> >> On 5/12/14, 5:54 PM, Cody Roux wrote: >> >>> [ The Types Forum, http://lists.seas.upenn.edu/ >>> mailman/listinfo/types-list ] >>> >>> As others have noted, tracing historical shifts in points of view is >>> quite difficult. I somehow feel that the "Lawvere" part of the >>> "Curry-Howard-Lawvere-isomorphism" is at the heart of the real shift >>> from a "prohibitive" point of view to a "prescriptive" point of view. >>> >>> Thanks, Vladimir for your very interesting question. It is really a >> shame that (as far as I know) there is not a comprehensive article or book >> that we could turn to on this material. To follow up on the "Lawvere part", >> Goguen and the ADJ group developed initial algebra semantics as an >> algebraic theory of abstract data types in the early-mid 1970s, directly >> inspired by Lawvere's work in semantics. Goguen and Burstall went on to >> develop the CLEAR specification language, which elaborated these ideas, and >> as far as I know algebraic data types proper were first implemented in HOPE >> (described in Burstall, MacQueen, Sannella, 1980). It seems to me that the >> shift from data-types-as-hiding (the "abstract" notion of modularity) to >> data-types-as-presenting-actions (algebraic data types) is an example of >> precisely that shift from restriction to possibility that we're looking for. >> >> (However, I am confused by the reference to "Curry-Howard-Lawvere" as I >> thought the isomorphism proper [via cartesian closed categories] was due to >> Lambek? Is this a mistype, or was Lawvere more involved in that portion of >> the story than I realize?) >> >> In skimming papers looking for ideas here, I ran into a very funny >> counterexample as well. Reynolds' 1972 "Definitional Interpreters for >> Higher-Order Programming Languages" praises Scott semantics as follows: >> "The central technical problem that Scott has solved is to define functions >> that are not only higher-order, but also _typeless_, so that any function >> may be applied to any other function, including itself." From a modern >> perspective, this of course reads as very strange praise. But, I suppose >> (since I am too young to _know_), at the time it must have seemed that >> being typeless was essential to allowing general recursion, higher order >> functions, etc. >> >> Cheers, >> Gershom >> > The University of Edinburgh is a charitable body, registered in > Scotland, with registration number SC005336.
