Re: [TYPES] types

[ 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.
>
>
>
>
>