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 ESMTPS id 2EB9D5D5 for ; Wed, 27 Feb 2019 03:46:20 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.58,417,1544482800"; d="scan'208,217";a="371042069" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 27 Feb 2019 04:46:17 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id 96B33825F9; Wed, 27 Feb 2019 04:46:17 +0100 (CET) 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 D1EF482581 for ; Wed, 27 Feb 2019 04:46:04 +0100 (CET) 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@ms.math.nagoya-u.ac.jp IronPort-PHdr: =?us-ascii?q?9a23=3A8Z8foxyM/heSkkfXCy+O+j09IxM/srCxBDY+r6Qd?= =?us-ascii?q?2+oSIJqq85mqBkHD//Il1AaPAd2Lraocw8Pt8InYEVQa5piAtH1QOLdtbDQizf?= =?us-ascii?q?ssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1?= =?us-ascii?q?JuPoEYLOksi7ze+/94HQbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeu?= =?us-ascii?q?BWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbO?= =?us-ascii?q?SxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDtU7s6RSqt4LtqSB/wiS?= =?us-ascii?q?cIKTg58H3MisdtiK5XuQ+tqwBjz4LRZoyeKfhwcb7Hfd4CRWRPXdpeWCNcDI2y?= =?us-ascii?q?bYQBEeQBM+FDoobnu1cOqAGzBQmwCO/xzDJDm3/43bc90+QkCQzI2BYvEM4XsH?= =?us-ascii?q?TJstr1L7oZX+Gvw6nS1zXDbvxW2Srj54PVdR0hruuDXahqccrQxkkvCh3Kg06V?= =?us-ascii?q?qYP/IzOV1v4Bs26B4OpvUuKui3QopxhsojS13MgjlpPFhoANyl3d8yhy3YU7Jc?= =?us-ascii?q?WgRUJmb9OpHoFcuiCAO4drTM4uX3tktDsnxrAApJW1ZjIFyI49yB7ac/GHc5aH?= =?us-ascii?q?4hbkVOuJJDd4n2hpeLeliBau8Uis0Ov8WdO70FZNritKiMDAtm0X2xPJ9seLUP?= =?us-ascii?q?l9/l+51TaO0QDc9P1ELFgpmafVJZMt2L89moAOvUnNAiP6glj6gLKOekUh4Oeo?= =?us-ascii?q?6uDnYrv8pp+bMo95kg7+Pb40msylAOQ4PRUOUHaA9OS5zrLj4U35TK9MjvIsna?= =?us-ascii?q?nZt5DbKt4Cqq6kGQNayJos5wy9Dze+yNgYh2UILEpZeBKbiIjkI03BL+r9Dfe7?= =?us-ascii?q?mlislDZrx+vaPrD6GZXMLn3DkK/7crpn6k5czhAzzdFF6J5OBLEBOqG7ZkiklN?= =?us-ascii?q?HeAgU4MESexOHiQIF924USQ2OMKrOeKKTT90eP4ftpKO6JMtw7ojH4ftos7Ofz?= =?us-ascii?q?gGRxtlYHZ6imwJZfPH+xBO5nLFiUSX/lntdHF24FuRs3CfGsgVbEUyYFNCX6ZL?= =?us-ascii?q?41+jxuUNHuNozEXI34xeXZhH7qTK0TXXhPDxW3KVmtcoyFX/kWbyfIe51kmyAE?= =?us-ascii?q?E76oRIgw3FSz8gbxjbh/fLKNpn8o8Kn73d0w3NX90Ako/GYtXcGUz2HLSWh7mX?= =?us-ascii?q?IBAiJw1as5o1Qvkg7eg5g9uORREJlo390MUgo+MsSAnelhTdX7RgKHeN6GT0ev?= =?us-ascii?q?B8jgCDp3TMpjm9I=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AeAAADB3ZclwuCBoVkGgEBAQEBAgEBA?= =?us-ascii?q?QEHAgEBAQGBZYEOgi0hEieNAY0KmhkBDIRsAoQcBgY0EgEDAQECAQEBAQETAQE?= =?us-ascii?q?BAQEIFgZMDII6KQGCZwEFJxkBATcBDwsYJwdGEQYTgyCBcqpggW0zgngBAQWCR?= =?us-ascii?q?YJ8IYFKCIxfgX+BOB+CHi6IPIImh2wHiWuSCQmSaBmTGpoCgxOBXoF3TTg7KgG?= =?us-ascii?q?CQT6BXhqGWodcMAMwklkBAQ?= X-IPAS-Result: =?us-ascii?q?A0AeAAADB3ZclwuCBoVkGgEBAQEBAgEBAQEHAgEBAQGBZYE?= =?us-ascii?q?Ogi0hEieNAY0KmhkBDIRsAoQcBgY0EgEDAQECAQEBAQETAQEBAQEIFgZMDII6K?= =?us-ascii?q?QGCZwEFJxkBATcBDwsYJwdGEQYTgyCBcqpggW0zgngBAQWCRYJ8IYFKCIxfgX+?= =?us-ascii?q?BOB+CHi6IPIImh2wHiWuSCQmSaBmTGpoCgxOBXoF3TTg7KgGCQT6BXhqGWodcM?= =?us-ascii?q?AMwklkBAQ?= X-IronPort-AV: E=Sophos;i="5.58,417,1544482800"; d="scan'208,217";a="371041980" Received: from bsd20.math.nagoya-u.ac.jp (HELO ms.math.nagoya-u.ac.jp) ([133.6.130.11]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 27 Feb 2019 04:46:02 +0100 Received: from garrigue-mini.math.nagoya-u.ac.jp (garrigue-mini.math.nagoya-u.ac.jp [172.16.30.37]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ms.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 614B9968A20; Wed, 27 Feb 2019 12:45:59 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=math.nagoya-u.ac.jp; s=20160220; t=1551239159; bh=UCl4cPNu0NbwjLMjuOcp5/NTtH9WJEiApfusHK9giP4=; h=From:Subject:Date:In-Reply-To:Cc:To:References; b=c2kN/m5RCM4rYaq9AR09V0LNDd+33+ALdkrm8OdAPM9ij65IanNoMJXC+gIWhh22L NLB8OYqMFL51OaWWfNJ6hJh4nqnhd1He55agINpc2ZDcP1FyqUVQA+KNezcinnZ0mj OAtF24unOuuWNB39acKo7wf59jQNAdR76SCxLu9M= From: Jacques Garrigue Message-Id: <710C867E-725F-419E-9FFA-0C6AF7FCD763@math.nagoya-u.ac.jp> Content-Type: multipart/alternative; boundary="Apple-Mail=_9762F7F0-E790-4A6D-A013-FA87ED1C7094" Mime-Version: 1.0 (Mac OS X Mail 11.5 \(3445.9.1\)) Date: Wed, 27 Feb 2019 12:46:20 +0900 In-Reply-To: <20190227015952.zvj7fef7fg3ivsnf@topoi.pooq.com> Cc: Mailing List OCaml To: Hendrik Boom References: <20190226062341.t35u2tz5tole2jyv@topoi.pooq.com> <20190227015952.zvj7fef7fg3ivsnf@topoi.pooq.com> X-Mailer: Apple Mail (2.3445.9.1) X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-4.6.2 (ms.math.nagoya-u.ac.jp [0.0.0.0]); Wed, 27 Feb 2019 12:45:59 +0900 (JST) X-Virus-Scanned: clamav-milter 0.99.2 at bsdserver20 X-Virus-Status: Clean X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on bsdserver20.math.nagoya-u.ac.jp Subject: Re: [Caml-list] An awkwardness with type parameters Reply-To: Jacques Garrigue X-Loop: caml-list@inria.fr X-Sequence: 17373 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: --Apple-Mail=_9762F7F0-E790-4A6D-A013-FA87ED1C7094 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=us-ascii On 2019/02/27 10:59, Hendrik Boom wrote: >=20 > On Tue, Feb 26, 2019 at 03:39:24PM +0900, Jacques Garrigue wrote: >>=20 >> 2019/02/26 15:23, Hendrik Boom >: >>>=20 >>> I have a (broken) function definition starting: >>>=20 >>> let mixfix : 'token1 'phrase1. >>> ('token1, 'phrase1, ('token1, 'phrase1) Phrasestream.phrasestream) = grammar >>> -> ('token1, 'phrase1) parser >>> =3D fun gram -> ( >>> ... >>>=20 >>> It goes o for a hundred-odd lines. >>> The type-parameterized types Phrasestream.phrasestream, grammar, and = parser =20 >>> have been previously defined, and there are also operations defined = on these >>> types. >>>=20 >>> The problem I'm having is that the OCaml type-checker ends up = identifying >>> the type parameters 'token1 an 'phrase1 because of type errors I've = made in >>> the body of the mixfix function. Somewhere I ended up using an >>> operator that's supposed to work on values of type 'token1 >>> on a value of type 'phrase1 instead, and identification of 'token1 = and=20 >>> 'phrase1 is the natural result. >>>=20 >>> Is there some way of forcing the type checker to treat 'token1 and=20= >>> 'phrase1 as different types so that I can get meaningful type errors >>> at the point were they occur? >>=20 >> You can use locally abstract types, which are often used with GADTs = but are not >> restricted to them: >> let mixfix : type token1 phrase1. >> (token1, phrase1, (token1, phrase1) Phrasestream.phrasestream) = grammar >> -> (token1, phrase1) parser >> =3D fun gram -> ( >=20 > Thus *with* the type keyword, but *without* the apostrophes on token1=20= > and phrase1? Exactly. This means that in the body of your function their are abstract = types, and you cannot unify them. Aside of that the behavior is the same = as what we had written first. Jacques --Apple-Mail=_9762F7F0-E790-4A6D-A013-FA87ED1C7094 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=us-ascii On 2019/02/27 10:59, Hendrik = Boom wrote:
On Tue, Feb 26, 2019 at 03:39:24PM +0900, Jacques Garrigue = wrote:

