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