[ 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!
