Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
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 <jeff.polakow@d...>
Subject: Re: [Caml-list] Re: Void type?

> > 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:



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.