[TYPES] types

[Philip Wadler]

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 <tony.dekker at gmail.com> 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 / dekker at acm.org
>
>
> On Tue, May 13, 2014 at 8:43 PM, Philip Wadler <wadler at inf.ed.ac.uk>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 <gershomb at gmail.com> 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.
>>
>>
>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.seas.upenn.edu/pipermail/types-list/attachments/20140513/350c4cf0/attachment-0001.ksh>