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=2.8 required=5.0 tests=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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id A09CEBC37 for ; Wed, 29 Jul 2009 15:41:35 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AsIBAIbub0pKfVwZimdsb2JhbACZS0EBCgkMBxEFqTgzhz+ISAEDAgSEDQWIIw X-IronPort-AV: E=Sophos;i="4.43,289,1246831200"; d="scan'208";a="30539018" Received: from qw-out-2122.google.com ([74.125.92.25]) by mail2-smtp-roc.national.inria.fr with ESMTP; 29 Jul 2009 15:41:35 +0200 Received: by qw-out-2122.google.com with SMTP id 3so448625qwe.33 for ; Wed, 29 Jul 2009 06:41:34 -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=AI1kifm0WIBEGSe7ehNLlpOAULdpyWLfQnpCcOE0Tv0=; b=K8sn2Wgxzd1dyZJ0r9DIawYliVVwWjYjDuONIqhbpimgXstm5h/tjDAlRfL2Zb0ybL nudYj14DyD4xfeUJExZhIKnUtYIpTAZBDozxd5X87VJ0ZED0UpECxOCYjSS1IHCpJuMJ fCm62h6c2cRW3C1UPnlhNYsh1OI0aydKNeTRI= 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=YoNnp0fzVof4eSl4e7zyznQBGiGTC7j/BsDc0jK38cTgLjmuJ7+S6OmAjjL4F3BO3l BD5OTPKQA1qnbgymckJmLxyBLfJsEw1gGJCCDmwMmffXnafhwIaHmuz+CwUsFuaSw2HU QjlZiI6swORQjQTAmWx4XpP0OPQWAYgBj1O0g= MIME-Version: 1.0 Sender: aaron678@gmail.com Received: by 10.220.95.206 with SMTP id e14mr5472330vcn.34.1248874894359; Wed, 29 Jul 2009 06:41:34 -0700 (PDT) In-Reply-To: <20090729074050.GK19609@janestcapital.com> References: <20090729074050.GK19609@janestcapital.com> Date: Wed, 29 Jul 2009 09:41:34 -0400 X-Google-Sender-Auth: 581706f0a07a80b1 Message-ID: Subject: Re: [Caml-list] annotations and type-checking From: Aaron Bohannon To: Mark Shinwell 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 bindings:01 ill-formed:01 ocaml:01 annotations:01 compiler:01 shinwell:01 toplevel:01 2009:98 28,:98 2009:98 wrote:01 wrote:01 upenn:01 caml-list:01 Thank you for that link. To 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). So if OCaml cannot do anything better than this, then why are type variables even syntactically legal in annotations? If backwards compatibility is the issue, could it not at the very very least give a compiler warning when they are used? - Aaron 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". =A0The= y are > not generalized until the type of the whole toplevel declaration has been > determined. =A0Consequentially, during type-checking of the body of your > 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/a03da53be62c12671a= 891708c51e85f9.en.html > > Mark >