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