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 651CB7EE25 for ; Fri, 25 Oct 2013 10:29:16 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of rdicosmo@gmail.com) identity=pra; client-ip=209.85.212.179; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rdicosmo@gmail.com"; x-sender="rdicosmo@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of rdicosmo@gmail.com designates 209.85.212.179 as permitted sender) identity=mailfrom; client-ip=209.85.212.179; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rdicosmo@gmail.com"; x-sender="rdicosmo@gmail.com"; 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@mail-wi0-f179.google.com) identity=helo; client-ip=209.85.212.179; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rdicosmo@gmail.com"; x-sender="postmaster@mail-wi0-f179.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AiICAK4qalLRVdSzm2dsb2JhbABZgz9OgxmoUo0fhmMWDgEBAQEBBgsLCRQogiUBAQUjBAsBDQEUGQsBAwwBBQUYAgIFBB0CAg8FIAEFAQEJGBMJCYdjAw8EAQMFmnKMA4NdhFMnAwqJZQEFDAqBE4xrhCo1gQ0DmAmBMIskg0hBgWSCbYFv X-IPAS-Result: AiICAK4qalLRVdSzm2dsb2JhbABZgz9OgxmoUo0fhmMWDgEBAQEBBgsLCRQogiUBAQUjBAsBDQEUGQsBAwwBBQUYAgIFBB0CAg8FIAEFAQEJGBMJCYdjAw8EAQMFmnKMA4NdhFMnAwqJZQEFDAqBE4xrhCo1gQ0DmAmBMIskg0hBgWSCbYFv X-IronPort-AV: E=Sophos;i="4.93,568,1378850400"; d="scan'208";a="31835346" Received: from mail-wi0-f179.google.com ([209.85.212.179]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 25 Oct 2013 10:29:15 +0200 Received: by mail-wi0-f179.google.com with SMTP id hm4so708722wib.12 for ; Fri, 25 Oct 2013 01:29:15 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=sender:date:from:to:cc:subject:message-id:references:mime-version :content-type:content-disposition:content-transfer-encoding :in-reply-to:user-agent; bh=TwYZRr9NDL87CBMBlnv1o5BEdJ+lC0PgabEmKqG7SoY=; b=kcw2CbCrOVaAhcKbHOJ3hunKSHD2ELRCtN1w8MtmS0BHMJRL/Q8vuGHwfH7Grogm58 yUgjqqtpSKDmvjQRF2faW2+i/a/vQZgHrA6+2Q9xYMLC46ux53hLMQ4V2xExAZcKrtlF WihPfICvRBmIIoz4+sJx2rKzwnCX65Z3eo0XY+IOvQZIcdJvSusQhQi/SVKDZpciimPY GddeVtwcoPl0F3+kwgEDzow5h5YiXqosDHyHsDsMVSEt7SBOMpSlfoseJ4YG7Hnt03C5 DpqlQt1dnFnw5wtQ7amC3yd4dXGWiGtaQYQMGDzJH6eAJHfNhaLa+8QqyWz8hyUer24F 6hmA== X-Received: by 10.194.94.33 with SMTP id cz1mr521773wjb.73.1382689754521; Fri, 25 Oct 2013 01:29:14 -0700 (PDT) Received: from voyager (bny92-3-81-56-44-163.fbx.proxad.net. [81.56.44.163]) by mx.google.com with ESMTPSA id d11sm3539428wic.4.2013.10.25.01.29.12 for (version=TLSv1.2 cipher=RC4-SHA bits=128/128); Fri, 25 Oct 2013 01:29:13 -0700 (PDT) Sender: Roberto Di Cosmo Received: from dicosmo by voyager with local (Exim 4.80) (envelope-from ) id 1VZclb-00046Q-D3; Fri, 25 Oct 2013 10:29:11 +0200 Date: Fri, 25 Oct 2013 10:29:11 +0200 From: Roberto Di Cosmo To: Andreas Rossberg Cc: Jacques Garrigue , OCaML List Mailing Message-ID: <20131025082911.GB23798@voyager> References: <97627FCD-30E1-45AD-A72B-CD423170C0AC@math.nagoya-u.ac.jp> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Disposition: inline Content-Transfer-Encoding: 8bit In-Reply-To: User-Agent: Mutt/1.5.20 (2009-06-14) Subject: Re: [Caml-list] Equality between abstract type definitions Dear Andreas, let me offer a comment on terminology here: 'a, 'b and the like have always been used to denote polymorphism in a type, and hence used as unification variables since the beginning of the ML language history, to infer the type of a program. When you annotate a program with types, you are just adding more type equations to the unification problem, and you may of course get at the end a type that is less generic than the one you gave in the annotation (that's the key rule of the game in unification). I am curious to know why you consider this a pitfall: if it is not what people expect, it is probably because nobody explained their meaning to them properly, and I am quite interested in understanding how to explain this better. On the other side, the '_a, '_b variables are just a convenient device that allows to give a type to programs with side effect when OCaml does not know if it's safe to apply the generalization rule: a function f of type '_a -> '_a can be instantiated only once, and after that its type will no longer change (sometimes these are called "logical" variables, but this terminology is kind of misleading). You cannot use '_a variables yourself: # let f (x: '_a) = x;; Error: The type variable name '_a is not allowed in programs -- Roberto On Fri, Oct 25, 2013 at 08:44:50AM +0200, Andreas Rossberg wrote: > On Oct 25, 2013, at 01:23 , Jacques Garrigue wrote: > > In OCaml, type variables used in type annotations are just unification variables: > > 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 type, > > 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 they want either -- especially since there often is no convenient way to actually 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 variables, and only ones of the form '_a, '_b as unification variables. That matches the notation that OCaml has always been using in its output. More expressive and clearer signalling of intent. > > 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 such 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 thing, because it uncovers actual bugs. > > Anyway, just dreaming aloud… :) > > /Andreas > > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa.inria.fr/sympa/arc/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs -- Roberto Di Cosmo ------------------------------------------------------------------ Professeur En delegation a l'INRIA PPS E-mail: roberto@dicosmo.org Universite Paris Diderot WWW : http://www.dicosmo.org Case 7014 Tel : ++33-(0)1-57 27 92 20 5, Rue Thomas Mann F-75205 Paris Cedex 13 Identica: http://identi.ca/rdicosmo FRANCE. Twitter: http://twitter.com/rdicosmo ------------------------------------------------------------------ Attachments: MIME accepted, Word deprecated http://www.gnu.org/philosophy/no-word-attachments.html ------------------------------------------------------------------ Office location: Bureau 3020 (3rd floor) Batiment Sophie Germain Avenue de France Metro Bibliotheque Francois Mitterrand, ligne 14/RER C ----------------------------------------------------------------- GPG fingerprint 2931 20CE 3A5A 5390 98EC 8BFC FCCA C3BE 39CB 12D3