A Pointless Library Proposal

Conor McBride ctm at cs.nott.ac.uk
Wed Oct 25 05:24:57 EDT 2006

Hi again

[editing slightly]

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 mailing list