From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 322DFBBAF for ; Wed, 2 Aug 2006 09:00:22 +0200 (CEST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id k7270Lgo001704 for ; Wed, 2 Aug 2006 09:00:21 +0200 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id JAA07750 for ; Wed, 2 Aug 2006 09:00:21 +0200 (MET DST) Received: from smtp6-g19.free.fr (smtp6-g19.free.fr [212.27.42.36]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id k7270KE8001699 for ; Wed, 2 Aug 2006 09:00:21 +0200 Received: from [192.168.0.1] (rke75-3-82-229-183-156.fbx.proxad.net [82.229.183.156]) by smtp6-g19.free.fr (Postfix) with ESMTP id 899FD22531; Wed, 2 Aug 2006 09:00:20 +0200 (CEST) Message-ID: <44D04D83.5020503@inria.fr> Date: Wed, 02 Aug 2006 09:00:19 +0200 From: Alain Frisch User-Agent: Thunderbird 1.5.0.4 (X11/20060614) MIME-Version: 1.0 To: Remi Vanicat Cc: "O'Caml Mailing List" , Chris King Subject: Re: [Caml-list] Unexpected '_a problem References: <875c7e070608011347y62d2dd21lc55390cd4ffd00a1@mail.gmail.com> <004801c6b5b0$47811030$15b2a8c0@wiko> <6b8a91420608011509s696233cew8d499f315aa0cba9@mail.gmail.com> In-Reply-To: <6b8a91420608011509s696233cew8d499f315aa0cba9@mail.gmail.com> X-Enigmail-Version: 0.94.0.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 44D04D85.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 44D04D84.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; frisch:01 frisch:01 val:01 wwwfun:01 reformulate:01 semantically:01 forall:01 syntactical:01 generalizing:01 forall:01 principality:01 ocaml:01 wrote:01 polymorphic:01 caml-list:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 Remi Vanicat wrote: > But for a reson I don't > fully understood, one cannot do: > > # let f () (_ : 'a -> unit) = ();; > val f : unit -> ('a -> unit) -> unit = > # f ();; > - : ('_a -> unit) -> unit = See the paper _Relaxing the value restriction_ by Jacques Garrigue ( http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/morepoly-long.pdf ), page 15: dangerous type variables (which are not generalized when the right-hand side of the let-binding is not a value) are not only those is contravariant position - this would be enough to ensure type soundness - but also those which appear in a contravariant branch (e.g. anywhere on the left of an arrow) - this is necessary to ensure that the type system has principal types. Let me reformulate the example given in the paper. Consider the top-level binding: let f = print_newline (); fun x -> raise Exit Semantically, it would be sound to give g a polymorphic type: \forall 'a,'b. 'a -> 'b. However, the relaxed value restriction does not try to be that clever; it decides which variables to generalize only by looking at the type of the bound expression (when it is not a syntactical value). Here are two possible types for the expression: 'a -> 'b ('c -> 'd) -> 'b Generalizing all variables in covariant positions would give these two type schemes: \forall 'b. 'a -> 'b ('a monomorphic) \forall 'b,'c. ('c -> 'd) -> 'b ('d monomorphic) The only type-scheme which is more general than these two would be \forall 'a,'b. 'a -> 'b, but this one is not ok (a contravariant variable has been generalized). To retrieve principality, the type system has been designed so that the variable 'c above would not be generalized (it is on the left of an arrow), which makes the type scheme \forall 'b. ('c -> 'd) -> 'b less general than \forall 'b. ('a -> 'b) (which is the principal type scheme inferred by OCaml). -- Alain