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=0.4 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id 70648BC37 for ; Wed, 29 Jul 2009 16:39:32 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ApoEAC78b0qFBoIF/2dsb2JhbADUPgEFhBGJbw X-IronPort-AV: E=Sophos;i="4.43,289,1246831200"; d="scan'208";a="33782178" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail1-smtp-roc.national.inria.fr with ESMTP; 29 Jul 2009 16:39:31 +0200 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 56693B603; Wed, 29 Jul 2009 23:39:28 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id CE3C188A3; Wed, 29 Jul 2009 23:39:27 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= date:message-id:to:cc:subject:from:in-reply-to:references :mime-version:content-type:content-transfer-encoding; s=alpha; bh=Wq+xTJjk0vQJeQ2tWpulS7Jc2/I=; b=LVQfotdQPvYRO4QJWqd2+Zhxjmls ICSrbwiidVpt2jwlUGPzxySelryS5MN0JG0uGzL0hsL2bbCN5zfwsCzEI7YqiWuA ZNW5OF65XTO0vwIWDQP5IjD6WprYlON8/Vea7ddIkMce8Dg2Jlk9AtT1Soads/1R EKvwcPlXQY55ehw= DomainKey-Signature: a=rsa-sha1; h=Received:Date:Message-Id:To:Cc:Subject:From:In-Reply-To:References:X-Mailer:Mime-Version:Content-Type:Content-Transfer-Encoding; b=rV81AUndt5LDMYC5U3W4aLvaduI9FkU6ZuSC0+8JXycVYISvq/0+f4B8nJKCLzTMyFComLvh5pQdKmNd+dGDtu4HAhGpgXDTy443BOmbY33igYHRqxCvzF4AXkv2LcKuI6bzjbcPrJJ9QzEDDWbb4LDYD8UwxAHFg5s50k0yBpI=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from localhost (millas [172.16.30.29]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 9630088A2; Wed, 29 Jul 2009 23:39:27 +0900 (JST) Date: Wed, 29 Jul 2009 23:39:28 +0900 (JST) Message-Id: <20090729.233928.59476910.garrigue@math.nagoya-u.ac.jp> To: bohannon@cis.upenn.edu Cc: caml-list@inria.fr Subject: Re: [Caml-list] annotations and type-checking From: Jacques Garrigue In-Reply-To: References: <20090729074050.GK19609@janestcapital.com> X-Mailer: Mew version 6.2 on Emacs 22.3 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 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 toplevel:01 alain's:01 ocaml:01 annotations:01 compiler:01 shinwell:01 toplevel:01 2009:98 28,:98 2009:98 wrote:01 wrote:01 From: Aaron Bohannon > Thank you for that link. To boil it down, it seems (1) type variable= s > 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? If 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". =A0= They 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/a03da53be62c1= 2671a891708c51e85f9.en.html >> >> Mark