[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Philip, That's true -- I can't trace an exact path, but Turing does at least cite that 1940 paper by Church [Newman and Turing (1942), "A Formal Theorem in Church's Theory of Types" / Turing (1948), "Practical Forms of Type Theory"]. More significantly, ALGOL 60 was influenced by Church, and Landin explicitly acknowledges that in some of his papers. I'm *guessing* this influence extended to ALGOL's type system, but I haven't checked. -- Anthony Dekker / [email protected] On Tue, May 13, 2014 at 9:53 PM, Philip Wadler <[email protected]> wrote: > 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. > >
