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=1.0 required=5.0 tests=AWL,SPF_NEUTRAL 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 4858ABC69 for ; Sun, 29 Jul 2007 22:06:57 +0200 (CEST) Received: from nf-out-0910.google.com (nf-out-0910.google.com [64.233.182.191]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l6TK6uMC017629 for ; Sun, 29 Jul 2007 22:06:56 +0200 Received: by nf-out-0910.google.com with SMTP id e27so118386nfd for ; Sun, 29 Jul 2007 13:06:56 -0700 (PDT) DKIM-Signature: a=rsa-sha1; c=relaxed/relaxed; d=gmail.com; s=beta; h=domainkey-signature:received:received:message-id:date:from:user-agent:mime-version:to:subject:references:in-reply-to:content-type:content-transfer-encoding:sender; b=OYmnHYgLq5pCBqV9msNRIAKOa5VZHWbKPWoCO2wMaABNJjf9b3mC1LaL+Qv3v/1/H54eWCGx6IN0RDJl5yDxrBUR5WZYAdUWoa9IsrQpaiWhyOGuc9m4EdRVYV3l0uTnmPKFAmwZPyg3RlbwNHMLaoC6n9IIBwvjxS95Knrjr2M= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:user-agent:mime-version:to:subject:references:in-reply-to:content-type:content-transfer-encoding:sender; b=nxiWEwiy27zr/J8K7M9m1Xx4uJlgCZ5g8SyiuBNmVo2UmruG8NkuAYVr9kACmrkppnNjPZdhAxVQiqJ9QEbRoAbP5xh1Ifbo4yxdUW8e8Vucjf8coNCaxuDO2nB5lc52z4U6p1ojwdbgBuVwLt7QDH7RElKdySEuMD4VLGxE2PQ= Received: by 10.86.59.3 with SMTP id h3mr207986fga.1185739616646; Sun, 29 Jul 2007 13:06:56 -0700 (PDT) Received: from ?192.168.0.2? ( [87.88.165.197]) by mx.google.com with ESMTPS id g8sm10530640muf.2007.07.29.13.06.54 (version=SSLv3 cipher=RC4-MD5); Sun, 29 Jul 2007 13:06:55 -0700 (PDT) Message-ID: <46ACF35F.5070102@lix.polytechnique.fr> Date: Sun, 29 Jul 2007 22:06:55 +0200 From: Arnaud Spiwack User-Agent: Thunderbird 2.0.0.5 (Windows/20070716) MIME-Version: 1.0 To: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Re: Void type? References: <46AC748B.10200@lix.polytechnique.fr> <200707291216.34682.jon@ffconsultancy.com> <46AC7BB8.8050609@gmail.com> <20070729124340.GA18564@furbychan.cocan.org> <46AC8EEF.1040102@gmail.com> <20070729170216.GA8137@furbychan.cocan.org> In-Reply-To: <20070729170216.GA8137@furbychan.cocan.org> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit Sender: Arnaud Spiwack X-Miltered: at discorde with ID 46ACF360.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; lix:01 0200,:01 val:01 rephrase:01 ocaml:01 semantics:01 wrote:01 arnaud:01 arnaud:01 abstract:01 caml-list:01 functions:01 define:02 equivalence:03 programming:03 Richard Jones a écrit : > On Sun, Jul 29, 2007 at 02:58:23PM +0200, Arnaud Spiwack wrote: > >> 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. > > Rich. > Well, I don't really know why to use a void type in OCaml as well, thus my answer may be quite abstract. But when I provide a new type, I give a way to build it and a way to use it. In the case of the void type, there is no way to build an element of that type, but there is a way to use one such element : a void element can be used in place of any type. I don't know if it can come handy (it does in certain cases for dependant type programming in my experience). But it's part of the semantics of the type somehow. It is the function which says "void has no element". It occures to me that it might be needed if you need a void type. One reason why it might be useful, is that it gives an equivalence between the types t -> void and t -> 'a (for any type t). Earlier in this thread it was mentioned that these sort of functions could be a reason to use a void type. Since I have no concrete example in mind, I won't be able to be more specific. Still, there is something morally satisfying in being able to define this function without cheating, even if you don't need it. Uh well... then... what is morally satisfying is really a matter of tastes, I guess. Arnaud Spiwack