From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=HTML_MESSAGE, UNPARSEABLE_RELAY autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id C70F9BC69; Mon, 30 Jul 2007 16:27:41 +0200 (CEST) Received: from imr8.us.db.com (imr8.us.db.com [160.83.65.200]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l6UEReKc012411 (version=TLSv1/SSLv3 cipher=EDH-RSA-DES-CBC3-SHA bits=168 verify=FAIL); Mon, 30 Jul 2007 16:27:41 +0200 Received: from sdbo1005.db.com by imr8.us.db.com id l6UERYLn031318; Mon, 30 Jul 2007 10:27:35 -0400 In-Reply-To: <20070729170216.GA8137@furbychan.cocan.org> To: rich@annexia.org Cc: Arnaud Spiwack , caml-list@yquem.inria.fr, caml-list-bounces@yquem.inria.fr Subject: Re: [Caml-list] Re: Void type? MIME-Version: 1.0 X-Mailer: Lotus Notes Release 6.5.5 CCH1 March 07, 2006 From: Jeff Polakow Message-ID: Date: Mon, 30 Jul 2007 10:27:29 -0400 X-MIMETrack: Serialize by Router on sdbo1005/DBNA/DeuBaInt/DeuBa(Release 6.5.5FP1|April 11, 2006) at 07/30/2007 10:27:35 AM, Serialize complete at 07/30/2007 10:27:35 AM Content-Type: multipart/alternative; boundary="=_alternative 004F6B9A85257328_=" X-Miltered: at discorde with ID 46ADF55C.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; polakow:01 polakow:01 val:01 rephrase:01 isomorphism:01 deduced:01 wikipedia:01 wikipedia:01 wiki:01 val:01 rephrase:01 isomorphism:01 deduced:01 wiki:01 sans-serif:98 This is a multipart message in MIME format. --=_alternative 004F6B9A85257328_= Content-Type: text/plain; charset="US-ASCII" 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. --=_alternative 004F6B9A85257328_= Content-Type: text/html; charset="US-ASCII"
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.
--=_alternative 004F6B9A85257328_=--