[Haskell-cafe] Use unsafePerformIO to catch Exception?

[wren ng thornton]

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 at p1 -> f x1 ...
                    x2 at 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