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 72CA7BC69 for ; Sun, 29 Jul 2007 14:58:26 +0200 (CEST) Received: from ug-out-1314.google.com (ug-out-1314.google.com [66.249.92.169]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l6TCwP1k011488 for ; Sun, 29 Jul 2007 14:58:26 +0200 Received: by ug-out-1314.google.com with SMTP id o2so917461uge for ; Sun, 29 Jul 2007 05:58:25 -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; b=QhBKxzLW+zKJ1rsBsME4QAXobyqSa003/waLtU20W/rBvBmdNHzAf5gJ+XoHb3gZBLKY4zzeyUNZq0QIcNWX7cYWPCLnIRiLRkMVA4+BSYrZhbUPXe0W9U/hYLEeXokxYZLw8CjVh/4OFLTHCjoFWssq+mtrCT9k0VOW7YqWOXI= 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; b=I6hqqdCFmYf1PNIwGavfLKwseu9iHknWl/gZ0EitYWyHWwm0QdtTlt9VX/qRY0+teEeWzyubdODQ+1sxfkpl52zwyFSnTDLbJ6Nl+WFjPv4yac4jNYBSDKu1F/4ucWYRaPvUTWETe8PM0FrHHNNgOWo/4YJjb6MUQ8HNXkop3ks= Received: by 10.86.57.9 with SMTP id f9mr3200064fga.1185713905698; Sun, 29 Jul 2007 05:58:25 -0700 (PDT) Received: from ?192.168.0.2? ( [87.88.165.197]) by mx.google.com with ESMTPS id y2sm8969924mug.2007.07.29.05.58.23 (version=SSLv3 cipher=RC4-MD5); Sun, 29 Jul 2007 05:58:24 -0700 (PDT) Message-ID: <46AC8EEF.1040102@gmail.com> Date: Sun, 29 Jul 2007 14:58:23 +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> In-Reply-To: <20070729124340.GA18564@furbychan.cocan.org> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit X-j-chkmail-Score: MSGID : 46AC8EF1.000 on discorde : j-chkmail score : X : 0/20 1 0.000 -> 1 X-Miltered: at discorde with ID 46AC8EF1.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; val:01 val:01 0200,:01 syntax:01 syntax:01 ocaml:01 failwith:01 failwith:01 wrote:01 wrote:01 arnaud:01 arnaud:01 rec:01 assert:01 caml-list:01 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 = Of course there are various ways to get the same for void2 : # let void2_elim1 (x:void2) = assert false;; val void2_elim1 : void2 -> 'a = # let rec void2_elim2 (x:void2) = void2_elim2 x;; val void2_elim2 : void2 -> 'a = # let void2_elim3 (x:void2) = Obj.magic x;; val void2_elim3 : void2 -> 'a = But none of these are really functional/well typed except maybe void2_elim2 but it looks like cheating. Of course these are all safe because void has no closed instance. But I'd consider void1 to be morally much more satisfying. It really contains the essence of what a void type should be. Arnaud Spiwack Richard Jones a écrit : > On Sun, Jul 29, 2007 at 01:36:24PM +0200, Arnaud Spiwack wrote: > >> Jon Harrop a écrit : >> >>> On Sunday 29 July 2007 12:05:47 Arnaud Spiwack wrote: >>> >>> >>>> It is the good solution if you work with the original syntax (and it's >>>> absolutely equivalent to the dual definition in term of empty variant >>>> which you can write in the revised syntax). >>>> >>>> >>> I don't quite understand this "empty variant from the revised syntax >>> thing". How is: >>> >>> type void >>> >>> not an empty variant? >>> >>> >>> >> Well, not technically I believe. It's a type with no definition. I >> wouldn't be adamant about that but I reckon it's not considered as a sum >> type by OCaml type system. >> Plus you cannot write the empty matching : >> match x with [] >> in the original syntax, preventing you from writing a function of type >> void -> 'a without using exceptions or Obj.magic or an obviously >> looping function or such. >> >> Thus it does not really have the logical behavior of an empty variant. >> > > Can you explain what you mean a bit more? > > type void1 = { v: 'a. 'a };; > let f (_ : void1) = 1;; > --> val f : void1 -> int = > let f () : void1 = failwith "error";; > --> val f : unit -> void1 = > > type void2;; > let f (_ : void2) = 1;; > --> val f : void2 -> int = > let f () : void2 = failwith "error";; > --> val f : unit -> void2 = > > They seem to be fairly similar to me. > > Rich. > >