matthias at ccs.neu.edu
Mon May 12 17:24:32 EDT 2014
On May 12, 2014, at 1:47 PM, 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 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.
More information about the Types-list