Re: [TYPES] types

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

On 14-05-13 09:09 AM, Sam Tobin-Hochstadt wrote:
> On Tue, May 13, 2014 at 7:57 AM, Jacques Carette <carette-xc3H/SjimlosA/[email protected]> wrote:
>>   [I use 'enable' here, knowing that one can do pattern matching without sums
>> and without types, but the results are not as compelling.]
> Jacques,
>
> I'm not sure what you mean by compelling, but any pair of these three
> is available without the other.  For example, patterns matching and
> sums (but without types) are used extensively in Friedman and Wand's
> Essentials of Programming Languages textbook, and pattern matching
> with types but without sums can be seen in Typed Racket (for example,
> our paper on functional data structures [1]).  Types and sums without
> pattern matching is easy to define, but as you say, awkward to program
> with.
>
> Sam Tobin-Hochstadt
>
> [1] http://www.ccs.neu.edu/racket/pubs/sfp10-kth.pdf with source at
> https://github.com/takikawa/tr-pfds/

What I mean by 'compelling' is most influenced by my (recent) experience 
with agda-mode in Emacs: given a (dependant!) sum type, one can ask the 
IDE to give all valid case-split on a particular variable of that type.  
One is insured coverage, by the language, by construction.  This feature 
allows one to write folds over large ASTs in just a few keystrokes, with 
little chance for error.

It is really the confluence of types, sum and pattern-matching which 
hits a 'sweet spot' quite similar to what Hindley-Milner does for inference.

To me, 'compelling' usually means faster production (by a human) of 
correct *readable* code.  I want my compiler to verify certain parts of 
"correct" for me.

Jacques