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?