A Pointless Library Proposal

Donald Bruce Stewart dons at cse.unsw.edu.au
Mon Oct 23 22:12:33 EDT 2006

```kahl:
> Samuel Bronson <naesten at gmail.com> wrote:
>  >
>  > On 10/23/06, John Meacham <john at repetae.net> wrote:
>  > > On Mon, Oct 23, 2006 at 03:26:33PM +0100, Conor McBride wrote:
>  >
>  > > data Bottom
>  > Why not "data Void"?
>
> I'd say that ``Void'' is not a desirable candidate
> since too many people know C,
> and the C type ``void'' corresponds to ``()'' (or ``IO ()''...)
>
>
> (One name I have used before is ``Empty'', but I find ``Zero''
> and ``Absurdity'' appropriate, too.
> ``Absurd'' perhaps sounds more like a value than like a type...)
>

A precedent for Void comes from Djinn, http://darcs.augustsson.net/Darcs/Djinn,

Since Djinn handles propositional calculus it also knows about the
absurd proposition, corresponding to the empty set.  This set is
called Void in Haskell, and Djinn assumes an elimination rule for the
Void type:

data Void
type Not x = x -> Void
void :: Void -> a

Using Void is of little use for programming, but can be interesting
for theorem proving.  Example, the double negation of the law of
excluded middle:

Djinn> f ? Not (Not (Either x (Not x)))
f :: Not (Not (Either x (Not x)))
f x1 = void (x1 (Right (\ c23 -> void (x1 (Left c23)))))

I'd go so far as to say its intuitive to use Void, after the last year
spent playing with Djinn online.

-- Don
```