Luke Palmer wrote:
Alexander Dunlap wrote:
> 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.
My idea amounts to trying to make case expressions more first-class than
they are now. As Luke says, we'd have to be conservative about it (until
the dependent-types and total-functional-programming folks do the
impossible), but I think there's still plenty of room for biting off a
useful chunk of the domain without falling off that cliff.
--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
