A Pointless Library Proposal

[Conor McBride]

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