Re: [TYPES] types

[ 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 <carette-xc3H/SjimlosA/[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.