A Pointless Library Proposal
Donald Bruce Stewart
dons at cse.unsw.edu.au
Mon Oct 23 22:12:33 EDT 2006
> 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
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
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.
More information about the Libraries