[ 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 <[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
