From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 2C6CFBBAF for ; Fri, 21 May 2010 18:02:46 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ag8BAM9L9kvUTWUIkGdsb2JhbACDGIJimCYVAQEBAQkJDAcRBB6sfZB4gSWDA2oE X-IronPort-AV: E=Sophos;i="4.53,279,1272837600"; d="scan'208";a="51622662" Received: from mx4.wp.pl ([212.77.101.8]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 21 May 2010 18:02:45 +0200 Received: (wp-smtpd smtp.wp.pl 3099 invoked from network); 21 May 2010 18:02:40 +0200 Received: from pfpleia.if.uj.edu.pl (HELO [149.156.90.26]) (d0@[149.156.90.26]) (envelope-sender ) by smtp.wp.pl (WP-SMTPD) with AES256-SHA encrypted SMTP for ; 21 May 2010 18:02:40 +0200 Message-ID: <4BF6AE25.2040901@wp.pl> Date: Fri, 21 May 2010 18:00:37 +0200 From: Dawid Toton User-Agent: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.1.9) Gecko/20100423 Thunderbird/3.0.4 MIME-Version: 1.0 To: caml-list Subject: Re: Binding and evaluation order in module/type/value languages References: <4BF196F3.5050508@wp.pl> <20100518.123313.173589671.garrigue@math.nagoya-u.ac.jp> In-Reply-To: <20100518.123313.173589671.garrigue@math.nagoya-u.ac.jp> Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit X-WP-AV: skaner antywirusowy poczty Wirtualnej Polski S. A. X-WP-SPAM: NO 0000000 [UTNk] X-Spam: no; 0.00; semantics:01 ocaml:01 compiler:01 unify:01 compiler:01 unification:01 unify:01 sml:01 avoids:01 incompatible:01 defined:02 binding:02 module:03 languages:03 types:05 > It is not clear that this will work at all. > The semantics of ocaml (contrary to SML) is not defined in terms of > type generativity. > > This is great eureka to me. I thought that when the compiler refuses to unify some types it knows that they are incompatible (as the error message says). But now I think (as I currently understand non-generativity) that sometimes the compiler simply doesn't know if some types are equal and avoids unification of such types. The error message should be instead: "Cannot unify the following types, because I don't have any proof that they are equal (and I don't have looked for the proof really hard)..." So in order to have not unifiable phantom types one has to kind of trick the compiler and hide the fact that they are equal. Dawid