A Pointless Library Proposal

Russell O'Connor roconnor at theorem.ca
Wed Oct 25 04:52:59 EDT 2006

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.

More information about the Libraries mailing list