Re: [TYPES] types

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

On Mon, May 12, 2014 at 10:47 AM, Vladimir Voevodsky <[email protected]>wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
>
> Hello,
>
> I am reading Russell's texts and the more I investigate them the more it
> seems to me that the concept of types as we use it today has very little
> with how types where perceived by Russell or Church.
>
> 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."
>
> The types which we use today are a constructive tool. For example, types
> in Ocaml are a device without which writing many programs would be
> extremely inconvenient.
>
> I am looking for a historic advice - when and where did types appear in
> programming languages which were enabling rather than forbidding in nature?
>

My understanding, which may be wrong/incomplete, is that types started to
appear as a powerful mechanism in computer science with Milner and ML. For
instance:

Robin Milner. A theory of type polymorphism in programming. Journal of
Computer and System Sciences, 17:348-375, August 1978.

I got that paper from this list, which contains many other great papers to
help you build up an historical context:
http://www.cis.upenn.edu/~bcpierce/courses/670Fall04/GreatWorksInPL.shtml

I hope that helps!