A Pointless Library Proposal

[Donald Bruce Stewart]

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, 
well-known to #haskell irc people:

    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