A Pointless Library Proposal

[Robert Dockins]

On Oct 25, 2006, at 5:24 AM, Conor McBride wrote:

> 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 _|_'.


I'd have to say that all we really need for the original problem is a  
case statement with no arms.  eg,


data Void

void :: Void -> a
void x = case x of {}


However, I feel this whole conversation is pretty academic because

void x = undefined

has exactly the same semantics, and

void x = x `seq` undefined

will even have pretty much the same operational behavior.  I agree  
that being able to directly implement the Void catamorphism is  
appealing, I just don't think it makes a big practical difference.


I would not at all like to see the ability to define functions by  
just writing type signatures.

> 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


Rob Dockins

Speak softly and drive a Sherman tank.
Laugh hard; it's a long way to the bank.
           -- TMBG