[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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" <[email protected]> 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. > > > > >
