From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTP id D76955D4 for ; Fri, 15 Jun 2018 15:21:34 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.51,227,1526335200"; d="scan'208,217";a="332006030" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 15 Jun 2018 17:21:33 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id DEA2D82496; Fri, 15 Jun 2018 17:21:32 +0200 (CEST) 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 84E9D82416 for ; Fri, 15 Jun 2018 17:21:25 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=markus.mottl@gmail.com; spf=Pass smtp.mailfrom=markus.mottl@gmail.com; spf=None smtp.helo=postmaster@mail-ua0-f172.google.com IronPort-PHdr: =?us-ascii?q?9a23=3AemhFCxyLrkkAJZrXCy+O+j09IxM/srCxBDY+r6Qd?= =?us-ascii?q?2+seIJqq85mqBkHD//Il1AaPAd2Graocw8Pt8InYEVQa5piAtH1QOLdtbDQizf?= =?us-ascii?q?ssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1?= =?us-ascii?q?JuPoEYLOksi7ze+/94HTbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeu?= =?us-ascii?q?BWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbO?= =?us-ascii?q?SxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDtU7s6RSqt4LtqSB/wiS?= =?us-ascii?q?cIKTg58H3MisdtiK5XuQ+tqwBjz4LRZoyeKfhwcb7Hfd4CSmVBUMReWSxPDI2/?= =?us-ascii?q?coUBEfYOMP1CoIXhvVYDtweyCRWuCe7p1zRGhmX23ao/0+k5Fg/JxhYgH9ETsH?= =?us-ascii?q?TPsd77M6ASUfypzKnM0D7OaPZW1i3n6IjLbxAhuuuAXbd3ccrN1UkvExjIjlqV?= =?us-ascii?q?qYP/PjOV0v4BvHSc7+plTO+ijXMspQ92ojiq3Mgsi4/Ji5oSyl/Y7yp5xYI1Kc?= =?us-ascii?q?e5SE59b96kF51dvDyZOYtuWs4uXX1ktSIgxrAFuZO3ZjYGxIklyhLFdvCKcZaE?= =?us-ascii?q?7xT+X+iLOzh4nmhqeLenihay70egzur8W9Gx0FlQrypFlsDAtm0X2BDP88SHRO?= =?us-ascii?q?Zx80W/1TqV2ADT7eZEIU8wlaXFMZIu3rkwlp8LvUTCGC/5hln2gbeIekk4/uWk?= =?us-ascii?q?8efqb7X8qpOCKoN5iBvyPrksl8ChGeg4NxIBX2mf+eSyzr3j+kj5Ta1PjvIsiK?= =?us-ascii?q?nZs43aJd8Bqq68BA9Vzpoj6xKkAjep1dQXh3gHLFZfdB2biIjpPknCIOrkAven?= =?us-ascii?q?n1SsjDBryujaMbL7B5XNKmHPkLPgfbZm905R0xEzzNBa55JMEL4NOvPzWknrtN?= =?us-ascii?q?zZFBA1KQK0w/y0QOl6g6oaUGTHOaSZNaLOrRfc7+YmJa+Xb48QuSrhA+Ai4+/y?= =?us-ascii?q?gHQ5n14EYKTv2oEYPiOWBPNjdmCQe3nxmZ8kFnsWukJqSeXwi0CZFztUe2q2d6?= =?us-ascii?q?057zA/TomhCNGQFciWnLWd0XLjTdVtbWdcBwXJSC+wLtTWa7I3cCuXZ/RZvHkB?= =?us-ascii?q?XLmlRZUm0Ej35gD/wrtjaOHT/39B7M6x5J1O/+TW0CoK23lsFc3EijOCSmh1mi?= =?us-ascii?q?UDQDpkhPki83w48U+K1O1Du9IdFdFX4KkXAAIzNJqZ0uUiTt6rBViHcdCOR1Kr?= =?us-ascii?q?BN6hBGNpQw=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0ATAwCl2CNbh6zZVdFbHQEBBQELAYNsP?= =?us-ascii?q?n8og3mBHYJQkGmBf5ZnCxuEUQKCUhkHAQQ0FAECAQEBAQEBAQEBEwEBAQgNCQg?= =?us-ascii?q?pIwyCNSQBgk8BBAEjBBkBFAcdAQMBCwYDAgQHNwICIQEBEQEFARwGEwiDGgKBZ?= =?us-ascii?q?gEDDQiOE5ADPIsIgWkWBQEXgnIFg00KGSYNVVeBYAIGEog6gVQ/hBuCUYUlglU?= =?us-ascii?q?Ch1eRCywHAoFqihCDB404ilmGWQ8hgTeBczMaI1AxghIJggwag06CWYgVIzCQW?= =?us-ascii?q?QEB?= X-IPAS-Result: =?us-ascii?q?A0ATAwCl2CNbh6zZVdFbHQEBBQELAYNsPn8og3mBHYJQkGm?= =?us-ascii?q?Bf5ZnCxuEUQKCUhkHAQQ0FAECAQEBAQEBAQEBEwEBAQgNCQgpIwyCNSQBgk8BB?= =?us-ascii?q?AEjBBkBFAcdAQMBCwYDAgQHNwICIQEBEQEFARwGEwiDGgKBZgEDDQiOE5ADPIs?= =?us-ascii?q?IgWkWBQEXgnIFg00KGSYNVVeBYAIGEog6gVQ/hBuCUYUlglUCh1eRCywHAoFqi?= =?us-ascii?q?hCDB404ilmGWQ8hgTeBczMaI1AxghIJggwag06CWYgVIzCQWQEB?= X-IronPort-AV: E=Sophos;i="5.51,227,1526335200"; d="scan'208,217";a="268939508" Received: from mail-ua0-f172.google.com ([209.85.217.172]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 15 Jun 2018 17:21:23 +0200 Received: by mail-ua0-f172.google.com with SMTP id n4-v6so6636760uad.6 for ; Fri, 15 Jun 2018 08:21:23 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=D1zVrvusOZ8e3g5unUxNBNIYqrc4PuOT2jVO94FL8wM=; b=E1v6KWp9fYlNkxpCo00w6aW0sbnr6Kokiy8NgptfYU6SCcmkq3YhURIY2bGEcjkEDK ftG3OdKUPNimR/V4MjcYe7TSJZsS8NkmoEwdDyBK/eYEG8B4zHdimC1+ca1pZ6k867TD palq7TJOCPcT/QarfY3RUgsexy/K33GHS/V8wL+Oj9DeUXuctBSN+kD1cN9bS12cKjfh lgZ8AcqB9O2eotP/afDy/pDH2gBHmlx1SbdQagHLLBJn2wwnPcaLQPnmY/DvXBjInwJM O7fIdp4wgv7IEJ1QzJJ1RcMWHWoiT6RaMt/wo+CN01Sj2hw+9N7bg724LzpWjFLjzUQV 6f9g== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc; bh=D1zVrvusOZ8e3g5unUxNBNIYqrc4PuOT2jVO94FL8wM=; b=es8TAgZboWTSGVxqoUugQRLTIwGoRe2iXDbOR2Kl+SSpDALtE7yGPIROQHtHNWAmYt RIbzyXahWRpfs1zaGv+fEASln4BQzKVNpYCuWi08ShD/J/lWUHn6FMV0r3srfaPIefUd aLzCOIllF1RGZyrbwWjQRXem/+xrw2im3vLJ1F+nURuNagfTAyJg0zH7qbI681oR9ekw ic1sl7dS12GJsu8MrnC7d6OaxO1IglV1EJdLkGVvqnqHYN85UvilN0ghn9hqWPtA7utz 0MDxjnilwaoPkrAhbZmemO9lqg4PGphvIuSmk8coYrHrqIgIfcGmWogj8u2DZsCtnG+m hnag== X-Gm-Message-State: APt69E07x1xxOi5250VAltR6qUPnbhRFQtQUUNJhqMHXay+iWehKH2F9 hZAH/bgMANKd0mtL3fOV9Fu/6a2fhzEkkRoK+YCpPALd X-Google-Smtp-Source: ADUXVKKZbwXl5MUeOImNcEDoyafU+cecQo7lFviSnY1F1ak43w0/HY+ojd4Jcge6VOwCyOL79lmGrOzkcqzqM6+6fIo= X-Received: by 2002:ab0:1e41:: with SMTP id n1-v6mr1406361uak.146.1529076082301; Fri, 15 Jun 2018 08:21:22 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Markus Mottl Date: Fri, 15 Jun 2018 11:21:10 -0400 Message-ID: To: Alan Schmitt Cc: OCaml List Content-Type: multipart/alternative; boundary="000000000000b85f43056eafc487" Subject: Re: [Caml-list] a question about GADTs Reply-To: Markus Mottl X-Loop: caml-list@inria.fr X-Sequence: 16942 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: --000000000000b85f43056eafc487 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I don't think that you can currently do this. According to the manual entry for GADTs: "This return type must use the same type constructor as the type being defined, and have the same number of parameters." But I guess it would be a supportable feature to perform type substitutions until the above is satisfied if at all possible. Substituting manually is probably the only thing you can do until then. On Fri, Jun 15, 2018 at 10:35 AM Alan Schmitt < alan.schmitt@polytechnique.org> wrote: > Hello, > > I'm trying to write the following: > > #+begin_src ocaml > type state > type value > type literal > > type (_,_) term =3D > | Skip : (state, state) term > | Const : literal -> (state, value) term > | If : expr * stat * stat -> (state,state) term > and expr =3D (state,value) term > and stat =3D (state,state) term > #+end_src > > and it works well. However I would like to replace the right-hand side > with their abbreviations (stat and expr), and at that point the > typechecker complains. Is there a workaround? > > Thanks, > > Alan > > -- > OpenPGP Key ID : 040D0A3B4ED2E5C7 > Monthly Athmospheric CO=E2=82=82, Mauna Loa Obs. 2018-05: 411.25, 2017-05= : 409.65 > --=20 Markus Mottl http://www.ocaml.info markus.mottl@gmail.com --=20 Caml-list mailing list. Subscription management and archives: https://sympa.inria.fr/sympa/arc/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs= --000000000000b85f43056eafc487 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I don't think that you can currently do this.=C2=A0 Ac= cording to the manual entry for GADTs: "This return type must use the = same type constructor as the type being defined, and have the same number o= f parameters."

