On Oct 25, 2006, at 5:24 AM, Conor McBride wrote:
Hi again
[editing slightly]
Russell O'Connor wrote:
Conor McBride
writes: may I now write
boo :: WrapVoid -> x hoo :: Void -> Bool -> x
with no equations? It would be considered ``covered''; however you may, at your option, wish to add function body to handle (Wrap x). This is considered covered, but again you may, at your option, wish to add a function body to handle the hoo v True and hoo v False cases.
Hmmm. For GADTs, I fear that this coverage checking problem may be undecidable. To see why, check page 179 of my PhD thesis, although the result (due to Gerard Huet, I believe) was certainly known to Thierry Coquand in 1992. But...
Basically we considered all the cases covered if they are covered for all non-bottom values. This is (I understand) what the warning in GHC does.
...isn't (Wrap _|_) a non-bottom value? Doesn't
moo (Wrap v) = True
distinguish (Wrap _|_) from _|_ ?
If you're willing to tolerate the need to cover these cases, coverage checking becomes decidable! Of course, it leaves you wondering what to write on the right-hand side...
I would also be willing to consider Christian Maeder's proposal where a missing function body is never an error.
I'd be more comfortable with a more explicit way to leave a stub, but I agree that there should be a way to indicate 'unfinished' which is distinct from 'defined to be _|_'.
I'd have to say that all we really need for the original problem is a case statement with no arms. eg, data Void void :: Void -> a void x = case x of {} However, I feel this whole conversation is pretty academic because void x = undefined has exactly the same semantics, and void x = x `seq` undefined will even have pretty much the same operational behavior. I agree that being able to directly implement the Void catamorphism is appealing, I just don't think it makes a big practical difference. I would not at all like to see the ability to define functions by just writing type signatures.
Moreover, I should very much like to have a token I can write in the place of an expression, such that on compilation, I receive a diagnostic giving me as much type information as possible about what must replace the token. When you try the old trick of making a deliberate type error to achive this effect, you often get less back than you might hope. Fine for genuine errors, but not enough to satisfy the ulterior motive.
Cheers
Conor
Rob Dockins Speak softly and drive a Sherman tank. Laugh hard; it's a long way to the bank. -- TMBG