[TYPES] types

[Sergei Soloviev]

Hi, Vladimir,

I was reading quite a lot Cantor. When he suggested his own notion of set, he was quite unsure how
"laxist" the definition may be - essentially he would not admit that any elements (without unifying principle
or construction) can be taken together to form a set. Much more laxist view was taken by Frege and some
others, and Cantor himself started to take more risky approach  - and there result some paradoxes concerning 
ordinals that much discouraged him.

With respect to all this, Russel's types are a restriction. Constructive types (as in programming)
are restrictive in the sense that they require some common constructing principle (or principles)  behind.

All the best

Sergei Soloviev

 
 
 
Le Lundi 12 Mai 2014 19:47 CEST, Vladimir Voevodsky <vladimir at ias.edu> a écrit: 
 
> [ 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.
> 
> 
> 
> 
>