[TYPES] types

[Sean McDirmid]

There are two places where I have seen types used prescriptively rather than restrictively. 

(1) Type-based implicit resolutions in languages like Scala. 

(2) Code completion in IDEs that is enabled by type information; types are typically used to filter choices for the programmer's "next move." 

(2) is more of a tooling concern, but it is important enough to be a first class concern in production languages (i.e. language features are evaluated based on how they help/hurt code completion). 

> On May 13, 2014, at 4:28 AM, "Vladimir Voevodsky" <vladimir at ias.edu> 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.
> 
> 
> 
> 
>