From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q46FgM2L002390 for ; Sun, 6 May 2012 17:42:22 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AuIBAOiapk/ZSMDqgGdsb2JhbABEsmsiAQELCwsFFgMkggwBAQQBOj8FCwshJQ8BBA0bIROHfwEDBgkHr0kfKw2JU4oXhwgElw+EUoVch24 X-IronPort-AV: E=Sophos;i="4.75,539,1330902000"; d="scan'208";a="142743923" Received: from fmmailgate03.web.de ([217.72.192.234]) by mail4-smtp-sop.national.inria.fr with ESMTP; 06 May 2012 17:42:17 +0200 Received: from moweb002.kundenserver.de (moweb002.kundenserver.de [172.19.20.108]) by fmmailgate03.web.de (Postfix) with ESMTP id 9C4AD1B4639B6 for ; Sun, 6 May 2012 17:42:16 +0200 (CEST) Received: from frosties.localnet ([95.208.118.96]) by smtp.web.de (mrweb002) with ESMTPA (Nemesis) id 0McWXI-1SiiyW1Sim-00HhJ9; Sun, 06 May 2012 17:42:16 +0200 Received: from mrvn by frosties.localnet with local (Exim 4.77) (envelope-from ) id 1SR3bD-0000Xv-Rx; Sun, 06 May 2012 17:42:15 +0200 From: Goswin von Brederlow To: Gabriel Scherer Cc: Goswin von Brederlow , caml-list@inria.fr References: <87sjfd31z9.fsf@frosties.localnet> Date: Sun, 06 May 2012 17:42:15 +0200 In-Reply-To: (Gabriel Scherer's message of "Sun, 6 May 2012 15:11:37 +0200") Message-ID: <8762c9co4o.fsf@frosties.localnet> User-Agent: Gnus/5.110009 (No Gnus v0.9) XEmacs/21.4.22 (linux, no MULE) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Provags-ID: V02:K0:QXEDB4Nmd2HN/tgus0KO/28jTFUkMKpUVp1kObeXoJZ Yb0ihMEp6NILCYRRJ2MFtqM4fKUUbElz+9jNWG97DUfsy20guD zEWtA2nbxjC5esa4cJyuoirKgCLtfZGP/6+NT+TT/lbcfL2slW 1u+mTGycOOYh7QcFDTeYrW6emkpk00rr6vqzfVVlaAtbB1940/ oBeEiZpyrRaWl6WuzkC7A== Subject: Re: [Caml-list] Implementation for a (nearly) typesafe shallow option type and a compiler bug? Gabriel Scherer writes: > What you observe is the so-called "strengthening" of type equalities > in functor applications. See papers 5 or 6 in this list: > http://caml.inria.fr/about/papers.en.html > > It is not a bug, but a feature: you can write functors F such that > applying F(X) twice yields compatible, rather than incompatible, > types. If you want to recover incompatible types, you can seal the > functor result as you did in your workaround, or pass a non-path > functor expression (that behave in a more generative way): F(struct > include X end). Good to know. I found that surprising. I think it is bad that you can't specify the type of the functor so that both compatible and incompatible types would be an option. Just like you can use 'a, +'a and -'a to fine tune variance in types there could be some syntax to make the functor type strengthened or not. > On your more general code: > - I do not understand why you specify the abstract type ('a t) to be > contravariant, and I suspect this will be unsound (is an (< m : int > > t) also an (< m : int; s : string > t)?) Left over from trying to make the functor type not strengthened. > - I am not sure using (Obj.magic (ref 0)) is safe wrt. types whose > representation is not always a pointer (ie. floats) (Obj.magic (ref 0)) is always a pointer that is unique to the instance of the functor. No other value can legally have this bit pattern. As for floats: Manual 18.3.1 Atomic types Caml type Encoding float Blocks with tag Double_tag. A float is always a pointer and that can't be legally pointing to our (Obj.magic (ref 0)). MfG Goswin