Alexander Dunlap wrote:
wren ng thornton wrote:
Jules Bean wrote:
head uses "error" in precisely the correct, intended fashion.
head has a precondition (only call on non-empty lists)
And that is *exactly* my complaint: the precondition is not verified by the compiler. Therefore it does not exist in the semantic system, which is why the error screws up semantic analysis.
The type of head should not be [a] -> a + Error, it should be (a:[a]) -> a. With the latter type the compiler can ensure the precondition will be proved before calling head, thus eliminating erroneous calls.
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.
The issue is the obligation of proof, not what the actual runtime values are. Types give a coarsening of the actual runtime values, but they're still fine-grained enough to catch many errors (e.g. we know readFile will return some String and not an Int, even if we don't know which particular string it'll return). The proposal is to enhance the vocabulary of types such that we can require certain new proofs (e.g. having head require the proof that its argument is non-empty). The only way to discharge the obligation is to provide a proof. In this case, the way we provide a proof is by using a case expression--- it knows the actual runtime value because it evaluates things enough to match the patterns. For example, consider let x = ... in case x of x1@p1 -> f x1 ... x2@p2 -> g x2 ... Under the current system x, x1, and x2 all have the same type, by definition. We can relax this however since it is guaranteed that by the time x1 enters scope it will be bound to a value that adheres to the pattern p1; and we similarly know that x2 must be bound to a value that adheres to p2 (Removing things that also match p1). With that in mind, if the function f requires a proof of p1 about x1 (or g requires proof of p2 about x2), those obligations are discharged because the calls to f and g are guarded by the case expression. Given such a type system, your example would fail to type check because lines does not offer the guarantee that the return value is of type ((a:[a]):[[a]]). That is, the compiler will tell you that you need to provide proofs, i.e. handle all cases. As always, the devil is in the details; but that's what research is for :) -- Live well, ~wren