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

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

[Beck01, Wolfgang]

> 
> 
> From: "Beck01, Wolfgang" <BeckW@t-systems.com>
> 
> > v1.ml ----------------------------
> > 
> > open Vtop
> > 
> > type t = {
> >     v1_x : int array;
> > }
> > 
> > let init = `V1 { v1_x = [| 0 |] }
> Sure: [| 0 |] creates a mutable data structure, and as such is
> considered as a side-effecting expression. As a result the type of
> init cannot be generalized.

Funnily, I just found a workaround:
v1.ml ----------------------------
open Vtop

type r_t = {
    r_a : int array;
}

type t = {
    v1_x : r_a;
}
let r_init = { r_a = Array.make 100 0 }
let init = `V1 { v1_x = r_init }
----------------------------------
compiles. However, "let init = `V1 { v1_x = { r_a = Array.make 100 0 }} "
does not. 

> 
> OCaml 3.07 is more clever about that, and the above program would be
> accepted with no problem.
> 
Good to hear. I have introduced variants im my major project after playing
around with toy programs like the one above. But I did not check if
arrays would work. After a week of rearranging my code, I successfully
implemented my first real-world variant (without an array). Then, I
started a second one yesterday and was quite upset when I found that
it did not compile (it took me some time to find that arrays were causing
the trouble). 


Regards,

Wolfgang Beck

-------------------
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

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

[Didier Remy]

"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

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

[Frederic De Jaeger]

skaller> They not only allow more accurate typing,
skaller> they're also *faster*. For example,
skaller> consider a restriction of a term type
skaller> in which rewriting rules reduce some 
skaller> sugars to lower level primitive
skaller> (for example macro expansion).

[example skipped]

That's right, in this case they are faster.  But the pattern matching
against polymorphic variants is slightly slower than the
non-polymorphic ones.  The later can be compiled as a parametric
jump. 

Cheers,

  Frédéric De Jaeger

-------------------
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

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

[skaller]

On Wed, 2003-09-10 at 18:18, Jacques Garrigue wrote:
> From: "Beck01, Wolfgang" <BeckW@t-systems.com>

