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 59B357EE42 for ; Sun, 27 Oct 2013 13:07:58 +0100 (CET) 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: AowDALcBbVKLEwExhGdsb2JhbABZrlCUIoEyDgEBAQoHBAkJFCiCJQEBBAEnGQEBNwEECwsYLlcZiAEGBKRchFMBBY4pBo8iMweDH4ENrTs X-IPAS-Result: AowDALcBbVKLEwExhGdsb2JhbABZrlCUIoEyDgEBAQoHBAkJFCiCJQEBBAEnGQEBNwEECwsYLlcZiAEGBKRchFMBBY4pBo8iMweDH4ENrTs X-IronPort-AV: E=Sophos;i="4.93,580,1378850400"; d="scan'208";a="32073745" 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; 27 Oct 2013 13:07:57 +0100 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=4xtf1O7hpyNUzMh1Yljmco/YOlMv2Yr0+N32pHGMgNo=; b=oQc7kjpo814WHZDMJuTsQoNj0sUWNXyxS+HRcVheb1CfvmZyC5Gvxb2XCXzcs6iPQOoioD+5s1Tv/wxoizLPuoQ15+LRPN0ePjgCwTvQsC6IamX1qfYbIE2Po2sSTiUZjCwQAZoE/bQXSO4HkNflnpYzhuDs+A670Of9JuB9f9E=; Received: from zak.mpi-klsb.mpg.de ([139.19.1.29]:48205) by hera.mpi-klsb.mpg.de (envelope-from ) with esmtp (Exim 4.72) id 1VaP8M-0001pN-Un; Sun, 27 Oct 2013 13:07:57 +0100 Received: from mnch-5d856b49.pool.mediaways.net ([93.133.107.73]:54400 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 1VaP8M-0003AJ-EF; Sun, 27 Oct 2013 13:07:54 +0100 Mime-Version: 1.0 (Mac OS X Mail 6.6 \(1510\)) Content-Type: text/plain; charset=iso-8859-1 From: Andreas Rossberg In-Reply-To: <526BFCCA.8080804@inria.fr> Date: Sun, 27 Oct 2013 13:07:54 +0100 Cc: caml-list@inria.fr, Francois Pottier Content-Transfer-Encoding: quoted-printable Message-Id: References: <97627FCD-30E1-45AD-A72B-CD423170C0AC@math.nagoya-u.ac.jp> <20131025082911.GB23798@voyager> <526A7A3F.2090405@mpi-sws.org> <526BFCCA.8080804@inria.fr> To: Didier.Remy@inria.fr X-Mailer: Apple Mail (2.1510) X-MPI-Local-Sender: true Subject: Re: [Caml-list] Equality between abstract type definitions On Oct 26, 2013, at 19:32 , Didier Remy wrote: >>> 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). >=20 >> 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 >=20 > Andreas, I am not sure what point you are trying to make. >=20 > Sure, the name "unification variable" is misleading and should not be used > here, as it refers to the algorithm. Instead, one should call them flexib= le > type variable or whatever that refers to the specification. >=20 > Still, flexible variables make a lot of sense in the specification (even > if not often done in formal presentations). Oh, I agree. I was merely questioning that all explicit type variables in M= L would naturally be flexible variables, which was what I was reading into = Roberto's reply (if you take the preceding paragraph from his post as conte= xt). Sure, flexible variables are easy (and useful) to add, but technically= speaking they are an extension, i.e., require extra rules. Or would you no= t say so? And yes, I want to have both forms of variables/bindings, as I suggested in= my original post. My main concern with the current state of affairs in OCa= ml is that implicitly interpreting 'a as the flexible kind obviously is sur= prising to many people, arguably because it is somewhat inconsistent. Espec= ially when rigid probably is the more common use case. > 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: >=20 > G |- M ['a <- t] : s > ----------------------- > G |- for some 'a. M : s >=20 > Fran=E7ois and I discuss this and formalize it in our chapter "The Essenc= e of > ML Type Inference" in "Advanced Topics in Types and Programming". Ah, yes, thanks for the reminder. >> (I seem to remember that the Didiers did that in the context of MLF). >=20 > Yes, since we needed more annotations in MLF because all function paramte= rs > 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: >=20 > for some 'u, for all 'a, 'b, ('a -> 'b) -> 'a * 'u -> 'b * 'v >=20 > 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. >=20 > We found this necessary in MLF, but it would also be quite useful in OCam= l. Yes, makes sense. I suppose the main obstacle is retrofitting a nice syntax= into OCaml. /Andreas