[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Thanks, Tony, but that answer is incomplete. What is the linkage from Church to the early computing machines? Turing is an obvious link, but I don't know in which paper, or whether, he uses types in connection to computing machinery. I had thought FORTRAN referred to types, but I am halfway through downloading an early paper and it appears I may be mistaken. So Church may be part of the path, but what is the rest? 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 12:45, Tony Dekker <[email protected]> wrote: > Why do we use Russell's term "types"? Church's classic 1940 paper "A > Formulation of the Simple Theory of Types" explicitly cites Russell's work > as an influence. Because of Church's great influence, I presume this paper > provides the "linkage." > > -- Anthony Dekker / [email protected] > > > On Tue, May 13, 2014 at 8: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. >> >> >
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
