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 4692E7FD26 for ; Thu, 5 Nov 2015 12:29:21 +0100 (CET) IronPort-PHdr: 9a23:bl1dlRLytd8XChfzM9mcpTZWNBhigK39O0sv0rFitYgULv7xwZ3uMQTl6Ol3ixeRBMOAu68C0Lad6/2ocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC0oLsi6vqptX6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVWqz/e+E8TKdEJDUgKWE8osPx5jfZSg7ayXwHTWQQ2gRPBUDv9hz2U431tTSy4uV6wzabO4joCLocRjmoqatmHky7wBwbPiI0pTmEwvd7i7hW9Uqs Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=goswin-v-b@web.de; spf=Pass smtp.mailfrom=goswin-v-b@web.de; spf=None smtp.helo=postmaster@mout.web.de Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of goswin-v-b@web.de) identity=pra; client-ip=212.227.17.12; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of goswin-v-b@web.de designates 212.227.17.12 as permitted sender) identity=mailfrom; client-ip=212.227.17.12; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mout.web.de) identity=helo; client-ip=212.227.17.12; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="postmaster@mout.web.de"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0BIAACrPDtWnAwR49RehA5vtj6JLRmFeQKBLDsRAQEBAQEBAQEQAQEBAQEGDQkJIS6CLoIIAQEEJwsBVgsYCSUPBSg0iBgBGbxjH4R0AQsBIIZVhH2FJ4J9gRUFlkiFHYd+giqGaQyTKzeCU4FecYUfAQEB X-IPAS-Result: A0BIAACrPDtWnAwR49RehA5vtj6JLRmFeQKBLDsRAQEBAQEBAQEQAQEBAQEGDQkJIS6CLoIIAQEEJwsBVgsYCSUPBSg0iBgBGbxjH4R0AQsBIIZVhH2FJ4J9gRUFlkiFHYd+giqGaQyTKzeCU4FecYUfAQEB X-IronPort-AV: E=Sophos;i="5.20,247,1444687200"; d="scan'208";a="186201308" Received: from mout.web.de ([212.227.17.12]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 05 Nov 2015 12:29:20 +0100 Received: from frosties.localnet ([95.208.221.151]) by smtp.web.de (mrweb103) with ESMTPSA (Nemesis) id 0LtWwK-1adZ8G0wSq-010uoe for ; Thu, 05 Nov 2015 12:29:20 +0100 Received: from mrvn by frosties.localnet with local (Exim 4.84) (envelope-from ) id 1ZuIjH-0006oV-Fy for caml-list@inria.fr; Thu, 05 Nov 2015 12:29:19 +0100 Date: Thu, 5 Nov 2015 12:29:19 +0100 From: Goswin von Brederlow To: caml-list@inria.fr Message-ID: <20151105112919.GA23627@frosties> References: <55D827DB.3010506@tu-berlin.de> MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline Content-Transfer-Encoding: 8bit In-Reply-To: User-Agent: Mutt/1.5.23 (2014-03-12) X-Provags-ID: V03:K0:q0kSXZ0X0Rb43fYZSTaV1DF7QaHZw9LlFq264BzJ8QwDHQ4ce8d RA+AUCZ6fhZkLLC6GYuLRi67xetj2wPcSmJuyqQiZIz39C/S/tsEDszdW++Sn+lJDdNTCz1 lAn0pzpHrfl2WKyDH8dQ7HUQFZ4+zU0FKBgrh04NRx2OwHSAaAPsS3OjmoGio71qmIJXJ/7 fqB9+Eme9NjudBodkV2VA== X-UI-Out-Filterresults: notjunk:1;V01:K0:PKS4+Lky7gg=:0pWMD+xl8GuU1GxS6TxRcs tnsDIYlgbG9+4WqHT1iK9aS3XPfpoM2lzNd9bUxU/RdRrJJ4UGgonr0d8PYOnLqinheF17FLP Dy7dhb6oSKWzqc0S4NflwFgbucyDReFw/301jYWE4hF1I1O/HYyOLLeqUO1sXSNxJkkd+9Gll ufjmQ2S69N3FSMz9maYVcHdrPzNbSmhqfVerquvK1WVb128MhU+kEOiKV6aS42sFTzvZmkAz0 nw+VtsUHY+RihWn+nuZFc7ePIzs+pIiLgIHuQiR4KCoBS9xGRf1qAaAC3OhMEfx0iL5IUfkpB mNnKucjVlv+D8//ghLkw9ktpUE0UE7fkHU1gqxAlokJNoBdD6Os1wzWvdjhBe6xXyEmkTAkvj JJE1qudqbC+Ko6il0DG6ohHgIgGeQD5GkiWuG0FIdZcfzv3twny5SopLX/MnHrYCx7/cPue74 r7OOny2wB2sG1KbRpT1lBZI4YvsbP02b3/GRAE/S+mCXayPq5R+j1NYOJT/L6xdSGTnX33YCI EhIlYDTZdu05P/0czdP0Wsp41DTTDrJuB+NWRfRGkibkzW9fuPKdT6rbMwv4HYyE2JLqYbFH+ 0fCwZen5AWr2nKKodh58mgWHq+Nieqv9w7rlDPPN6JhCbCxOj7R72Q6L0DHQGFbO3zDZp8+OL 2kJ0wj3WJ+qQ6oleVXuKO7K6XF4RUDghvsI+q6Uhsd9/jY07+1K0csGO2I/o4q26m1JaQyOPd UF622WMz4txIjA/rN7YAoSil8Rj7B3EUE1nQ5FAfatz5uatSszUJlhrmW/w= Subject: Re: [Caml-list] Expansion of type-constructors in ctype.ml On Sat, Aug 22, 2015 at 10:23:04AM +0100, Jeremy Yallop wrote: > On 22 August 2015 at 08:42, Christoph Höger > 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? > > "If", but not "iff", unless you expand first. Consider > > type 'a t = unit > > Then 'int t' and 'float t' should be considered equal, since they both > expand to 'unit', even though the argument lists are unequal > > > 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, right? > > Again, you need to expand the path first. Consider the following > function, using the same definition of 't' as above: > > fun (a : 'a) (b : 'b) -> > let c : 'a t = () > and d : 'b t = () in > ignore [c; d]; > > 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: > > 'a -> 'a -> unit > > Expanding 't' before unifying means that 'a and 'b are not unified, > and the function can be given the more general type: > > 'a -> 'b -> unit In both cases wouldn't it make sense (and be semantically equivalent) to first check for equality and only expand when not equal? I mean f you already have 'a t and 'a t then it doesn't matter if t uses the 'a or not. There is no need to expand it. MfG Goswin