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

[Jacques Garrigue <garrigue@kurims.kyoto-u.ac.jp>]

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