From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.9 required=5.0 tests=AWL,DNS_FROM_RFC_POST, SPF_NEUTRAL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 0DD5DBC37 for ; Wed, 29 Jul 2009 18:50:26 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AvcBAFoacErRVd24mGdsb2JhbACZS0EBAQEICQwHE6oLM4c8iEgBAwIEhA0FiCOBRw X-IronPort-AV: E=Sophos;i="4.43,289,1246831200"; d="scan'208";a="31858238" Received: from mail-qy0-f184.google.com ([209.85.221.184]) by mail3-smtp-sop.national.inria.fr with ESMTP; 29 Jul 2009 18:50:25 +0200 Received: by qyk14 with SMTP id 14so1382009qyk.1 for ; Wed, 29 Jul 2009 09:50:24 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:sender:received:in-reply-to :references:date:x-google-sender-auth:message-id:subject:from:to:cc :content-type:content-transfer-encoding; bh=42H8eddPN1rF7OREIo7dySnItkK/w99AULdogc9R+uY=; b=U8B2QDvdI74Oc+Jf7rGl8TZ9opPJ2uwMSBixu+PAXoq8av7NFxO2gl7a/v9fl3HxKs STdmVK4TgMLO6B+h/kB4wXxP/uVa51YQ/e8wa8KrfbH/hC9oRUSqN/gO+4F0zEhrBPwC RZejeU3Rryg5cmNDCIGbjKpKhjmnH0v8eh4iI= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type :content-transfer-encoding; b=XURBRgetaNkt56XiFPD4eUKimuDUtVVonVFh+HRRj09yHu9v9uB9jTJcNTr3/660ov n+7/pWPX0xM9xaWR0xOgxv03/LXcTQ5njCVEMNKbghyVwsu8G+ybqyvpCsZCgWYafkcF THAPDjHjnHCd8VbcC1B5ihyqOH+OD7lFmTLcI= MIME-Version: 1.0 Sender: aaron678@gmail.com Received: by 10.220.86.70 with SMTP id r6mr550vcl.70.1248886224490; Wed, 29 Jul 2009 09:50:24 -0700 (PDT) In-Reply-To: <20090729.233928.59476910.garrigue@math.nagoya-u.ac.jp> References: <20090729074050.GK19609@janestcapital.com> <20090729.233928.59476910.garrigue@math.nagoya-u.ac.jp> Date: Wed, 29 Jul 2009 12:50:24 -0400 X-Google-Sender-Auth: ef463d182a11bad8 Message-ID: Subject: Re: [Caml-list] annotations and type-checking From: Aaron Bohannon To: Jacques Garrigue Cc: caml-list@inria.fr Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Spam: no; 0.00; annotations:01 annotations:01 type-checker:01 bindings:01 ill-formed:01 toplevel:01 alain's:01 ocaml:01 compiler:01 shinwell:01 toplevel:01 2009:98 2009:98 28,:98 polymorphic:01 Yes, I was completely wrong. Type variables do prevent me from writing let f (x : 'a -> 'a) : 'a =3D x;; and let f (x : 'a) (y : 'a) : int =3D 3 in f true "true";; So they are certainly not meaningless. But I use annotations primarily to get better, more accurately located error messages from the type-checker, and apparently annotating functions that are (intended to be) polymorphic is never useful for this purpose. And it boggles my mind that annotations with type variables *prevent* generalization. But at least by now, I guess anyone following this discussion should know whether this program type-checks... ;) let f (x : 'a -> unit) : unit =3D () in f print_string; let g (y : 'a -> unit) : unit =3D () in g print_float ;; - Aaron On Wed, Jul 29, 2009 at 10:39 AM, Jacques Garrigue wrote: > From: Aaron Bohannon >> Thank you for that link. =A0To boil it down, it seems (1) type variables >> annotating top-level declarations are ignored, and (2) type variables >> annotating local bindings are treated existentially (as if one had >> written '_a, although that name itself is considered syntactically >> ill-formed). > > Point (1) is wrong. They are not ignored, they act as constraints. > Actually, their behaviour is uniform: they are always bound and > generalized at toplevel. This is true both for normal functions an > classes. The only exception is with modules, but it is not surprising > as modules work on a different level. > > I can see only one really buggy behaviour in Alain's mail, the fact > that local modules did flush type variables. Fortunately, this has > been corrected. > >> So if OCaml cannot do anything better than this, then why are type >> variables even syntactically legal in annotations? =A0If backwards >> compatibility is the issue, could it not at the very very least give a >> compiler warning when they are used? > > Because it is useful to be able to have type annotations sharing type > variables in different places in a term (for instance for different > arguments). > > Jacques Garrigue > >> On Wed, Jul 29, 2009 at 3:40 AM, Mark >> Shinwell wrote: >>> On Tue, Jul 28, 2009 at 05:47:25PM -0400, Aaron Bohannon wrote: >>>> Why do the first two programs type-check but the thrid one does not? >>> >>> Dark corners of the type system. >>> >>>> let f (x : 'a) : 'a =3D x in (f true, f 3);; >>> >>> Explicit type variables in this situation are considered "global". =A0T= hey are >>> not generalized until the type of the whole toplevel declaration has be= en >>> determined. =A0Consequentially, during type-checking of the body of you= r >>> let expression, 'a is not a generalized variable. >>> >>> There is more detail on similar situations here: >>> >>> http://caml.inria.fr/pub/ml-archives/caml-list/2002/06/a03da53be62c1267= 1a891708c51e85f9.en.html >>> >>> Mark >