[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On May 12, 2014, at 1:47 PM, 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? Viewing types as restrictive or enabling mechanisms is simply a matter of perspective, not intrinsic to the idea/language itself. One man's "types rule out X" is another man's "with types you can say that you can't get X" in a program. Furthermore, you can use typed thinking to organize the design of programs even in the absence of a type language and type checking. I have run courses for over 20 years this way and successfully so from the middle school level to the MS level. More concretely, you can program with types in "Scheme"; you don't need to be in "Ocaml" (quotes to remind readers that I mean the idea, not the exact language). Indeed, given the huge demand for "untyped" programmers, I argue that a responsible instructor must expose students to just such scenarios to prepare his students for this world. -- Matthias
