[TYPES] types

[Altenkirch Thorsten]

Thank you Uday.

My understanding of Type Theory is that types are first and values come
later, they are only justified with reference to a type. The view that
types are only a way to classify untyped entities is outdated because it
focusses on the mechanism instead of the functionality and hence hinders
abstraction. This is also the fundamental issue with set theory, where we
can talk about elements and membership independently (and we can ask
stupid questions such as "is the empty set an element of the natural
numbers?").

While it is interesting as Vladimir suggests to look into the historic
origins of the strongly typed approach and I think you are right to
identify Scott, Girard and Reynolds but should not forget Martin-Loef, I
think it is important to overcome the low level view that untyped entities
are first, which is is still prevalent among many people.

Thorsten

On 13/05/2014 00:34, "Uday S Reddy" <u.s.reddy at cs.bham.ac.uk> wrote:

>[ The Types Forum,
>http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
>Vladimir Voevodsky writes:
>
>> For them types were a restriction mechanism. As Russell and Whitehead
>> write:
>> 
>> "It should be observed that the whole effect of the doctrine of types is
>> negative: it forbids certain inferences which would otherwise be valid,
>> but does not permit any which would otherwise be invalid."
>
>I am afraid the situation was very much the same in early programming
>language theory as well.  Milner's "theory of type polymorphism in
>programming", which was mentioned by somebody earlier, defines an untyped
>calculus and then a typed version of it (ML) as a restriction of the
>untyped
>calculus.  The selling point is that the programs that belong to the typed
>subset don't go "wrong".
>
>The first place where I have seen a contrary view was in:
>
>    Dana Scott, Relating theories of the lambda calculus, in "To H.B.
>Curry:
>    Essays in Combinator Logic, Lambda Calculus and Formalism", Hindley
>and
>    Seldin (eds), Academic Press, 1980.
>
>Here, Scott argues that the typed lambda calculus is conceptually prior to
>the untyped calculus, and that the untyped calculus is just a special case
>of the typed calculus with a single type.  That was quite remarkable to me
>at that time, coming as it did from the master of the untyped lambda
>calculus himself!
>
>I don't know how widely this paper was read, but when I went to the
>"Semantics of Data Types" conference in 1984, I noticed that almost
>everybody was talking about typed calculi without worrying much about the
>untyped lambda calculus.
>
>By 1984, the polymorphic lambda calculus (System F) was a hot topic
>(frequently called the "Girard-Reynolds calculus" at that time).  Both
>Girard and Reynolds defined their calculus without any reference to any
>untyped calculus.  So, all other people that worked with the polymorphic
>lambda calculus also followed the same approach.
>
>So, it seems to me that Scott, Girard and Reynolds, somehow jointly killed
>the untyped lambda calculus as a foundation by 1984.
>
>Cheers,
>Uday

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it.   Please do not use, copy or disclose the information contained in this message or in any attachment.  Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment
may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.