Hi David Menendez wrote:
Conor McBride writes:
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!
I think you could avoid that frustration by defining Zero/Void/Bikeshed liko so:
newtype Void = Void { avoid :: forall a. a }
That gets you a strictly defined avoid and emphasizes that Void is isomorphic to (forall a. a).
Aha, the Church Void! That's a neat way of doing it under the circumstances. The datatype with no constructors issue will show up again with GADTs, but this is a sensible way to postpone it. I guess (to answer Rob Dockins) that it's not the number of lines I'm bothered by, but rather the invocation of 'undefined', 'error' or some other signal of /underdefinition/ to present a function which is entirely well-defined, indeed trivially so. This may seem academic, but with types being used increasingly in their role as evidence, we'll eventually need to be comfortable with negative information as well as positive.
On a semi-related note, how about instances for the Prelude classes?
For example,
instance Show Void where show = avoid
instance Read Void where readsPrec _ _ = []
instance Eq Void where a == b = avoid a
instance Ord Void where compare a b = avoid a
Absolutely! It's not a joke. Some notion of Zero (and here's really why I like Zero) is very useful if you're doing algebra, let alone calculus with data structures. Given how many of our favourite datatypes are fixpoints of polynomial functors, with Show, Eq, etc, it's important that each of the building blocks of polynomials is closed under these things. You might not often need to use a Zero in the polynomial datatypes you define, but it's useful to have Zero if you're calculating one polynomial from another. I want to get for free that if my datatype has polynomial nodes, its type of one-hole contexts is showable. All the best Conor