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 = > > 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.