From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by sympa.inria.fr (Postfix) with ESMTPS id 4E5E27ED34 for ; Sun, 15 Jul 2012 22:37:53 +0200 (CEST) Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.213.182; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail1-smtp-roc.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.213.182 as permitted sender) identity=mailfrom; client-ip=209.85.213.182; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-yx0-f182.google.com) identity=helo; client-ip=209.85.213.182; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-yx0-f182.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ApoBAA8pA1DRVdW2kGdsb2JhbABEpx+RCwgiAQEBAQkJDRsEI4IgAQEBAwESAiwBGxIEBwEDAQsGBQsNLiIBEQEFAQoSBhMih1sBAwYGnF8JA4wjgnGDdQoZJw1XiHEBBQyKTmaGAgOIS4xwiwSDJT6EHg X-IronPort-AV: E=Sophos;i="4.77,588,1336341600"; d="scan'208";a="166932067" Received: from mail-yx0-f182.google.com ([209.85.213.182]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 15 Jul 2012 22:37:52 +0200 Received: by yenl8 with SMTP id l8so6483904yen.27 for ; Sun, 15 Jul 2012 13:37:51 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=WuKlr6tBNDH17/rkDN0MbsLPS+Izlj/vp+2dm+wbnLk=; b=Bd45QHO9IzI88FWIbNGzRyqKry8ReuFFrWTeCe7tbypu9RAWJ2tnxB0fZlXZ5oUhbF Dk6Xzs3JrL6/+5iwRXAlC7EXzwI87rnuphUFLr9+wFpA2JPB4U87p7XMhm40WhGATxsi Mi4Frf03Abb0FLOwlOzSkwLDjJM6L7Z5hGzsMDj37WqndaPGzyJqDmTa053LmrlVPR3z eltS71wz/iY82AdKRcg+rUp8t7SZsDuGtJCKMtXifcEGu00XGDslkvNurggw9ergamFl Zs8gTAmCgj+4UhQUTP2SJdktmp2qQoOt3ttiR8w67zjWzEmwkJqG2SXyfXVEuFzcOgQO FowQ== Received: by 10.50.77.200 with SMTP id u8mr3884226igw.6.1342384671228; Sun, 15 Jul 2012 13:37:51 -0700 (PDT) MIME-Version: 1.0 Received: by 10.50.94.39 with HTTP; Sun, 15 Jul 2012 13:37:10 -0700 (PDT) In-Reply-To: <1342378720.56667.YahooMailNeo@web111507.mail.gq1.yahoo.com> References: <1342371289.7422.YahooMailNeo@web111511.mail.gq1.yahoo.com> <1342378720.56667.YahooMailNeo@web111507.mail.gq1.yahoo.com> From: Gabriel Scherer Date: Sun, 15 Jul 2012 13:37:10 -0700 Message-ID: To: Dario Teixeira Cc: "caml-list@inria.fr" Content-Type: text/plain; charset=ISO-8859-1 Subject: Re: [Caml-list] GADTs and parsers > In this case the use of polymorphic variants for the type parameter comes > in handy because there is a subtyping relation and the [> ] declaration > allows for useful mixing Precisely, your example does *not* use subtyping (it's easy to see: in OCaml, subtyping is explicit, you have to use (e :> t) casts. If there are none, you're not using subtyping). [> `Link ] is actually a shortcut for something like [ `Link | 'r ], where 'r is a polymorphic row variable that stands for any number of additional cases. So going from [> `Link ] to [> `Link | `Nolink ] is not subtyping, only instantiation of 'r into (`Nolink | 'r2) for a fresh 'r2. So it may be the case that your previous example also could work with the parameter invariant. I haven't looked at it deeply enough to tell. On Sun, Jul 15, 2012 at 11:58 AM, Dario Teixeira wrote: > Hi, > > And thanks for the prompt reply! > >> I suspect the problem may be one of variance: you are using > >> polymorphic variants, but implicitly assuming that ([ `Nolink ] >> inline_t) is a subtype of ([ `Nolink | `Link ] inline_t), which means >> that "inline_t" is covariant in its first parameter. However, variance >> of GADTs is currently very strict, and your inline_t definition is in >> fact considered invariant (to check that, replace "type _ inline_t" by >> "type (+'a) inline_t" and watch the error), so this conversion does >> not pass. On the contrary, with a phantom type definition, the >> parameter is inferred to be irrelevant (any variance is accepted), so >> you can do whatever you want inside the abstraction boundary. > > Ah, indeed. And on a related note: is there a way to get the compiler > to spill out the variance it infers? I'm assuming that 'ocamlc -i' does > not include inferred variance because it is generally "obvious" and > not something you usually have to worry about unless you want to > make a type abstract. However, in a case like this it would help. > (Or does the compiler *always* assume invariance with GADTs?) > > >> (For more information on GADTs and variance, see the previous thread >> on this on the mailing-list; the summary is that it's complicated, but >> I still hope we could get something finer in the future. It would >> probably not work with polymorphic variant instances, anyway.) > > In this case the use of polymorphic variants for the type parameter comes > in handy because there is a subtyping relation and the [> ] declaration > allows for useful mixing: > > # let x1 = Text "ola";; > val x1 : [> `Nonlink ] inline_t = Text "ola" > > # let x2 = Link "lnk";; > val x2 : [> `Link ] inline_t = Link "lnk" > > # let xs = [x1; x2];; > val xs : [> `Link | `Nonlink ] inline_t list = [Text "ola"; Link "lnk"] > > Cheers, > Dario