A Pointless Library Proposal

[Conor McBride]

Robert Dockins wrote:
>
> On Oct 30, 2006, at 9:38 AM, Ben Rudiak-Gould wrote:
>
>> Simon Peyton-Jones wrote:
>>> I've occasionally wondered about emitting a warning, but not an error,
>>> when there's a type signature for a function but no definition. The
>>> compiler could automatically generate an error message stub
>>> implementation, much as it does for an incomplete pattern match, of
>>> which this is an extreme example.
>>
>> I don't like this idea because the necessary stub is different for 
>> different numbers of arguments, and there's no way to tell how many 
>> arguments the programmer intended. I do like the idea of allowing 
>> empty case expressions, though, and I don't think that even a warning 
>> would be necessary.
>
>
> This opinion++

Yes, when I'm not being facetious, I'm inclined to think that some 
syntax which represents the explicit dismissal of impossible input is 
preferable to the mere absence of anything to deliver an output. Empty 
case expressions are one possibility, but I'd also be pleased to see a 
'definition form', ie some sort of pattern rejection, in the same way 
that pattern equations give a neat definition form for nonempty case 
analysis. Moreover, in the case of GADTs, if you want coverage checking, 
you need something of the sort.

The key question, unless this is just a storm in a teacup in a bikeshed, 
is how to distinguish underdefined programs from well-defined but 
vacuous ones. To do the job properly, whatever syntax is used to reject 
some element of an uninhabited datatype should be considered erroneous 
if there is a constructor-pattern of that type in some context. That is 
(if it's empty case)

  voo :: Void -> x
  voo v = case v of {}

should be fine, but

  boo :: Bool -> x
  boo b = case b of {}

should be rejected because True (and False) provide a case to answer. 
Moreover, if we have

  data Overjoid = Joy Void
  woo :: Overjoid -> a
  woo x = case x of {}
  noo :: Overjoid -> a
  noo (Joy x) = case x of {}

then woo should be rejected but noo accepted.

I'd also like to see more support for stubs in code, by way of being 
able to ask a compiler 'what more must I do here?', but I should also 
prefer this to be more actively indicated than just by an empty space.

Artful silence may be alright for Samuel Beckett, but it strikes me a 
dangerous way to be straightforward about what sort of nothing you mean.

All the best

Conor