carette at mcmaster.ca
Tue May 13 13:31:17 EDT 2014
On 14-05-13 09:09 AM, Sam Tobin-Hochstadt wrote:
> On Tue, May 13, 2014 at 7:57 AM, Jacques Carette <carette at mcmaster.ca> wrote:
>> [I use 'enable' here, knowing that one can do pattern matching without sums
>> and without types, but the results are not as compelling.]
> 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 ). Types and sums without
> pattern matching is easy to define, but as you say, awkward to program
> Sam Tobin-Hochstadt
>  http://www.ccs.neu.edu/racket/pubs/sfp10-kth.pdf with source at
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.
More information about the Types-list