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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 23AA07EF53 for ; Mon, 24 Aug 2015 00:18:39 +0200 (CEST) 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 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0D/AAB4RtpVlwWCBoVdg29pgyW8MQKGAwKBbQEBAQEBARIBAQEBAQgWB0+EIwEBAQMBIwQZAwE1AQEDCwsYAgIYDgICVwYTG4gLB69ZcYRrAos2hQ8BAQEBAQEEAQEBAQEBAQEBEgEGgSKKNYRXMweCLjsSHYEUjWGHWIUGh2yBS0aUVYNqhDNigkwBAQE X-IPAS-Result: A0D/AAB4RtpVlwWCBoVdg29pgyW8MQKGAwKBbQEBAQEBARIBAQEBAQgWB0+EIwEBAQMBIwQZAwE1AQEDCwsYAgIYDgICVwYTG4gLB69ZcYRrAos2hQ8BAQEBAQEEAQEBAQEBAQEBEgEGgSKKNYRXMweCLjsSHYEUjWGHWIUGh2yBS0aUVYNqhDNigkwBAQE X-IronPort-AV: E=Sophos;i="5.15,734,1432591200"; d="scan'208";a="174578426" 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; 24 Aug 2015 00:18:08 +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 3389D6444; Mon, 24 Aug 2015 07:18:05 +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 BB9E92511; Mon, 24 Aug 2015 07:18:04 +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=bWZrLENch577PRFMyFL7GTK5sf0=; b=2V8ztYC7zqffYvBo4ymXQARb5ihe ignTzhtUD5vhlz6RlieVlgegDNHY1lyflWLGOMpac8B4ygs2SPnTejHZdf5ZaH/D bc8VktAuIqrCuwVY/Qx9CXAIz+KW6BZJMuvAFqxYXQCTNb97Y8V1uFxSqIWccsjF vU+bGjT0ei0B2VE= 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=QeoWXgUhOlM1TEVl9iZZf9On9o2u25xTXwQ0BZGWhqJNP6KgIfDml2Xuwr1oflhQw3imuytlerwhk9SivX6c6zzjNAx6QC6xOrasMAu8hnq8/VkeYmLw7z9KY2MyKm8gnIIERNI3MCqCQrrFyXd5nbvHQgZRNJu/JFNWsVCugfU=; 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 956568018; Mon, 24 Aug 2015 07:18:06 +0900 (JST) Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2104\)) From: Jacques Garrigue In-Reply-To: <55D85FE7.2050001@tu-berlin.de> Date: Mon, 24 Aug 2015 07:18:03 +0900 Cc: OCaML List Mailing Content-Transfer-Encoding: quoted-printable Message-Id: <0D467B24-3C94-4640-8264-85BE5312EB55@math.nagoya-u.ac.jp> References: <55D827DB.3010506@tu-berlin.de> <55D85FE7.2050001@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/22 20:41, Christoph H=C3=B6ger wrote: >=20 > Right, that is a good point. That means unification _is_ a special > issue. How about moregen? >=20 > However, I wonder what the true special case is, here: Does this only > apply to type-constructors where some argument is left unused? So if I > would apply my optimization only to constructors where all arguments > appear on the right-hand side (how would I check that?) would that help? 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 approximation 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. Note that this is tricky, and forgetting some needed unification is of cour= se unsound. Also, expansion is used in many places, so that avoiding it completely would be very hard. In theory, we only expand to a graph, so the problem is only if your mutual recursion between classes has very long cycles. You might consider turning some of the types into concrete datatypes, to cut the cycles. > I am facing a real issue here, because my thesis depends on the > compilation of 12k such classes into OCaml, and I need to demonstrate > its practical feasibility. So patching the compiler is not a big issue > (since I find it quite readable). However, I would prefer to upstream > these changes, of course and this would require some mentoring (API, > code style etc.) I would have to see the code to tell you more. As stated above, the real problem is the length of the cycles in the expand= ed graph. Jacques Garrigue >=20 > Am 22.08.2015 um 11:23 schrieb Jeremy Yallop: >> On 22 August 2015 at 08:42, Christoph H=C3=B6ger >> wrote: >>> 1. In the case of equality, it seems fairly simple. Iff the path of two >>> constructors is the same and both argument lists are equal, the types >>> are equal, right? >>=20 >> "If", but not "iff", unless you expand first. Consider >>=20 >> type 'a t =3D unit >>=20 >> Then 'int t' and 'float t' should be considered equal, since they both >> expand to 'unit', even though the argument lists are unequal >>=20 >>> 2. In the case of unification, if both paths are the same, the argument >>> lists are of the same length, we can directly unify the arguments, righ= t? >>=20 >> Again, you need to expand the path first. Consider the following >> function, using the same definition of 't' as above: >>=20 >> fun (a : 'a) (b : 'b) -> >> let c : 'a t =3D () >> and d : 'b t =3D () in >> ignore [c; d]; >>=20 >> The last line involves unifying the types 'a t and 'b t. Unifying the >> type arguments 'a and 'b results in the following type for the >> function: >>=20 >> 'a -> 'a -> unit >>=20 >> Expanding 't' before unifying means that 'a and 'b are not unified, >> and the function can be given the more general type: >>=20 >> 'a -> 'b -> unit