A Pointless Library Proposal
Conor McBride
ctm at cs.nott.ac.uk
Thu Oct 26 03:19:40 EDT 2006
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
More information about the Libraries
mailing list