[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Another landmark paper in the development of types as enablers is: Jim Morris, Types are nots sets, POPL 1973. (That's the first POPL.) http://dl.acm.org/citation.cfm?id=512938 Yours, -- P . \ Philip Wadler, Professor of Theoretical Computer Science . /\ School of Informatics, University of Edinburgh . / \ http://homepages.inf.ed.ac.uk/wadler/ On 13 May 2014 09:12, Derek Dreyer <[email protected]> wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list] > > Hi Vladimir. > > I would argue that types are enabling *because* they are forbidding. > That sounds very zen, but I have a concrete point in mind. > > As Bob mentioned already, it was Reynolds who observed that types are > useful for syntactically enforcing levels of abstraction, and what > that really meant to Reynolds is that one can locally establish > invariants for -- and change private representation of -- abstract > data types (ADTs), without affecting the observable behavior of code > that relies on those types. From my perspective, the crucial point > here is that types *enable* programmers to write more reliable code > because the burden of establishing invariants on an ADT is kept > *local* to the module that defines it. The restrictions of the type > system then guarantee that the rest of the program, by virtue of being > forced to respect the abstraction of the ADT, is also forced to > respect the ADT's locally-established invariants. Thus, the very > restrictiveness of types is what enables program *correctness* to > scale. > > Notice I said program correctness, not verification. What I mean is > that programs written in mainstream typed languages often behave > correctly due to complex invariants on ADTs that the programmer has in > their head but that have not been written down or verified. These > invariants are often really complex -- we are only now in a stage of > verification research where we can even begin to express them > formally! But even ignoring formal verification, types have the > practical benefit of enabling the programmer to do some complex > informal reasoning locally but have confidence that it holds good when > the ADT is used in a much larger program. > > Best regards, > Derek > > On Mon, May 12, 2014 at 7:47 PM, 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. > > > > > > > > > > > >
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
