Void type?
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20070730 (14:27) 
From:  Jeff Polakow <jeff.polakow@d...> 
Subject:  Re: [Camllist] 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 CurryHoward 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 email may contain confidential and/or privileged information. If you are not the intended recipient (or have received this email in error) please notify the sender immediately and destroy this email. Any unauthorized copying, disclosure or distribution of the material in this email is strictly forbidden.