On Thu, Mar 26, 2009 at 5:23 PM, wren ng thornton <wren@freegeek.org> wrote:
> It's a static error, detectable statically, and yet it's deferred to the
> runtime. I'd much rather the compiler catch my errors than needing to create
> an extensive debugging suite and running it after compilation. Is this not
> the promise of purity?

Ultimately, it's not detectable statically, is it? Consider

import Control.Applicative

main = do
f <- lines <$> readFile "foobar"
print (head (head f))

You can't know whether or not head will crash until runtime.

Static checkers are usually conservative, so this would be rejected. In fact, it's not always essential to depend on external information; eg. this program:

(\x y -> y) (\x -> x x) (\x -> x)

Behaves just like the identity function, so surely it should have type a -> a, but it is rejected because type checking is (and must be) conservative.

Keeping constraints around that check that head is well-formed is a pretty hard thing to do. Case expressions are easier to check for totality, but have the disadvantages that wren mentions.

Much as we would like to pressure the language to support static constraints, I don't think we are yet in a position to. It's not the kind of thing you can just throw on and be done with it; see Conor McBride's current project for an example of the issues involved.

Luke