[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
As others have noted, tracing historical shifts in points of view is quite difficult. I somehow feel that the "Lawvere" part of the "Curry-Howard-Lawvere-isomorphism" is at the heart of the real shift from a "prohibitive" point of view to a "prescriptive" point of view.
Of course it's hard not to cite Martin-Löf "On the Meaning of Logical Constants" (the Sienna lectures):
http://www.ae-info.org/attach/User/Martin-L%C3%B6f_Per/OtherInformation/article.pdf It explains the philosophy behind the modern attitude towards type theory. Best, Cody On 05/12/2014 01:47 PM, Vladimir Voevodsky 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? Vladimir.
