Re: Polymorphic variants question

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

From: Brian Rogoff <bpr@best.com>

>  class type ['a] a = object method do_a : int method downcast : 'a end
[...]
> If we replace the variant with a polymorphic variant. 
> type objsum = [`A of objsum a | `B of objsum b];;
> 
> and then we do the same thing as before the type checker complains. 
> 
> # class test_a =
>     object (s)
>       method downcast = `A (s :> objsum a)
>       method do_a = 1
>     end;;
> # Characters 6-103:
> # Some type variables are unbound in this type:
> # class test_a : object method do_a : int method downcast : #objsum[>`A]
> end
> # The method downcast has type #objsum[>`A] where 'a is unbound
> 
> This is a good error message, and it tells me what to do to fix the
> problem right away: I add an annotation to constrain that "#objsum[>`A]" 
> 
> Now, in order to avoid surprises in the future, can someone tell me why I
> should have expected that type "#objsum[>`A]" to be computed, and hence known
> that I would need to constrain the type? It makes sense, but I don't yet
> have a good mental model for the typing of polymorphic variants
> which would have allowed me to write the correct version immediately. How 
> do the experts go about mentally inferring the right types in cases like
> this?

Variant typing can be quite subtle, so I suggest that you read my ML
workshop paper. This is the first one in the list at
        http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/
A simpler document is olabl's manual
        http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/
What OCaml 3 does is even more complicated, but the explanations in
these papers should be more intuitive.

The idea is that a variant type is the combination of 3 components:

* a list of pairs tag/type giving the type of the argument for each
  constructor.
* a lower bound, that is the list of tags any matching on this variant
  must handle. This appears after the ">" in types.
* an upper bound, that is the list of tags one may add to this type.
  This appears after the "<" in types. When there is a ">" and no "<"
  in a variant type the upper bound is open: you may add anything.

To print types in a reasonably compact way, the actual syntax of types
mangles that a bit: if there is no upper bound, argument types are
printed inside the lower bound, otherwise they are printed in the upper
bound.

Your example is a bit hard to follow, but here is what happens:
* since you coerce (s) to (objsum a), it is given the type (#objsum #a)
  (a is covariant in its parameter).
* since (s) is the object itself, this constrains downcast to return a
  result of type (#objsum), which actually represents an upper bound:
  [< `A of objsum a | `B of objsum b]
* as downcast returns actually (`A ...), there is also a lower bound
  constraint: [< `A of objsum a | `B of objsum b > `A].
* since the lower bound {`A} is smaller than the upper bound {`A,`B},
  this type is polymorphic: it can be instantiated either in
  (objsum), i.e. [`A of objsum a | `B of objsum b], or in
  [`A of objsum b] (dropping the `B).

Hope it helps,

        Jacques
---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>