[Haskell-cafe] Re: exceptions vs. Either

[Conor T McBride]

Hi folks

Alastair Reid wrote:
 >>I have a hard time understanding why functional programmers
 >>would not want more static typing guarantees, after all they
 >>can always use C if they dont like type systems!
 >
 > I think the value of Haskell's type system is that it catches a lot 
of > bugs _cheaply_.  That is, with little programmer effort to write the
 > type annotations, little effort to understand them and little effort
 > to maintain them as the program evolves.

I entirely agree. The effort-to-reward ratio is the key consideration
when deciding how much information to build into types. I'm biased, of
course, but the thing I like about working with a dependent type system
is that I at least have the option to explore a continuum of static
expressivity and choose a compromise which suits my conception of the
task at hand. To oppose the availability of more informative types is to
rule out the option of exploiting them even when they are useful.

A key aspect of the Epigram approach is to pay attention to the
/tools/ we use to write programs. Of course it gets harder to work with
more involved types if you have to do it all in your head.
Frankly, polymorphic recursion is enough to make my brain hurt, let
alone the kind of type class shenanigans which various people (myself
included) have been engaging in. I have a not-so-secret weapon. Once
I've developed the program interactively in Epigram (or its predecessor,
OLEG, in the case of the Faking It stuff), exploiting the fact that
a computer can push type information /into/ the programming process,
it's quite easy to crank out the relevant steaming lump of obfuscated
Haskell.

One tool that's really needed here is a refactoring editor which
enables you to write the program naively, exposing the exceptional
cases, then, once you've seen where they show up, refine the data
structures to eliminate some or all of them. It's a fair cop: at the
moment, Epigram requires you to dream up the data structures from thin
air before you write the programs. That doesn't fit with the fact that
good ideas only tend to come a bit at a time. However, we can certainly
improve on this situtation, given time and effort.

 > In general, as we try to express more and more in the type system, the
 > costs go up so the goal in using a different programming style or
 > extending the type system is to catch more bugs without significantly
 > increasing the cost.  At an extreme, we could probably use some
 > variant of higher order predicate calculus as our type system

I'd recommend a system which enables you to build stronger structural
invariants directly into data structures, rather than using data
types which are too big, and then a whole pile of predicates to cut
them down to size afterwards: as you fear, the latter is a good way
to fill a program up with noisy proofs. But if you use indexed datatype
families (Dybjer, 1991), you can avoid a lot of this mess and what's
more, a type-aware editor can rule out many exceptional cases on your
behalf. In many cases, the Epigram editor shows you exactly the data
which are consistent with the invariants, without any effort on your
part.

 > and specify that a sort function (say) returns an
 > ordered list but the programmer effort in doing so would probably be
 > quite high.

I'm pleased to say it isn't. See

   http://www.dur.ac.uk/c.t.mcbride/a-case/

and in particular

   http://www.dur.ac.uk/c.t.mcbride/a-case/16so/

onwards, for treesort-enforcing-sorted-output. There's not much to it,
really. The thing is, ordinary if-then-else loses the fact that
performing the comparisons directly establishes the properties required
to satisfy the sorting invariants in the output structures. It's not
hard to remedy this situation. Moreover, most of the logical plumbing
can be managed implicitly, as it merely requires picking up proofs
which are immediately visible in the context. Of course, (see
Inductive Families Need Not Store Their Indices, by Edwin Brady, James
McKinna and myself) none of this logical stuff incurs any run-time
overhead.

 > Using Maybe and the like to catch more errors with the type system
 > isn't as expensive as using full-on specification and is often the
 > right thing to do but, in some cases, the benefits of programming that
 > way don't justify the effort required whereas the techniques suggested
 > for reporting the location of the problem are cheap and effective.

You're absolutely right. And today's technology often means that the
match-exception way, let alone the Maybe-way, wins this trade-off.
Tomorrow's technology will not remove this trade-off, but it might
sometimes change the outcome of the calculation. I think that's worth
working for.

Cheers

Conor