[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Is it possible that calling them "types" in FORTRAN was just a coincidence in that it used the same term used by Russell? I was under the impression that types as used in that language didn't really have as much of a mathematical basis as they do today. Tamreen On Tue, May 13, 2014 at 6:52 AM, Philip Wadler <[email protected]> wrote: > [ 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. > >
