A Pointless Library Proposal

[Conor McBride]

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.