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.