dagitj at gmail.com
Mon May 12 16:30:44 EDT 2014
On Mon, May 12, 2014 at 10:47 AM, Vladimir Voevodsky <vladimir at ias.edu>wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
> 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
> "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
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:
I hope that helps!
More information about the Types-list