[TYPES] types

[Simone Martini]

There is not a real tension between 
"types as restriction" (Russell) and "types as enablers" 
(modern programming languages)--these two views live at two different levels. 

From the syntactical point of view, what Russell says it is an
obvious truth, for their types and for our types. There are
programs which would be correct according to a BNF grammar which become
illegal after typing. And, if we insist that typing be decidable, 
there will be programs which will not cause any type error during
execution, and still will be declared illegal by typing. 

The essential difference with respect to Russell (and Church, and most of
the "types-as-a-foundation-of-mathematics" authors) is that for them
types where never supposed to be actually used by the working mathematician
(with the debatable exception of Russell himself). It was sufficient that
*in principle* most of the mathematics could be done in typed languages.

Types in programming languages, on the contrary, while being restrictive in the
same sense, are used everyday by the working computer programmer. 
And hence, from the very beginning in Algol and Pascal, computer science had
to face the problem to make types more "expressive", "flexible", "enabling".
One of the first explicit attempts to combine these two views is certainly the 
early work on LCF/ML---Damas-Milner type inference providing a powerful
mechanism of enforcing type restrictions while allowing more liberal (but principled!)
reasoning. 

The crucial point, here and in most computer science applications of
mathematical logic concepts and techniques, is that CS never used 
ideological glasses (types per se; constructive mathematics per se; etc.),
but exploited what it found useful for the design of more elegant,
economical, usable, etc. artifacts.

-s.



On 12/mag/2014, at 19.47, 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.
> 
> 
> 
> 
>