From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id AB9707ED11 for ; Sun, 18 Sep 2016 10:17:39 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=paurkedal@gmail.com; spf=Pass smtp.mailfrom=paurkedal@gmail.com; spf=None smtp.helo=postmaster@mail-oi0-f41.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of paurkedal@gmail.com) identity=pra; client-ip=209.85.218.41; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="paurkedal@gmail.com"; x-sender="paurkedal@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of paurkedal@gmail.com designates 209.85.218.41 as permitted sender) identity=mailfrom; client-ip=209.85.218.41; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="paurkedal@gmail.com"; x-sender="paurkedal@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-oi0-f41.google.com) identity=helo; client-ip=209.85.218.41; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="paurkedal@gmail.com"; x-sender="postmaster@mail-oi0-f41.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3A90H7aBbAVzHq3NUxlx6Ws1n/LSx+4OfEezUN459i?= =?us-ascii?q?sYplN5qZpMy+bnLW6fgltlLVR4KTs6sC0LuP9fC4EjZfuN7B6ClEK80UEUddyI?= =?us-ascii?q?0/pE8JOIa9E0r1LfrnPWQRPf9pcxtbxUy9KlVfA83kZlff8TWY5D8WHQjjZ0Iu?= =?us-ascii?q?frymUrDbg8n/7e2u4ZqbO1wO32vkJ+MqZ0/p9E2R7pBQ2to6bP5pi1PgmThhQ6?= =?us-ascii?q?xu32RmJFaezV7Xx/yb29pdyRlWoO8r7MVaUK/3LOwSRL1cCyk6YShuvJW4/TGK?= =?us-ascii?q?dwaE52MdX2MKiVIIRlGdtFCpFqv25w7zrOlgw2G/OtHqSfhgXD247LpwDhrvlD?= =?us-ascii?q?sDHzE8+WDTzMd3ifQIjgimokk1+4PIfIyPfNM4Np7Hft4WTG4LFpJJXjFbAY6w?= =?us-ascii?q?Zo8nAO8IPOIepI748Qhd5SCiDBWhUbu8ggRDgWX7iOhji7ws?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BQAAAtTN5XfynaVdFdGgEBAQECAQEBA?= =?us-ascii?q?QgBAQEBFgEBAQMBAQEJAQEBgw8BAQEBAXVtDweNLKs9ggMghX4CgTAHOBQBAQE?= =?us-ascii?q?BAQEBAQEBARIBAQkLCwkXMYIyBAEVAQSCEAEBAQMBEhEEGQEbHQEDAQsGBQsNA?= =?us-ascii?q?gImAgIhAQERAQUBHAYTGweIDQEDDwinbIEyPjKLPYFrgl8Fg1gKGScNVIJTAQE?= =?us-ascii?q?BAQEFAQEBARsCAQUQdooFgkeEf4JaAQSZOjUBhiWGRoJwj2qEWIN9hA+CORMeg?= =?us-ascii?q?REegyiBejw0hXeBQAEBAQ?= X-IPAS-Result: =?us-ascii?q?A0BQAAAtTN5XfynaVdFdGgEBAQECAQEBAQgBAQEBFgEBAQM?= =?us-ascii?q?BAQEJAQEBgw8BAQEBAXVtDweNLKs9ggMghX4CgTAHOBQBAQEBAQEBAQEBARIBA?= =?us-ascii?q?QkLCwkXMYIyBAEVAQSCEAEBAQMBEhEEGQEbHQEDAQsGBQsNAgImAgIhAQERAQU?= =?us-ascii?q?BHAYTGweIDQEDDwinbIEyPjKLPYFrgl8Fg1gKGScNVIJTAQEBAQEFAQEBARsCA?= =?us-ascii?q?QUQdooFgkeEf4JaAQSZOjUBhiWGRoJwj2qEWIN9hA+CORMegREegyiBejw0hXe?= =?us-ascii?q?BQAEBAQ?= X-IronPort-AV: E=Sophos;i="5.30,355,1470693600"; d="scan'208";a="193803046" Received: from mail-oi0-f41.google.com ([209.85.218.41]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 18 Sep 2016 10:17:38 +0200 Received: by mail-oi0-f41.google.com with SMTP id w11so157287248oia.2 for ; Sun, 18 Sep 2016 01:17:38 -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; bh=/Swud1BZWde0L8y3Fl9/NBPg5LqE1NiSnjkS7buVyWw=; b=Mto+PLlIlN9LzaTDNMeLShBiWrhCVKdmchf4LXXsjKBF+MaDyBsboFfIUGqWEDSjRv WqXbbkp/epBDSEf3TubhIB0WvaUIcDXV4UpBBUql67X1lMtfUohevvihYAM1H9Ktz8EV /ogGmNGi5XMMWfiWvKi4BR5xNZ2VT5g4D/6cxHfW9RIOyI+OT/JRHVAJrSCfx3bDIEz3 FiQtlMfyjRjho51wooeEF4+zeT+Wai2CVEAogYxdpFe0bPMoREzs1Rt309H9IXsp3b35 uXPB0dnLhHzsKidXt4F6gxA0GNPdowLjzJqTK+Eq82A1tWEM6RgxN8NWX4UvebpDr/RT GQRw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc; bh=/Swud1BZWde0L8y3Fl9/NBPg5LqE1NiSnjkS7buVyWw=; b=LZUPvECrjX+ZUEzAxU1La3lwsKTEeXcr9HWmDPMQRu8vkxOQxGB7xNof9pqZ+UFKLT wbjWRIQ7bDhqXhynXLRV5XNHnE/MrkICEBflFiUO0+EWJgKxRUpXMntwj09gU7lutVE9 ZvhJjnaWlyGsYaBmyCiBp1W1wa4HemUKvOVO0qgzoTZc8so4AeuHdwc46KCTolkkRUYi 9sqZbwffUq8Bp3SETr0LCZaYMXIlpA6TT7Tf1vHqCYf/d6115xSWME959zT1O1SSzLZl E8O3G/cCHsDfGfw0y8eGQsfeYdM/7UxpePYFBuHxWoHa6XVBTlAcAxMg2Rh+Ktlv28Oc M0gA== X-Gm-Message-State: AE9vXwPq4M1amyzv0vWFAfNG/2eh0UT96sICNLeap8H01fRkicWjoo8IUF/Fojsb/jNaLxsRSDvi4eT0tD4gmg== X-Received: by 10.202.175.75 with SMTP id y72mr12692760oie.8.1474186657352; Sun, 18 Sep 2016 01:17:37 -0700 (PDT) MIME-Version: 1.0 Received: by 10.202.228.21 with HTTP; Sun, 18 Sep 2016 01:17:36 -0700 (PDT) In-Reply-To: References: From: "Petter A. Urkedal" Date: Sun, 18 Sep 2016 10:17:36 +0200 Message-ID: To: Markus Mottl Cc: OCaml List Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] Covariant GADTs Hi Markus, On 17 September 2016 at 19:38, Markus Mottl wrote: > Hi, > > GADTs currently do not allow for variance annotations so I wondered > whether there are any workarounds for what I want: > > ----- > type +_ t = > | Z : [ `z ] t > | S : [ `z | `s ] t -> [ `s ] t > > let get_next (s : [ `s ] t) = > match s with > | S next -> next > ----- > > The above compiles without the variance annotation, but then you > cannot express "S Z", because there is no way to coerce Z to be of > type [`z | `s] t. > > Another approach I tried is the following: > > ----- > type _ t = > | Z : [ `z ] t > | S : [< `z | `s ] t -> [ `s ] t > > let get_next (s : [ `s ] t) : [< `z | `s ] t = > match s with > | S next -> next > ----- > > The above gives the confusing error: > > ----- > Error: This expression has type [< `s | `z ] t > but an expression was expected of type [< `s | `z ] t > The type constructor $S would escape its scope > ----- > > There are apparently two type variables associated with [< `s | `z ] > t: the locally existential one introduced by matching the GADT, and > the one in the type restriction of the function, but the compiler > cannot figure out that these can be safely unified. There is > currently no way of specifying locally abstract types that have type > constraints, which could possibly also help here. In this case, you can supply the needed type information to `get_next` with structural type matching: type _ t = Z : [`z] t | S : 'a t -> [`s of 'a] t let get_next : [`s of 'a] t -> 'a t = function S next -> next This gives you a richer type which also allows defining get_next_pair, etc. > Are there workarounds to achieve the above? Are there any plans to > add variance annotations for GADTs? I had a similar problem myself and found a paper [1] explaining the issue and a possible solution. Haven't really studied it, but as I understand the issue is that the current GADTs only introduce type equality, which is too strict to verify variance. What is needed is more like (my ASCIIfication) type +'a t = | Z when 'a >= [`z] | S when 'a >= [`s] of [< `z | `s] t allowing 'a in each case to be a supertype rather than equal to the specified type. In that spirit, I tried type +_ t = | Z : [> `z] t | S : [< `s | `z] t -> [> `s] t;; but that does not check for variance either. Best, Petter [1] https://arxiv.org/abs/1301.2903