Accueil     À propos     Téléchargement     Ressources     Contactez-nous

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Void type?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2007-07-30 (14:27) From: Jeff Polakow Subject: Re: [Caml-list] Re: Void type?
```Hello,

> > Here is what you can do with void1 and not with void2 :
> > type void1 = { v: 'a. 'a };;
> > # let void1_elim x = x.v;;
> > val void1_elim : void1 -> 'a = <fun>
>
> Maybe I should rephrase the question then.  What use is this function?
> The only Google searches for void type and the "elimination principle"
> all seem to point back to this very thread.
>
As others have mentioned the motivation for an elimination principle comes
from the Curry-Howard isomorphism. In case you're wondering, the actual
phrase "elimination principle" (or rule, or form, or whatever) comes from
the presentation of formal logic as a natural deduction system which is a
bunch of rules describing how to create valid logical deductions. The
rules of a natural deduction system are divided into introduction rules,
which explain how to deduce a formula (e.g. if you can deduce A and you
can deduce B then you can deduce A & B), and elimination rules, which
explain how a deduced formula can be used (e.g. if you can deduce A & B
then you can deduce A). Here is a wikipedia article with more detail:
http://en.wikipedia.org/wiki/Natural_deduction

-Jeff

---

This e-mail may contain confidential and/or privileged information. If you
are not the intended recipient (or have received this e-mail in error)
please notify the sender immediately and destroy this e-mail. Any
unauthorized copying, disclosure or distribution of the material in this
e-mail is strictly forbidden.
```