A Pointless Library Proposal
ctm at cs.nott.ac.uk
Wed Oct 25 05:24:57 EDT 2006
Russell O'Connor wrote:
> Conor McBride <ctm <at> cs.nott.ac.uk> 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 _|_'.
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.
More information about the Libraries