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 3A7757EE25 for ; Sat, 26 Oct 2013 19:32:59 +0200 (CEST) X-IronPort-AV: E=Sophos;i="4.93,577,1378850400"; d="scan'208";a="38921830" Received: from ras75-4-82-229-153-115.fbx.proxad.net (HELO MP-R19.local) ([82.229.153.115]) by mail2-relais-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-CAMELLIA256-SHA; 26 Oct 2013 19:32:57 +0200 Message-ID: <526BFCCA.8080804@inria.fr> Date: Sat, 26 Oct 2013 19:32:58 +0200 From: Didier Remy Reply-To: Didier.Remy@inria.fr User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:24.0) Gecko/20100101 Thunderbird/24.0.1 MIME-Version: 1.0 To: caml-list@inria.fr, Francois Pottier References: <97627FCD-30E1-45AD-A72B-CD423170C0AC@math.nagoya-u.ac.jp> <20131025082911.GB23798@voyager> <526A7A3F.2090405@mpi-sws.org> In-Reply-To: <526A7A3F.2090405@mpi-sws.org> Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Subject: Re: [Caml-list] Equality between abstract type definitions >> 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). > Aren't you conflating two different universes here? Namely, the > declarative type system and the type inference algorithm? The ML type > system semantics as such, at least in most formalisations I can remember, > knows nothing about unification variables -- that's an implementation > detail of algorithm W. And the user interface of a language is the > declarative system, not the underlying implementation. Making unification > variables user-visible is an extension to the basic ML type system that I > have rarely seen made precise Andreas, I am not sure what point you are trying to make. Sure, the name "unification variable" is misleading and should not be used here, as it refers to the algorithm. Instead, one should call them flexible type variable or whatever that refers to the specification. Still, flexible variables make a lot of sense in the specification (even if not often done in formal presentations). A language that does type inference should allow the user to say that two arguments have the same type without telling what these types are, using a flexible type variable. (It should also allow the user to tell the type checker that some expression whould have exactly this type scheme, using a rigid type variable. For this reason, the language should expose to the user the both notions of rigid and flexible bindings. One can easily specify the introduction of a flexible variable 'a in some program M as the following typing rule and without reference to the implementation: G |- M ['a <- t] : s ----------------------- G |- for some 'a. M : s François and I discuss this and formalize it in our chapter "The Essence of ML Type Inference" in "Advanced Topics in Types and Programming". ---------------- > (I seem to remember that the Didiers did that in the context of MLF). Yes, since we needed more annotations in MLF because all function paramters that are used polymorphically must be annotated, we wanted to be able to only annoatte specify parts of the parameter that had to be used polymorphically. We could give type annotations of the form: for some 'u, for all 'a, 'b, ('a -> 'b) -> 'a * 'u -> 'b * 'v When used as the annotation of a function parameter, 'u could be freely instantiated, even to a polymorphic type, as long as this part of the argument was not used polymorphically. We found this necessary in MLF, but it would also be quite useful in OCaml. Didier