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.