>  In that case we have now polymorphic fields.
>       type mix = {data: 'a. 'a -> 'a ; mutable count: int}
>       let r = {data = (fun x -> x); count = 0}
> 
> So, I think this is a good idea in itself, but before I try again
> introducing this improvement, I need a few compelling examples to
> justify the effort.

Curious: this isn't yet dual to the variants: the field values
are polymorphic, by the record itself is not. Wouldn't one like
to have a record of a set of tags where the typing is like:

	match { `A 1; `B 2 } with
	| { `A x } -> ...

that is, allow subtyping based on tag sets?
[Hmm .. what is the variance of the field values ?]

-------------------
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

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

[skaller]

On Wed, 2003-09-10 at 17:10, Beck01, Wolfgang wrote:
> Didier Remy [mailto:remy@morgon.inria.fr] wrote:
> 
> > 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
> > 
> > [detailed explanation omitted]
> 
> well, I was not aware that compilation of polymorphic variants is an area
> of ongoing research. In the OCaml manual, they are not mentioned under
> "Language extensions" but as a section in the chapter "An introduction to
> Objective Caml". There is a statement
> 
>     "In programs, polymorphic variants work like usual ones. You just
>     have to prefix their names with a backquote character `."
> 
> and this is not true, at least in 3.06. After spending another evening
> with weird type errors, I replaced polymorphic variants with ordinary
> ones. My project looks uglier now since I had to split up some files,
> but at least it compiles and runs.

I use polymorphic variants extensively. Technically, you have to add
the backquote ` and also [] in the type definitions:

	type x = X of int

becomes

	type x = [ `X of int ]

If you do both these changes, everything should work, plus
or minus some casts. Occasionally, you will have to
cast some value using single or double coercions:

	(a:t)   (* annotation only *)
	(a:>t)  (* conversion *)
	(a:u:>t) (* double conversion *)


This is quite rare, but it is sometimes necessary
when you have wildcard matches like:

let f e = 
	match e with
	| `A -> ..
	| _ -> ...

How can the compiler know what the type here really is 
supposed to be? Unlike ordinary variants, the tag `A can
occur in any number of types.

if you now use that expression in a context requiring
type [`A | `B] you'll get an error. Perhaps e contained
the tag `C?

So with polymorphic variants, because the typing is so
flexible, you have to use type
annotations and casts a bit more often than ordinary variants.

The situation is entirely different if your code has an
error in it! In this case, you will often get
vvvvvvvveeeeeeeerrrrrrrryyyyyyy long error messages:
in my case hundreds of lines long usually.

This really is a problem, particularly when the source
of the problem could easily be diagnosed in some
cases: for example a missing tag, or a tag with
an incompatible argument. The compiler *does* detect
some of these cases (but not enough yet).

You are therefore advised to make smaller changes to
your program before recompiling, since then you know
the error is in a place you just changed.

Are polymorphic variants worth it?

For simple uses, the answer is no. However,
in a complex program such as a compiler which
can benefit from a large number of types which
are typing different subsets of a universal term
type, polymorphic variants are indispensible.

They not only allow more accurate typing,
they're also *faster*. For example,
consider a restriction of a term type
in which rewriting rules reduce some 
sugars to lower level primitive
(for example macro expansion).

Either you forgoe a typing in which macros
cannot be in the output type of the rewriting,
or you have to convert all the terms from one
variant type to another like

	match e with 
	| A -> AA
	| B -> BB
	| C i -> CC i
	| Macro x -> f x..
	
which is slower than the polymorphic variant version:

	match e with
	| `Macro x -> f x
	| #nonmacro as x -> x

since there is no need deconstruct and reconstruct
the isomorphic terms, since the isomorphism is
represented by value equality: the same tags

	`A, `B, `C of int

can occur in both the input and output types.



-------------------
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

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

[Jacques Garrigue]

From: "Beck01, Wolfgang" <BeckW@t-systems.com>

> Didier Remy [mailto:remy@morgon.inria.fr] wrote:
> 
> > 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
> > 
> > [detailed explanation omitted]
> 
> well, I was not aware that compilation of polymorphic variants is an area
> of ongoing research. In the OCaml manual, they are not mentioned under
> "Language extensions" but as a section in the chapter "An introduction to
> Objective Caml". There is a statement
> 
>     "In programs, polymorphic variants work like usual ones. You just
>     have to prefix their names with a backquote character `."
> 
> and this is not true, at least in 3.06. After spending another evening
> with weird type errors, I replaced polymorphic variants with ordinary
> ones. My project looks uglier now since I had to split up some files,
> but at least it compiles and runs.

Well the problem discussed above is not one of polymorphic variants,
but of polymorphism in general. And it is about type checking, not
compilation (the latter being pretty trivial).
The relaxed value restriction happens to make life easier with
variants, but this is not its only goal.

There is maybe a misunderstanding on the "work like" bit.
Honestly, if polymorphic variants where "just like" normal variants,
there would be no point in using them. The intended meaning, is that
they have the same operational semantics as normal variants, but the
typing is fully another story. And there are a few warnings in the
manual about the need to write some types if want to avoid an overdose
of polymorphism. Polymorphic variants are not dangerous (actually
they're type safe!) but they can bite if you're not careful.

I understand your disappointment, and just hope you will look again at
this feature after getting more used to the type checker.

Answering to Didier Remy, when I introduced the relaxed value
restriction I intended first to do both improvements simultaneously,
but I stopped short of it for several reasons.
* the improvement you describe would require extensive changes in the
  type checker, as all the work on polymorphism is currently delegated
  to the handling of let.
* the combination with the relaxed restriction makes it even trickier
* in many cases, the relaxed restriction does already the job
* even when this is not the case, this improvement is purely
  syntactic, so you can still expand your definition to solve the
  problem, as Wolfgang discovered himself
* actually there is an exception, if a record type mixes both mutable
  and immutable fields
      type 'a mix = {data: 'a ; mutable count: int}
      let r = {data = (fun x -> x); count = 0}
  There is no solution here, short of changing the type to use a
  reference rather than a mutable field.
  But it might also be the case that you just want to put the identity
  there. In that case we have now polymorphic fields.
      type mix = {data: 'a. 'a -> 'a ; mutable count: int}
      let r = {data = (fun x -> x); count = 0}

So, I think this is a good idea in itself, but before I try again
introducing this improvement, I need a few compelling examples to
justify the effort.

Cheers,

Jacques Garrigue

-------------------
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

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

[Fernando Alegre]

On Wed, Sep 10, 2003 at 09:10:06AM +0200, Beck01, Wolfgang wrote:

>     "In programs, polymorphic variants work like usual ones. You just
>     have to prefix their names with a backquote character `."
> 
> and this is not true, at least in 3.06. After spending another evening
> with weird type errors, I replaced polymorphic variants with ordinary
> ones. My project looks uglier now since I had to split up some files,
> but at least it compiles and runs.

I think polymorphic variants are the trickiest part in OCaml, but once
you understand them, they do indeed work like the usual ones. I found
that when they do not work, it is because I was not defining the types
correctly. Only once I got a very weird behavior, where the compiler
accepted the types but the program failed to link due to unresolved
symbols in a polymorphic variant...

My own experience in one year programming exclusively in OCaml, but
being familiar to both C++ and Lisp before, is something like this:

- 0 months: use either Lisp style (passing functions as arguments
            like crazy, creating complex records of closures and
            do all loops with "let rec"...)
            or C++ style (huge classes with imperative methods,
            for/while loops and extensive use of ";")
            In any case: no inner modules, no functors, no variants
            and, of course, no mli's

- 3 months: realize that most "let rec" can be replaced by X.fold,
            and start adding some inner modules, mli's. Standardize
            data structures, so that all have fold, map, etc..

- 6 months: timidly start using functors, so that cut-and-paste code
            in similar modules is replaced by functor application
            Shorten classes to a few essential methods, and move
            most of the code to functions called from the methods.

- 9 months: Functorize everything! Abstraction, abstraction, abstraction..
            Reduce use of "Open" to the absolute minimum. Move types
            to their own files, and reduce the number of types to the
            few really necessary. Use classes only to simulate polymorphic
            lists, and to interact with lablGtk and lablGl.
            Still no polymorphic variants...

- 12 months: Polymorphic variants everywhere! They make passing data
             between modules so much cleaner...

Fernando

-------------------
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

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

[Beck01, Wolfgang]

Didier Remy [mailto:remy@morgon.inria.fr] wrote:

> 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
> 
> [detailed explanation omitted]

well, I was not aware that compilation of polymorphic variants is an area
of ongoing research. In the OCaml manual, they are not mentioned under
"Language extensions" but as a section in the chapter "An introduction to
Objective Caml". There is a statement

    "In programs, polymorphic variants work like usual ones. You just
    have to prefix their names with a backquote character `."

and this is not true, at least in 3.06. After spending another evening
with weird type errors, I replaced polymorphic variants with ordinary
ones. My project looks uglier now since I had to split up some files,
but at least it compiles and runs.


--
Wolfgang Beck


-------------------
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