From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr 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 E02DC7F0D9 for ; Tue, 25 Aug 2015 16:02:45 +0200 (CEST) IronPort-PHdr: 9a23:LadfBBWmMFiXcwjfsYdUMWz6uoPV8LGtZVwlr6E/grcLSJyIuqrYZxSHt8tkgFKBZ4jH8fUM07OQ6PC7HzFRqs3a+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8aVPlQD32H1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu3SNp41Rr1ADTkgL3t9pIiy7UGCHkOz4S43Un8XiQZPGwjyzI/1U4255iD6rOtmxC6CPYv2Sr07VC6K87ouQhLyjCYBcTI0pjL5kMt12YBSqwu8qgc37IfOeoCaKfc2KqzUZ8kbSndMdsNYSywHBIqzaJoGSvdHNO0erZGr9AhGlge3GQT5XLCn8TRPnHKjmPRii+k= Authentication-Results: mail3-smtp-sop.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 (mail3-smtp-sop.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=mail3-smtp-sop.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 (mail3-smtp-sop.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=mail3-smtp-sop.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 (mail3-smtp-sop.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=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0AmAQD8dNxVlwWCBoVdFoNZaYMltB6GUoFtCoV7AoFrEgEBAQEBAQEBEAEBAQEBCBYHT4IdggcBAQICIx0DATUBAQ4LGAICGA4CAlcGLogSDrFecYRrAotChG8BAQEBAQEBAwEBAQEBAQEBARIBBoEiijWEVy4FB4IuDC8SHYEUjWSGVIEEhQaHbIFKRocIjVKDaoQzYgEBgkoBAQE X-IPAS-Result: A0AmAQD8dNxVlwWCBoVdFoNZaYMltB6GUoFtCoV7AoFrEgEBAQEBAQEBEAEBAQEBCBYHT4IdggcBAQICIx0DATUBAQ4LGAICGA4CAlcGLogSDrFecYRrAotChG8BAQEBAQEBAwEBAQEBAQEBARIBBoEiijWEVy4FB4IuDC8SHYEUjWSGVIEEhQaHbIFKRocIjVKDaoQzYgEBgkoBAQE X-IronPort-AV: E=Sophos;i="5.15,746,1432591200"; d="scan'208";a="143753036" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail3-smtp-sop.national.inria.fr with ESMTP; 25 Aug 2015 16:02:43 +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 705FE63D5; Tue, 25 Aug 2015 23:02:40 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (rabbit-172 [172.16.254.254]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id DEF764114; Tue, 25 Aug 2015 23:02:39 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; s=alpha; bh=3GjpcKEbO2BSwoSHEgmP7cqBiEA=; b=du9kpSTR4+Kl7h+no1CoMmswW7gC INWwKevXCFyeQG9U2ipvp4kR6fam+E1X9pFCmHdFxnlFQG4H+VIkK/LOyphQft2r tSLPpPhy1HEQkGzRkgjaWVVsXTkX/Uv7BfpYlxtubnDMWfXpXNJ5+jKnYonwN1Es DnCNi2aHbaFgeAQ= DomainKey-Signature: a=rsa-sha1; h=Received:Subject:Mime-Version:Content-Type:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=amsYIMSVyVx+pu2yFkk3LywCao47rP8lJx56l+Xis1VobpcVKoZ3/2sZLCGSfzWNdgLJ4GLow9JXm3y1KeyDaoVo5Vzd2MuNDHPBpMCpSTsJfYkd5YZwq/HSQQwznrgTHwMvmWwLBR9+vTrOHbOPyDou47lSKTMmYrP2zOEiiLA=; 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 D01DD844E; Tue, 25 Aug 2015 23:02:39 +0900 (JST) Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2104\)) Content-Type: text/plain; charset=utf-8 From: Jacques Garrigue In-Reply-To: <55DAEEDA.6020709@tu-berlin.de> Date: Tue, 25 Aug 2015 23:02:38 +0900 Cc: OCaML List Mailing Content-Transfer-Encoding: quoted-printable Message-Id: <3A6D9855-8FCD-4345-983D-011DD5138C0E@math.nagoya-u.ac.jp> References: <55D827DB.3010506@tu-berlin.de> <55D85FE7.2050001@tu-berlin.de> <0D467B24-3C94-4640-8264-85BE5312EB55@math.nagoya-u.ac.jp> <55DAB843.5010800@tu-berlin.de> <55DAEEDA.6020709@tu-berlin.de> To: =?utf-8?Q?Christoph_H=C3=B6ger?= X-Mailer: Apple Mail (2.2104) Subject: Re: [Caml-list] Expansion of type-constructors in ctype.ml On 2015/08/24 19:15, Christoph H=C3=B6ger wrote: >=20 > find attached a patch against the 4.02.3 tree that solves my issue with > compiling the problematic examples. >=20 > I am pretty confident that the change to eqtype is sound, I do not know > exactly what moregen() is intended to do, though and it seems that its > side-effects are required (that is why I expand the types there in any > case). >=20 > I appreciate any further comments, >=20 > Christoph Do you mean that modifying moregen and eqtype (but not unify) in a conservative way would be enough to solve your problem? Then indeed we could do that. At least your code for eqtype seems fine. For moregen, this is not sufficie= nt, due to non-local side effects. By the way, we should keep your example around to prevent regressions. On 2015/08/24 15:22, Christoph H=C3=B6ger wrote: > Am 24.08.2015 um 00:18 schrieb Jacques Garrigue: >> This is indeed a pretty difficult problem, as you must be careful of not >> changing the semantics of unification. >> Until recently, the only solution was to expand the type, as there was >> no static information cacheing whether an argument was used in the >> body or not. >> However, since relatively recent changes about variance information >> (the switch to 7 flags=E2=80=A6), we actually have at least an approxima= tion >> of which unifications must be done imperatively, and which needn=E2=80= =99t >> be done at all. >> So it might be doable at least for part of the parameters. >=20 > That sounds interesting. What are the relevant variance flags? >=20 You should read the following paper: http://www.math.nagoya-u.ac.jp/~garrigue/papers/injectivity.pdf If all the flags were always correct then it would be simple: any flag being set would mean that the variable really appears in the type, so you must recurse on it (at least for eqtype and moregen). However, variance inference for the result of functors is not exact, meaning that to be sure that a variable will not disappear, you must check that inj is set (meaning that there is a concrete occurence). In a nutshell: may_pos and may_neg are both unset (i.e. nothing is set) =3D> no need to re= curse inj is set =3D> must recurse otherwise =3D> must expand Jacques Garrigue=