Re: A Pointless Library Proposal

23 Oct 2006

      kahl:
...
Samuel Bronson  wrote:
...
On 10/23/06, John Meacham  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

Re: A Pointless Library Proposal

dons＠cse.unsw.edu.au