[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
I finally downloaded a scan of "The FORTRAN automatic coding system". The word type appears several times, for instance to distinguish "IF-type statement" from "DO-type statement", but is not used to distinguish fixed-point from floating-point. Yours, -- P J. W. Backus, et al, The FORTRAN automatic coding system, Papers presented at the 26-28 February 1957, Western Joint Computer Conference. http://dl.acm.org/citation.cfm?id=1455599 . \ Philip Wadler, Professor of Theoretical Computer Science . /\ School of Informatics, University of Edinburgh . / \ http://homepages.inf.ed.ac.uk/wadler/ On 13 May 2014 12:57, Jacques Carette <[email protected]> wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list] > > The history of type theory is actually rather well laid out at > http://en.wikipedia.org/wiki/History_of_type_theory. > > I have not read this book http://www.amazon.com/History- > Philosophy-Constructive-Synthese-Library/dp/9048154030 but it appears > topical. > > However, I am quite surprised that no one has yet mentioned "A Modern > Perspective on Type Theory", > http://www.springer.com/mathematics/book/978-1-4020-2334-7 > which takes a historical path through type theory. Perhaps because the > types mailing list is inhabited by mainly PL people? > > Having said that, I want to focus on a particular aspect of the question: > > > On 2014-05-12 1:47 PM, Vladimir Voevodsky wrote: > >> 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. >> > > While many have been quite philosophical about what this means, I think > something quite simple is being forgotten here: pattern matching. Without > types, eliminators for sums are very awkward to deal with. While one can > argue how much benefit there is in types for those whose values are given > largely through their introduction form, types really shine when types are > largely given by their elimination forms. Oh, it is possible to program > entirely in terms of eliminators, but the results are "extremely > inconvenient" indeed! > > To me, types enable a nice concept of sum types, which in turn enable a > nice notion of pattern matching . [I use 'enable' here, knowing that one > can do pattern matching without sums and without types, but the results are > not as compelling.] And pattern matching allows programs to be written > much more succinctly and clearly than without. > > Jacques > >
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
