From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <arnaud.spiwack@gmail.com>
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 A7ABDBC69
	for <caml-list@yquem.inria.fr>; Sun, 29 Jul 2007 13:05:56 +0200 (CEST)
Received: from nf-out-0910.google.com (nf-out-0910.google.com [64.233.182.189])
	by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l6TB5t9n026102
	for <caml-list@inria.fr>; Sun, 29 Jul 2007 13:05:56 +0200
Received: by nf-out-0910.google.com with SMTP id g13so142101nfb
        for <caml-list@inria.fr>; Sun, 29 Jul 2007 04:05:55 -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=jljZcc0Efp7DL4fjT8x9tcv7O50D/ZzKpw5/1QazGgMSn2ss4tiOC6AxZje8vi/zgmEdExPbLY0ot0VbpD6lLFL/tCXskNvf39hQgjO8Lvovlu37EMAn6VikzL72GBampCXV7Io8xYf/y0HTqJUd9qZ8PELP25SbyMezKAZchUI=
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=mbMrbwTf+Jo62FC+D2kL1+xUwXeVyEFy+tGcbvRXpITM8t7ZUaE5pvZsB7fKNVl9vfWGxkVZh4Z4xZX7sB2PacPLF5PcyJfzPrKdKw+Xwf445u+heqHfkiS1Bqavb4/TWIR63gAdOGZNg5YQk8KSUJqQ/34xtqv53kbhpwgl3do=
Received: by 10.86.80.5 with SMTP id d5mr3131453fgb.1185707155256;
        Sun, 29 Jul 2007 04:05:55 -0700 (PDT)
Received: from ?192.168.0.2? ( [87.88.165.197])
        by mx.google.com with ESMTPS id g1sm8509904muf.2007.07.29.04.05.48
        (version=SSLv3 cipher=RC4-MD5);
        Sun, 29 Jul 2007 04:05:48 -0700 (PDT)
Message-ID: <46AC748B.10200@lix.polytechnique.fr>
Date: Sun, 29 Jul 2007 13:05:47 +0200
From: Arnaud Spiwack <aspiwack@lix.polytechnique.fr>
User-Agent: Thunderbird 2.0.0.5 (Windows/20070716)
MIME-Version: 1.0
To: Caml List <caml-list@inria.fr>
Subject: Re: [Caml-list] Re: Void type?
References: <jwvvec5dv32.fsf-monnier+gmane.comp.lang.caml.inria@gnu.org>	<6h3rn4-uu7.ln1@mantle.rutgers.edu>	<61777.84.165.172.53.1185610925.squirrel@www.ps.uni-sb.de> <sqotn4-cgd.ln1@mantle.rutgers.edu>
In-Reply-To: <sqotn4-cgd.ln1@mantle.rutgers.edu>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Sender: Arnaud Spiwack <arnaud.spiwack@gmail.com>
X-Miltered: at discorde with ID 46AC7493.001 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)!
X-Spam: no; 0.00; lix:01 forall:01 syntax:01 syntax:01 arnaud:01 arnaud:01 rec:01 caml-list:01 variant:02 revised:02 let:03 let:03 void:06 void:06 spotted:07 


> What about:
>
>     # type void = { v: 'a. 'a };;
>     type void = { v : 'a. 'a; }
>     # let rec vv = { v = vv };;
>     This field value has type 'a which is less general than 'b. 'b
>   
Now that's a very nice solution. You give the impredicative coding of 
the void type (forall 'a. 'a) by boxing it into record type.

You get void_elim withouth cheating :
  let void_elim x = x.v

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).

Well spotted.


Arnaud Spiwack