Polymorphic variants question

From: Brian Rogoff (bpr@best.com)
Date: Wed Apr 26 2000 - 02:25:09 MET DST

  • Next message: John Prevost: "Re: Objective Caml 3.00 released"

    Hi,

    A long time ago John Prevost posted a nice trick to get a kind of
    downcasting in OCaml

    class type ['a] super =
      object
        method downcast : 'a
      end;;

    class type ['a] a =
      object
        inherit ['a] super
        method do_a : int
      end;;

    class type ['a] b =
      object
        inherit ['a] super
        method do_b : float
      end;;

    type objsum = A of objsum a | B of objsum b;;

    Which have types

    # class type ['a] super = object method downcast : 'a end
    # class type ['a] a = object method do_a : int method downcast : 'a end
    # class type ['a] b = object method do_b : float method downcast : 'a
    end
    # type objsum = A of objsum a | B of objsum b

    And to show that it works, he gave the following test code:

    class test_a =
        object (s)
          method downcast = A (s :> objsum a)
          method do_a = 1
        end;;
      class test_b =
        object (s)
          method downcast = B (s :> objsum b)
          method do_b = 1.0
        end;;

    # class test_a : object method do_a : int method downcast : objsum end
    # class test_b : object method do_b : float method downcast : objsum end

    and so on, testing that this meets assumptions.

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

    # class test_a =
      object (s)
        method downcast : objsum = `A (s :> objsum a)
        method do_a = 1
      end;;
      class test_b =
        object (s)
          method downcast : objsum = `B (s :> objsum b)
          method do_b = 1.0
        end;;

    # class test_a : object method do_a : int method downcast : objsum end
    # class test_b : object method do_b : float method downcast : objsum end

    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?

    -- Brian



    This archive was generated by hypermail 2b29 : Wed Apr 26 2000 - 08:47:13 MET DST