help from the community?

[Conor McBride]

Hi

Andres Loeh wrote:

>> I think it's important to keep some possibility for the compiler to detect 
>> probable errors as syntax errors. If all syntax is inhabited by strange 
>> defaults then this just means simple errors will go undetected eg:
>>
>>    let a = case foo of
>>
>> Here, the user has probably got sidetracked into editing some other part of 
>> the program and just forgotten to get back to fill in the cases for the 
>> case construct. Allowing zero cases means the user will get a strange 
>> runtime error instead as the "function" part of the case is undefined.
>>     
>
> I agree. On the other hand, if there are uninhabited types (modulo _|_), it
> might be nice to have an empty case as an explicit eliminator.
>   

Even if GADTs aren't on the immediate agenda, it's still important to 
design with them in mind. Empty case analyses are far from odd in that 
setting. They certainly show up all the time in Epigram programming, and 
it's important to show them as part of the explanation that a program 
covers all cases. Whether totality is being enforced or not, it's good 
to be clear that a piece of code is missing because it isn't needed, not 
because it's been forgotten or left as an "undefined" stub.

However, it might be worth having a separate notation or keyword, 
unmistakably for the purpose of refuting bogus elements of empty 
datatypes: "refute foo" or "nocase foo" or "foo stinks". Moreover, we 
could consider having a compiler warning if the programmer seeks to 
refute an element of a datatype which can contain a constructor pattern.

So, as far as Haskell' is concerned, I'd favour forbidding non-empty 
cases, but only because I favour having some more explicit syntax for 
empty cases, further down the line.

All the best

Conor