cody.roux at andrew.cmu.edu
Mon May 12 17:54:30 EDT 2014
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):
It explains the philosophy behind the modern attitude towards type theory.
On 05/12/2014 01:47 PM, Vladimir Voevodsky 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?
More information about the Types-list