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.8 required=5.0 tests=AWL,DNS_FROM_RFC_POST, 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 mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id 2B05EBB84 for ; Thu, 14 Aug 2008 13:23:00 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AsUDALCyo0jAXQIniGdsb2JhbACRPz4BAQEPIJx+hwEBAg X-IronPort-AV: E=Sophos;i="4.32,209,1217800800"; d="scan'208";a="16113185" Received: from concorde.inria.fr ([192.93.2.39]) by mail1-smtp-roc.national.inria.fr with ESMTP; 14 Aug 2008 13:22:59 +0200 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id m7EBMxGc009419 for ; Thu, 14 Aug 2008 13:22:59 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Am8BAMCxo0jRVcbulGdsb2JhbACRPz4BAQEBCQMKBxEDnH2HAAEC X-IronPort-AV: E=Sophos;i="4.32,209,1217800800"; d="scan'208";a="13988772" Received: from rv-out-0506.google.com ([209.85.198.238]) by mail2-smtp-roc.national.inria.fr with ESMTP; 14 Aug 2008 13:21:43 +0200 Received: by rv-out-0506.google.com with SMTP id k40so330345rvb.57 for ; Thu, 14 Aug 2008 04:21:42 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:message-id:date:from:to :subject:cc:in-reply-to:mime-version:content-type :content-transfer-encoding:content-disposition:references; bh=4gC9X0Kqhgw6Y+NcpqBVN5ulfVbNomgu/gBARFNCylc=; b=tKIh1jvIHjmKdwuS6ZRcwkxXRjCF64sxiKC5UbY1ejIkO5Z1ISMpTwhwGqvqBRMPz9 PuCpbsrWK3U5c4EC3AOlkdVOvwMRgb/AIEeNRFF2lDE/XOriJmMskehMKwE5CTBwsA6m GuyAcjeR+2fnRjyLxLi+RL15IzStQdr7iZbYM= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:cc:in-reply-to:mime-version :content-type:content-transfer-encoding:content-disposition :references; b=A1OI3VGulsGbTxV0bD5TumtibTzbwCBDCcA7XU13nNEkXCVtEMisMpSWVzWud7wIHX Qa6uiEQaJWno5YPu0JX/5McEWXKAZ4V3DgcarO6UV+LCQRS1zscGSduldOQG8RZzKpom MVdA43Fo2Uu/mLF27zEVUZcapjDAQhopj0Bf8= Received: by 10.141.69.1 with SMTP id w1mr550050rvk.147.1218712902598; Thu, 14 Aug 2008 04:21:42 -0700 (PDT) Received: by 10.140.126.17 with HTTP; Thu, 14 Aug 2008 04:21:42 -0700 (PDT) Message-ID: <4a708d20808140421q29be872dwca7c214587d4797d@mail.gmail.com> Date: Thu, 14 Aug 2008 13:21:42 +0200 From: "Lukasz Stafiniak" To: "Jacques Carette" Subject: Re: [Caml-list] Why is this coercion necessary? Cc: caml-list@inria.fr In-Reply-To: <48A395FA.2050704@mcmaster.ca> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline References: <48A395FA.2050704@mcmaster.ca> X-Miltered: at concorde with ID 48A41593.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; lukasz:01 coercions:01 ocaml:01 inference:01 subtyping:01 unification:01 intersection:01 syntax:01 coerced:01 'n':01 intersection:01 type-checker:01 coercions:01 polluting:01 'recursive:01 There is no way to avoid coercions altogether: OCaml doesn't have inference for subtyping, using unification with row variables gives the intersection behavior. But the language could be changed, with a syntax like match x return e with | ... -> ... | ... -> ... meaning that all branches should be coerced to e. On Thu, Aug 14, 2008 at 4:18 AM, Jacques Carette wrote: > Here is a much simplified version from a (much) larger problem I have > recently encountered: > > type 'a a = [`A of 'a b] > and 'a b = [`B of 'a a] > and 'a c = [`C ] > > type 'a d = [ 'a a | 'a b | 'a c] > type e = e d > > # this code gives an error (details below) > let f1 (x:e) : e = match x with > | `A n -> n > | `B n -> n > | `C -> `C > > # this works > let f2 (x:e) : e = match x with > | `A n -> (n :> e) > | `B n -> (n :> e) > | `C -> `C > > f1 gives an error on the "| `B n -> n" line, pointing to the second 'n' > with > This expression has type e a but is used with type e b > These two variant types have no intersection > > Indeed, they have no intersection, but they have a union! That is what it > seems the coercion in f2 'forces' the type-checker to realize, and all works > fine. But of course, such coercions end up polluting my code all over the > place (since the actual example is made of 9 types with 20 tags in total, > and the 'recursive knot' requires 2 parameters to close properly). > > So, is this a bug? Is there a way to avoid these coercions? > > Jacques > > _______________________________________________ > Caml-list mailing list. Subscription management: > http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs >