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 sympa.inria.fr (Postfix) with ESMTPS id 829DE7ED11 for ; Tue, 4 Oct 2016 12:34:29 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=garrigue@math.nagoya-u.ac.jp; spf=None smtp.mailfrom=garrigue@math.nagoya-u.ac.jp; spf=None smtp.helo=postmaster@mailhost.math.nagoya-u.ac.jp Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3A4BxRuB29OnZJqp0SsmDT+DRfVm0co7zxezQtwd8Z?= =?us-ascii?q?segUL/ad9pjvdHbS+e9qxAeQG96KsbQe1KGM4+igATVGusnR9ihaMdRlbFwst4?= =?us-ascii?q?Y/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVIm?= =?us-ascii?q?bsy8IIPZjty22uau4NWTJlwQ3HvuKY91eTC/twbMrYEzhpd+Lu5lzxLToWZTPe?= =?us-ascii?q?FR2X9sDV2Wlhf4oMy3+cgw3T5XvqcD/sVZTKjhN4sxV6ZZAykrezQ67dfxtBbe?= =?us-ascii?q?QCOK72ccFGMfnR1ZCk3YqhjxGJXp5Hip/tFh0TWXaJWlBYs/Xi6vuuIyEEfl?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0ClAABwhfNXlwWCBoVdHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBgxIBAQEBAYFxpDGWLQGGHQKCLxABAQEBAQEBAQEBARIBAQEBAQg?= =?us-ascii?q?WB0iCMgQBFQEEghEBAQQjBBkDATUBAQ4LGAICGA4CAlcGiF+wPGeESQcChHkZg?= =?us-ascii?q?xUBAQEBAQEEAQEBAQEBAQEWAQiBB4cygliER4MEK4IvhkgHiGKKTY90j3KMXRO?= =?us-ascii?q?DfjVrgneBamOGGIFBAQEB?= X-IPAS-Result: =?us-ascii?q?A0ClAABwhfNXlwWCBoVdHAEBBAEBCgEBFwEBBAEBCgEBgxI?= =?us-ascii?q?BAQEBAYFxpDGWLQGGHQKCLxABAQEBAQEBAQEBARIBAQEBAQgWB0iCMgQBFQEEg?= =?us-ascii?q?hEBAQQjBBkDATUBAQ4LGAICGA4CAlcGiF+wPGeESQcChHkZgxUBAQEBAQEEAQE?= =?us-ascii?q?BAQEBAQEWAQiBB4cygliER4MEK4IvhkgHiGKKTY90j3KMXRODfjVrgneBamOGG?= =?us-ascii?q?IFBAQEB?= X-IronPort-AV: E=Sophos;i="5.31,295,1473112800"; d="scan'208";a="239329857" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail2-smtp-roc.national.inria.fr with ESMTP; 04 Oct 2016 12:34:03 +0200 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id A765B63DF for ; Tue, 4 Oct 2016 19:34:01 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (rabbit-172.math.nagoya-u.ac.jp [172.16.254.254]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id B20FC4187; Tue, 4 Oct 2016 19:34:00 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= content-type:mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; s=alpha; bh=Ex/il6D6uckltoLG0uv4Qfa4+/M=; b=Enl+dpLTiah4hI/wy4cFq74Wt2VH YBKYarE0U9GG5BqD2usBueVAZ3H874HNcytBfFg44QxVYkNgpsGsFDS/Q/RPBczE jVYLnRf1rxpzsMohPdBqVh9/1EEl0ZzYVrrhBmTgCHNCWrq4e4of5Gv8iNPyJuoQ XHq4Bp10R5Z3IME= DomainKey-Signature: a=rsa-sha1; h=Received:Content-Type:Mime-Version:Subject:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=MZMxu9aTKdylajYzUIujq6GDUVEJmUcF932ULnQWNylWC8MXg0UPtZP32d/TQf+u9enlXoQIdUyyz/yvB+gPavcOokMEB3+XmhXbx37Ci5i5ZhmhXVztYBtOQ72Z0X+lYwnlmEv9S/XVE3Df2tJ+UCa21CHLfX+6lZp0Lp3ZCPA=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id B6B4E3CB; Tue, 4 Oct 2016 19:28:11 +0900 (JST) Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) From: Jacques Garrigue In-Reply-To: Date: Tue, 4 Oct 2016 19:33:59 +0900 Cc: OCaML List Mailing Content-Transfer-Encoding: quoted-printable Message-Id: <427FEE0F-28E7-4A77-8ADB-8ACE5BBA35E5@math.nagoya-u.ac.jp> References: <2161155.JggR3X9ZFM@molnar> <2324346.DfHVUap7Qc@molnar> To: Markus Mottl X-Mailer: Apple Mail (2.3124) Subject: Re: [Caml-list] Covariant GADTs On 2016/09/21 06:07, Markus Mottl wrote: >=20 > Has the OCaml team ever considered implementing existentially > quantified type variables for record fields? Having given it some > superficial thought, I didn't see any obvious reason why it would be > impossible, though it would be admittedly more difficult than the > usual (universally quantified) polymorphic record fields. There is no such thing for individual record fields, but note that inline records already give you that for type variable scoping the whole record. type t =3D T : {x: 'a; f: 'a -> int} -> t let g (T r) =3D r.f r.x or for your example: | Elt : {mutable prev : (=E2=80=98el, =E2=80=98kind) t} -> (=E2=80=98el, [= `elt]) t Non-quantified type variables in a GADT constructor are existential, and yo= u can still use explicit quantification for universals. Jacques=