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 82E757EE25 for ; Fri, 25 Oct 2013 16:03:49 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of rossberg@mpi-sws.org) identity=pra; client-ip=139.19.1.49; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="rossberg@mpi-sws.org"; x-sender="rossberg@mpi-sws.org"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.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=mail2-smtp-roc.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 (mail2-smtp-roc.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=mail2-smtp-roc.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: AmYDADV5alKLEwExhGdsb2JhbABZhya7NoE4DgEBAQoHBAkJFCiCJQEBBAEjFQgBATYBAQQLCxgCAgUWCwICCQMCAQIBIwUdBg0BBwEBh30GmxGLDXaDXQEFjmMGgSmOKgeCaoFCnkiOdA X-IPAS-Result: AmYDADV5alKLEwExhGdsb2JhbABZhya7NoE4DgEBAQoHBAkJFCiCJQEBBAEjFQgBATYBAQQLCxgCAgUWCwICCQMCAQIBIwUdBg0BBwEBh30GmxGLDXaDXQEFjmMGgSmOKgeCaoFCnkiOdA X-IronPort-AV: E=Sophos;i="4.93,570,1378850400"; d="scan'208";a="38789290" Received: from hera.mpi-sb.mpg.de (HELO hera.mpi-klsb.mpg.de) ([139.19.1.49]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES256-SHA; 25 Oct 2013 16:03:50 +0200 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=mpi-sws.org; s=mail200803; h=Content-Transfer-Encoding:Content-Type:In-Reply-To:References:Subject:CC:To:MIME-Version:From:Date:Message-ID; bh=RwKpy2+dr5Yz1DaNTiOiDvpHkqvPgy2l/8Is0yvPQ+I=; b=bvR3IbLDYpTqiFrzPjuuDl3K4hcHCD3e4BoNuhOcOUcC3P0oCKRHgpvH+OQ7LgtZ21XKFIy4dYrtGtmq0x7SMf/LcJWdLVbhBcWtikf6FJlwqt+KJp1Q1hSRI2MYDW04HVIlkYiOFeYbRQYhrNmU3Tj2zY0clxqhm0bZdfEjj5k=; Received: from srv-00-126.mpi-klsb.mpg.de ([139.19.1.29]:38303 helo=zak.mpi-klsb.mpg.de) by hera.mpi-klsb.mpg.de (envelope-from ) with esmtp (Exim 4.72) id 1VZhzM-0000SN-4f; Fri, 25 Oct 2013 16:03:46 +0200 Received: from [74.125.57.233] (port=56350 helo=bozo.muc.corp.google.com) by zak.mpi-klsb.mpg.de (envelope-from ) with esmtpsa (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.72) id 1VZhzL-0002ZV-No; Fri, 25 Oct 2013 16:03:43 +0200 Message-ID: <526A7A3F.2090405@mpi-sws.org> Date: Fri, 25 Oct 2013 16:03:43 +0200 From: Andreas Rossberg User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.0 MIME-Version: 1.0 To: Roberto Di Cosmo CC: Jacques Garrigue , OCaML List Mailing References: <97627FCD-30E1-45AD-A72B-CD423170C0AC@math.nagoya-u.ac.jp> <20131025082911.GB23798@voyager> In-Reply-To: <20131025082911.GB23798@voyager> Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit X-MPI-Local-Sender: true Subject: Re: [Caml-list] Equality between abstract type definitions On 10/25/2013 10:29 AM, Roberto Di Cosmo wrote: > 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. I believe you are mistaken. At least in Standard ML, explicit type variables have always been interpreted as quantified variables, not unification variables. If you try to write fun f(x : 'a) = x + 1 or fun g(x : 'a) = x : 'b that's an error. > 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 (I seem to remember that the Didiers did that in the context of MLF). /Andreas