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 611F47EE25 for ; Fri, 25 Oct 2013 08:44:53 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of rossberg@mpi-sws.org) identity=pra; client-ip=139.19.1.49; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rossberg@mpi-sws.org"; x-sender="rossberg@mpi-sws.org"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of rossberg@mpi-sws.org designates 139.19.1.49 as permitted sender) identity=mailfrom; client-ip=139.19.1.49; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rossberg@mpi-sws.org"; x-sender="rossberg@mpi-sws.org"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@hera.mpi-klsb.mpg.de) identity=helo; client-ip=139.19.1.49; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rossberg@mpi-sws.org"; x-sender="postmaster@hera.mpi-klsb.mpg.de"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ar4CABQSalKLEwExhGdsb2JhbABZDsJHgTYOAQEBCgcECQkUKIIlAQEFQAEBNwEPCxguVwYTiAcEpkKEUwEFjmYGjxozB4MfgQ2seUE X-IPAS-Result: Ar4CABQSalKLEwExhGdsb2JhbABZDsJHgTYOAQEBCgcECQkUKIIlAQEFQAEBNwEPCxguVwYTiAcEpkKEUwEFjmYGjxozB4MfgQ2seUE X-IronPort-AV: E=Sophos;i="4.93,568,1378850400"; d="scan'208";a="31820814" Received: from infao0809.mpi-klsb.mpg.de (HELO hera.mpi-klsb.mpg.de) ([139.19.1.49]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES256-SHA; 25 Oct 2013 08:44:52 +0200 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=mpi-sws.org; s=mail200803; h=To:References:Message-Id:Content-Transfer-Encoding:Cc:Date:In-Reply-To:From:Content-Type:Mime-Version:Subject; bh=hnkLVwQsR+21uU1kI4mv8EdZusjDvEuTLV+777I2lQg=; b=Vvkf6dq1AioW8U4PArNIZGOTCqOHHGrrVjQWBUZVKeeFCSFHBQWc4ipzcp6HjaABpTLqTlWMs+caZ1EyNc1mxGeL/7wPifV+20uYGGp+OR8iT0LRCh0K1RSULayLTzTpV5dS/1R/IZibUGBi9cSm86SdXobn83vj74G4+ITc2dA=; Received: from zak.mpi-klsb.mpg.de ([139.19.1.29]:57601) by hera.mpi-klsb.mpg.de (envelope-from ) with esmtp (Exim 4.72) id 1VZb8a-0000pv-L1; Fri, 25 Oct 2013 08:44:51 +0200 Received: from mnch-4d04d8b9.pool.mediaways.net ([77.4.216.185]:60949 helo=[192.168.178.44]) by zak.mpi-klsb.mpg.de (envelope-from ) with esmtpsa (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.72) id 1VZb8a-0002zJ-6d; Fri, 25 Oct 2013 08:44:48 +0200 Mime-Version: 1.0 (Mac OS X Mail 6.6 \(1510\)) Content-Type: text/plain; charset=windows-1252 From: Andreas Rossberg In-Reply-To: <97627FCD-30E1-45AD-A72B-CD423170C0AC@math.nagoya-u.ac.jp> Date: Fri, 25 Oct 2013 08:44:50 +0200 Cc: OCaML List Mailing Content-Transfer-Encoding: quoted-printable Message-Id: References: <97627FCD-30E1-45AD-A72B-CD423170C0AC@math.nagoya-u.ac.jp> To: Jacques Garrigue X-Mailer: Apple Mail (2.1510) X-MPI-Local-Sender: true Subject: Re: [Caml-list] Equality between abstract type definitions On Oct 25, 2013, at 01:23 , Jacques Garrigue = wrote: > In OCaml, type variables used in type annotations are just unification va= riables: > the type checker is allowed to merge them or instantiate them. > This is useful when you want to indicate that two things have the same ty= pe, > without writing the type by hand. Jacques, do you think there is any chance that this will ever be changed? I= think this keeps being one of the most annoying pitfalls in the OCaml type= system, not what most people expect, and in 98% of the cases, not what the= y want either -- especially since there often is no convenient way to actua= lly express what they want. A simple proposal, which I'm sure has been made many times before, would be= to interpret type variables of the form 'a, 'b as proper universal variabl= es, and only ones of the form '_a, '_b as unification variables. That match= es the notation that OCaml has always been using in its output. More expres= sive and clearer signalling of intent. Obviously, such a change would break some code, code that actually relies o= n 'a being just a unification variable. But my optimistic guess is that suc= h code is rather rare. And it would be trivial to adapt. It would also break code that assumed the wrong behaviour and only compiled= by accident (such as the Peter's example). But arguably, that's a good thi= ng, because it uncovers actual bugs. Anyway, just dreaming aloud=85 :) /Andreas