[TYPES] types

[Tony Dekker]

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 / dekker at acm.org


On Tue, May 13, 2014 at 9:53 PM, Philip Wadler <wadler at inf.ed.ac.uk> 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 <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.
>>>
>>>
>>
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
>