RE: [Camllist] strange behaviour with variants and "cannot be g eneralized"

Beck01, Wolfgang
 Didier Remy
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20030909 (19:13) 
From:  Didier Remy <remy@m...> 
Subject:  Re: [Camllist] strange behaviour with variants and "cannot be g eneralized" 
"Beck01, Wolfgang" <BeckW@tsystems.com> 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 valueonly 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 valueform, 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 wellknown(?) improvement of valueonly 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 nonvalues more carefully. Namely, Type variables appearing in the type of exposed nonvalue forms cannot be generalized. For simplication take nonvalue forms to be aplications nodes. Exposed nonvalue forms are nonvalue 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 nonvalue 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 nonvalue 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 (* nonvalue 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 valuerestriction. Fortunately, the formulation above avoids this decomposition beforehand and can actually be implemeted at no extra cost. 3) Jacques Garrigue "Relaxed valuerestriction".  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 contravariant 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.kyotou.ac.jp/~garrigue/papers/  To unsubscribe, mail camllistrequest@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/camlbugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners