A Pointless Library Proposal

[Russell O'Connor]

Conor McBride <ctm <at> cs.nott.ac.uk> writes:

> So, taking Void to be the colour of the empty bikeshed and
> 
>   avoid :: Void -> x
> 
> suppose I define
> 
>   data WrapVoid = Wrap Void
> 
> may I now write
> 
>   boo :: WrapVoid -> x
> 
> with no equations? Does this cover? Or does it neglect the crucial boo 
> (Wrap _|_) case?

It would be considered ``covered''; however you may, at your option, wish to add
function body to handle (Wrap x).
 
> What about
> 
>   hoo :: Void -> Bool -> x
> 
> ? Does this cover, or did I forget hoo v True and hoo v False?

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.

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.

I would also be willing to consider Christian Maeder's proposal where a missing
function body is never an error.