But I guess it would be a supportabl= e feature to perform type substitutions until the above is satisfied if at = all possible.=C2=A0 Substituting manually is probably the only thing you ca= n do until then.

On Fri, Jun 15, 2018 at 10:35 AM Alan Schmitt <alan.schmitt@polytechnique.org> wrote:
=
Hello,

I'm trying to write the following:

#+begin_src ocaml
type state
type value
type literal

type (_,_)=C2=A0 term =3D
=C2=A0 | Skip : (state, state) term
=C2=A0 | Const : literal -> (state, value) term
=C2=A0 | If : expr * stat * stat -> (state,state) term
and expr =3D (state,value) term
and stat =3D (state,state) term
#+end_src

and it works well. However I would like to replace the right-hand side
with their abbreviations (stat and expr), and at that point the
typechecker complains. Is there a workaround?

Thanks,

Alan

--
OpenPGP Key ID : 040D0A3B4ED2E5C7
Monthly Athmospheric CO=E2=82=82, Mauna Loa Obs. 2018-05: 411.25, 2017-05: = 409.65


--
Markus Mottl= =C2=A0 =C2=A0 =C2=A0 =C2=A0 http://www.oc= aml.info=C2=A0 =C2=A0 =C2=A0 =C2=A0 markus.mottl@gmail.com
--000000000000b85f43056eafc487--