Hi Ashley Yakeley wrote:
I wrote:
magic :: Zero -> a magic _ = error "There's magic, as no such thing!"
It's a little frustrating to have to define this function lazily. I prefer the strict definition with no lines, but it isn't valid Haskell!
This issue comes up a lot with GADTs.
It's quite familiar with dependent types too, so that shouldn't come as a surprise. Some of us have spent quite a while figuring out how to suck a complete absence of eggs.
For instance:
data MyGADT a where MyInt :: MyGADT Int MyChar :: MyGADT Char
or even data Eq a b where Refl :: Eq a a never :: Eq Int Bool -> a In 'Eliminating Dependent Pattern Matching', Healf Goguen, James McKinna and I suggest a notation which supplements the usual 'return an output' notation with a 'refute an input' notation. Something like never x _|_ x -- 'never x refutes x' which requires x to be checkably in a type with no constructors (under any hypotheses). This notation enables a machine to check whether the programmer has explained how to cover all cases by an explanation either of what to return or why there's no need. I wouldn't presume to propose this notation for Haskell, but equally, it's dangerous to presume that as more and more of these phenomena show up in Haskell, the old language choices will remain sufficient or suitable. We live in interesting times. All the best Conor This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.