Re: [TYPES] types

[ 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