Scott Brickner scottb at brickner.net
Thu Dec 21 15:20:09 EST 2006

```Jacques Carette wrote:

> Neil Mitchell wrote:
>
>> The biggest
>> runtime crasher is probably pattern match failings, something that
>> most of these type extensions don't catch at all!
>
> Array out-of-bounds, fromJust, head on an empty list, and
> pattern-match failures are in my list of things I wish the type system
> could help me with.  And sometimes it can [again, see Oleg's posts].
> But is definitely where I am *eager* to see developments.

If I understand things correctly (admittedly, a big "if" ;) ) this is
kind of the point of dependent types.

A type is a set - when you put a type on an expression, you're asserting
that the expression evaluates to a member of that set. So, "foo ::
Integer -> Rational", among other things, asserts that the result of
"foo x" (given that "x" is a member of the set of Integers) is a member
of the set of Rationals. But why stop there? Why not be able to say that
"foo x" is a /positive/ rational, or a non-negative rational between 0
and 1? Or, since we're just describing sets, why not explictly allow the
set to depend on x? Why not let the result type be "the set of rationals
r such that 1/r == x"?

The Curry-Howard isomorphism leads to all of that. A program that
outputs some value "x" is (isomorphic to) a proof that x is a member of
some type. We just generally lack a sufficiently powerful type grammar
to express that directly in the program. Dependent types let you make
the types of output /depend/ on the actual values of the input.

Check out Conor McBride and James McKinna's paper "The View From the
Left", and their work on the Epigram language to see where they've taken
this... http://www.dcs.st-andrews.ac.uk/~james/ - fascinating stuff.

I agree with you, though - I'm very eager to see further developments
along these lines. It's the main reason I started learning Haskell, and
I'm absolutely convinced that functional programming and this kind of
increasingly strong typing are the way of the future for programming.

--
-----
What part of "ph'nglui bglw'nafh Cthulhu R'lyeh wagn'nagl fhtagn" don't you understand?

```