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 4345D7EE25 for ; Fri, 25 Oct 2013 16:24:57 +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: AmYDAOB9alKLEwExhGdsb2JhbABZwlyBOA4BAQEKBwQJCRQogiUBAQUnEQgBATYBAQ8LGAkWDwkDAgECASMFHQYBDAEHAQGIA5sAiw2EUwEFjmMGjyAzB4QsnkiOdA X-IPAS-Result: AmYDAOB9alKLEwExhGdsb2JhbABZwlyBOA4BAQEKBwQJCRQogiUBAQUnEQgBATYBAQ8LGAkWDwkDAgECASMFHQYBDAEHAQGIA5sAiw2EUwEFjmMGjyAzB4QsnkiOdA X-IronPort-AV: E=Sophos;i="4.93,570,1378850400"; d="scan'208";a="38793459" 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:24:58 +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=hlI7Lemt7dsxgw6BQEFojhYgpWgOoJPV9fC/xM87DTw=; b=M+wGmsJwsnLyzlZar0I2C3lOrGgMSVAF0sOagb7kpBwMF3ijbmivHNEGo1U5NrwJVhkIR98lWiFDQSTze6uADSNPlGosoxwqYLzBdZ9y9hHqALnGLG0VoXaVFh7ZE71gmaoAzLLiZF+o/cYGx6XLloOLV7ZY/oILfv7epe8cScY=; Received: from zak.mpi-klsb.mpg.de ([139.19.1.29]:38684) by hera.mpi-klsb.mpg.de (envelope-from ) with esmtp (Exim 4.72) id 1VZiJo-0005wV-47; Fri, 25 Oct 2013 16:24:54 +0200 Received: from [74.125.57.233] (port=23950 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 1VZiJn-0003rg-Hs; Fri, 25 Oct 2013 16:24:51 +0200 Message-ID: <526A7F33.6040203@mpi-sws.org> Date: Fri, 25 Oct 2013 16:24:51 +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: Gabriel Scherer , Ivan Gotovchits CC: Roberto Di Cosmo , Jacques Garrigue , OCaML List Mailing References: <97627FCD-30E1-45AD-A72B-CD423170C0AC@math.nagoya-u.ac.jp> <20131025082911.GB23798@voyager> <878uxhd62p.fsf@golf.niidar.ru> In-Reply-To: Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-MPI-Local-Sender: true Subject: Re: [Caml-list] Equality between abstract type definitions On 10/25/2013 01:09 PM, Gabriel Scherer wrote: > However, I think that the current syntax of implicitly-introduced > variables with heuristically-defined scoping rules is bad in any case. > My own toy experiment with explicit syntaxes always use an explicit > binding syntax for both rigid and flexible variables (eg. "forall a b c > in ..." and "some a b c in ..."). In this regard, the ('a 'b . ty) or > (type a) syntaxes are definite improvements -- if only we had applied > those explicit binding forms to GADT constructor types as well... So I > think that even with Andreas' proposed change, people would still be > surprised by things like the following: > > let id : 'a -> 'a = fun x -> x > > let dup (x : 'a) ('a * 'a) = > let result = (x, x) in > (id : 'a -> 'a) result (* fails, while (id : 'b -> 'b) works *) Yes, I agree that implicit scoping is a bit of an ugly hack. That said, I don't expect anybody to be truly surprised about the example above. At least I never heard this being an issue for SML programmers. People probably hardly ever write anything like the above, or avoid shadowing for clarity anyway. /Andreas