Re: [Caml-list] strange behaviour with variants and "cannot be g eneralized"

[Didier Remy <remy@morgon.inria.fr>]

"Beck01, Wolfgang" <BeckW@t-systems.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 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