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 0A6C07EE25 for ; Mon, 28 Oct 2013 04:30:47 +0100 (CET) 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: AvsBABHZbVKFBoIFnGdsb2JhbABZwnGBMg4BAQEBAQgUCTyCJQEBBAEnHAE1AgMLCxgcElcGE4gBBaUchFkChRmJDQePIjMHgx+BDYlAjk2VPA X-IPAS-Result: AvsBABHZbVKFBoIFnGdsb2JhbABZwnGBMg4BAQEBAQgUCTyCJQEBBAEnHAE1AgMLCxgcElcGE4gBBaUchFkChRmJDQePIjMHgx+BDYlAjk2VPA X-IronPort-AV: E=Sophos;i="4.93,583,1378850400"; d="scan'208";a="32129996" 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; 28 Oct 2013 04:30:44 +0100 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 534CF638D; Mon, 28 Oct 2013 12:30:41 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id C15E640F1; Mon, 28 Oct 2013 12:30:40 +0900 (JST) DomainKey-Signature: h=Received:Subject:Mime-Version:Content-Type:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=; c=nofws; d=math.nagoya-u.ac.jp; q=; s=alpha Received: from tanpopo.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 71D5F40D0; Mon, 28 Oct 2013 12:30:40 +0900 (JST) Mime-Version: 1.0 (Mac OS X Mail 7.0 \(1816\)) Content-Type: text/plain; charset=windows-1252 From: Jacques Garrigue In-Reply-To: Date: Mon, 28 Oct 2013 12:30:43 +0900 Cc: OCaml Mailing List Content-Transfer-Encoding: quoted-printable Message-Id: <54E55371-5BB8-4798-83AF-A684404A2DBE@math.nagoya-u.ac.jp> References: <97627FCD-30E1-45AD-A72B-CD423170C0AC@math.nagoya-u.ac.jp> To: Andreas Rossberg X-Mailer: Apple Mail (2.1816) Subject: Re: [Caml-list] Equality between abstract type definitions Dear Andreas, It is a bit late to enter this discussion, but I just have two comments 1) All the bug reports (and messages on this list, but for this one) I have= seen were about the non-generalization of type variables, not their interpretation.= Namely, people have a hard time understanding why the following is not accepted: let f () =3D let id : 'a -> 'a =3D fun x -> x in (id 1, id true) I agree that in this respect SML=92s choice of inferring a minimal scope = (and allowing local generalization of named type variables) is more helpful. This part could be implemented without breaking existing programs. Note however that we already have other ways of introducing local type va= riables. (For instance, writing " id : =91a. =91a -> =91a " in the above.) 2) In ocaml, type variables are also used for describing sharing in recursi= ve types: ( as =91a) and also for talking about types that have a row variable (< m : int; .. > as =91a) -> =91a These two cases use an existential view of type variables. Jacques > On Oct 25, 2013, at 01:23 , Jacques Garrigue wrote: >> In OCaml, type variables used in type annotations are just unification v= ariables: >> 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 t= ype, >> without writing the type by hand. >=20 > 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 ty= pe system, not what most people expect, and in 98% of the cases, not what t= hey want either -- especially since there often is no convenient way to act= ually express what they want. >=20 > 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 varia= bles, and only ones of the form '_a, '_b as unification variables. That mat= ches the notation that OCaml has always been using in its output. More expr= essive and clearer signalling of intent. >=20 > Obviously, such a change would break some code, code that actually relies= on 'a being just a unification variable. But my optimistic guess is that s= uch code is rather rare. And it would be trivial to adapt. >=20 > It would also break code that assumed the wrong behaviour and only compil= ed by accident (such as the Peter's example). But arguably, that's a good t= hing, because it uncovers actual bugs. >=20 > Anyway, just dreaming aloud=85 :) >=20 > /Andreas >=20