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 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 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.11; 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.11; 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@ms.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.11; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@ms.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible 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 --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) gram= mar >>> -> ('token1, 'phrase1) parser >>> =3D fun gram -> ( >>> ... >>>=20 >>> It goes o for a hundred-odd lines. >>> The type-parameterized types Phrasestream.phrasestream, grammar, and pa= rser=20=20=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 identifyi= ng >>> the type parameters 'token1 an 'phrase1 because of type errors I've mad= e 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 ty= pes, and you cannot unify them. Aside of that the behavior is the same as w= hat 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 Ga= rrigue wrote:

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

I have a (broken)= function definition starting:

let mixfix : 't= oken1 'phrase1.
('token1, 'phrase1, ('token1, 'phrase1) Phras= estream.phrasestream) grammar
     &= nbsp;-> ('token1, 'phrase1) parser
 =3D  fun gra= m -> (
...

It goes o for a hu= ndred-odd lines.
The type-parameterized types Phrasestream.ph= rasestream, grammar, and parser   
have been previo= usly defined, and there are also operations defined on these
= types.

The problem I'm having is that the OCam= l type-checker ends up identifying
the type parameters 'token= 1 an 'phrase1 because of type errors I've made in
the body of= the mixfix function.  Somewhere I ended up using an
ope= rator 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 nat= ural result.

Is there some way of forcing the = type checker to treat 'token1 and&nbs= p;
'phrase1 as different types so that I can get meani= ngful 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.
  &n= bsp;(token1, phrase1, (token1, phrase1) Phrasestream.phrasestream) grammar<= br class=3D"">      -> (token1, phrase1) p= arser
 =3D  fun gram -> (

Thus *with* the type key= word, but *without* the apostrophes on token1 
a= nd phrase1?

Exactly. This means that in the body of your functio= n their are abstract types, and you cannot unify them. Aside of that the be= havior is the same as what we had written first.
Jacq= ues

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