[TYPES] types

[Philip Wadler]

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
>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.seas.upenn.edu/pipermail/types-list/attachments/20140513/8a51f27a/attachment-0001.ksh>