wadler at inf.ed.ac.uk
Tue May 13 09:32:31 EDT 2014
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.
. \ 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 <carette at mcmaster.ca> 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
> I have not read this book http://www.amazon.com/History-
> Philosophy-Constructive-Synthese-Library/dp/9048154030 but it appears
> However, I am quite surprised that no one has yet mentioned "A Modern
> Perspective on Type Theory",
> 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.
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
More information about the Types-list