2019/02/26 15:23, Hendrik Boom <hendrik@topoi.pooq.com>:

I have a (broken) function = definition starting:

let mixfix : 'token1 = 'phrase1.
('token1, 'phrase1, ('token1, 'phrase1) = Phrasestream.phrasestream) grammar
      -> ('token1, 'phrase1) = parser
 =3D  fun gram -> (
...
It goes o for a hundred-odd lines.
The type-parameterized types Phrasestream.phrasestream, = grammar, and parser   
have been previously = defined, and there are also operations defined on these
types.

The problem I'm having is = that the OCaml type-checker ends up identifying
the type = parameters 'token1 an 'phrase1 because of type errors I've made in
the body of the mixfix function.  Somewhere I ended up = using an
operator that's supposed to work on values of = type 'token1
on a value of type 'phrase1 instead, and = identification of 'token1 and 
'phrase1 is = the natural result.

Is there some way of = forcing the type checker to treat 'token1 and 
'phrase1 as = different types so that I can get meaningful type errors
at = the point were they occur?

You = can use locally abstract types, which are often used with GADTs but are = not
restricted to them:
 let mixfix : = type token1 phrase1.
   (token1, phrase1, = (token1, phrase1) Phrasestream.phrasestream) grammar
      -> (token1, phrase1) = parser
 =3D  fun gram -> (

Thus *with* the type keyword, but *without* the apostrophes = on token1 
and phrase1?

Exactly. This = means that in the body of your function their are abstract types, and = you cannot unify them. Aside of that the behavior is the same as what we = had written first.

Jacques

= --Apple-Mail=_9762F7F0-E790-4A6D-A013-FA87ED1C7094--