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
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
