A Pointless Library Proposal

[Conor McBride]

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.

Cheers

Conor