[Haskell-cafe] Re: Versioning

[Scott Brickner]

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?