[TYPES] types

[Vladimir Voevodsky]

> 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?

Generally speaking, Bob Harper might have answered this question by saying:

> i think the main thing we took from russell is the principle that "a type is the range of significance of a variable". 

but it would be interesting to find a reference.

Vladimir.

PS The precise quote from Russell 1908 is:

> A type is defined as the range of significance of a propositional function, i.e.,
> as the collection of arguments for which the said function has values. 
 


On May 13, 2014, at 12: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.