Re: Polymorphic variants question

From: Jacques Garrigue (garrigue@kurims.kyoto-u.ac.jp)
Date: Wed Apr 26 2000 - 11:34:07 MET DST

  • Next message: Daniel de Rauglaudre: "Camlp4 3.00"

    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>



    This archive was generated by hypermail 2b29 : Wed Apr 26 2000 - 15:41:29 MET DST