From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id VAA03034; Tue, 9 Sep 2003 21:13:30 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f 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 VAA12847 for ; Tue, 9 Sep 2003 21:13:29 +0200 (MET DST) Received: from morgon.inria.fr (morgon.inria.fr [128.93.8.33]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id h89JDRf06086; Tue, 9 Sep 2003 21:13:27 +0200 (MET DST) Received: (from remy@localhost) by morgon.inria.fr (8.11.6/8.11.6) id h89JHLp31365; Tue, 9 Sep 2003 21:17:21 +0200 To: "Beck01, Wolfgang" Cc: caml-list@inria.fr Subject: Re: [Caml-list] strange behaviour with variants and "cannot be g eneralized" References: From: Didier Remy Date: 09 Sep 2003 21:17:20 +0200 In-Reply-To: Message-ID: User-Agent: Gnus/5.0808 (Gnus v5.8.8) Emacs/20.7 MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Loop: caml-list@inria.fr X-Spam: no; 0.00; caml-list:01 didier:01 morgon:01 t-systems:01 compiles:01 3.06:01 orthogonal:01 implemented:01 3.07:01 3.06:01 implemented:01 monomorphic:01 abstraction:01 constants:01 abstraction:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk "Beck01, Wolfgang" writes: > Funnily, I just found a workaround: [... Example simplified...] > "let tmp = ref 0 let init = `V = tmp" compiles. > However, "let init = `V (ref 0)" does not. Yes, this may look funny... but it is all but far from a hasardous joke. Here is some explanation of 1) what happened in version 3.06 and 2) how this is related to a relaxed form of value restriction, 3) which is actually orthogonal to the solution implemented in 3.07 1) The strict value restriction. -------------------------------- When typing let x = e1 in e2, the value-only restriction says. If e1 is not a value, then the type of e1 cannot be generalized. This is what 3.06 implemented. In your example e1 is of the form `V e3 where e3 is not a value. Hence e1 is not a value and the type of `V (e3) is not generalized. However, in the expression let v3 = e3 in let x = `V v3 in e2 `V v3 is a value-form, hence its type may be generalized. Note that v3 itself cannot be generalized, but it happens to be monomorphic. Hence the type of `V v3 can be generalized in e2. 2) A well-known(?) improvement of value-only restriction. --------------------------------------------------------- Instead of enabling/disabling generalization for let expressions in a binary manner, we may only disable generalization of type variables may end in the type of a fresh piece of store by analyzing non-values more carefully. Namely, Type variables appearing in the type of exposed non-value forms cannot be generalized. For simplication take non-value forms to be aplications nodes. Exposed non-value forms are non-value forms that are not under an abstraction. For example, in the expression ((c1 c2) (fun x -> (c3 c4))), (fun x -> x)) where c1, .. c4 are constants, the exposed non-value forms are the two application nodes: "(c1 c2)" and and "(c1 c2) (fun x -> (c3 c4))" The application node (c3 c4) is under an abstraction and thus not exposed. The two abstractions and the pairing nodes are value forms. For intuition, consider an experssion e1 = e1'[e11] where e1'[z11] is a value for some fresh variable z1. Then, the expression let x = e1 in e2 is semantically equivalent to let "z1 = e11 in e1'[z1] in a2". Hence, the former can be typed as the latter. That is, since e1'[z] is a value, all variables of e1'[z] can be generalized except those that could not be generalized in the type of z1, i.e. those that cannot be generalized in e11. To get the generalized rule, just simultaneously all toplevel non-value parts e1k of e1 and bind them to variables zk: let z1 = e11 in ... let zk = e'k in e1'[z1, ... zk] in a2 Then, recursively decompose each e11, ... e1k. For instance, the full decomposition of Wolfgang's (simplified) example is: let z11 = 0 in (* value *) let z1 = ref z11 in (* non-value node but monomorphic *) let x = `V z1 in (* value, hence generalizable *) e2 In short, this decomposition could be virtually done by the typechecker in order to relax the value-restriction. Fortunately, the formulation above avoids this decomposition beforehand and can actually be implemeted at no extra cost. 3) Jacques Garrigue "Relaxed value-restriction". ----------------------------------------------- OCaml 3.07 uses the "relaxed value restriction" proposed by Jacques Garrigue [1]. This claims that variables that occurs only positively can always be generalized, Hence (1) becomes: If e1 is not a value, then type variables that occur (at least) once on the contra-variant side of a type constructor cannot be generalized. Here, the intuition is that although these variables can appear in the type of memory cells allocated during the evaluation of e1 these cells can never be updated outside of e1. When typechecking let x = `V e3 in e2 with this rule, the type of `V e3 can again be generalized in e2, since although `V v3 is not a value, the only variable ('a) appearing in its type ([> `V1 of t] as 'a) appears only once at at occurrence 0. ---------------- In summary, your example can be solved either by (2) [known for a long time, but not implemented in OCaml] or (3) [recent, implemented in 3.07]. This note is also to remark that (2) and (3) are both independent and complementary. Wolfgang's example happens to be at the intersection of (2) and (3), hence his successful trick in 3.06 and the successful typechecking in 3.07. So, maybe (2) would still be worth implementing some day... -Didier [1] Relaxing the value restriction. Jacques Garrigue. August 2003. http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/ ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners