Polymorphic variants question

Polymorphic variants question

[Brian Rogoff]

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

Re: Polymorphic variants question

[Jacques Garrigue]

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>

Re: Polymorphic variants question

[Chris King]

On 9/1/06, David Allsopp <dra-news@metastack.com> wrote:
> Now, if I try to constrain it to what I'm after with
> 
> let (f : [`A | `C] -> bool * [`A | `B | `C]) = fun x -> ...
> 
> then I get a type error unless I change
> 	(false, x)
> to
> 	(false, id x)
> with 
> 	let id = function `A -> `A | `C -> `C
> 
> Is there a better way of writing this?

Yes, you can use the coercion operator to tell the compiler to expand the type of x to include `B:

# let f (x: [`A | `C]) = if x = `A then (true, `B) else (false, (x :> [`A | `B | `C]))
val f : [ `A | `C ] -> bool * [ `A | `B | `C ] = <fun>

Perhaps someone else can clarify how this accomplishes the same thing as your id function, as my understanding of type theory is somewhat rudimentary.

- Chris King

Polymorphic variants question

[David Allsopp]

Forgive the potentially obvious question --- I'm not very familiar with
polymorphic variants but I think that they're what I want in this situation!

Suppose I'm dealing with three constructors `A, `B and `C and I have a
function f that's supposed to take either `A or `C and return any of `A, `B
or `C. If I write:

let f x = if x = `A then (true, `B) else (false, x)

then I get the type

val f : ([> `A | `B] as 'a) -> bool * 'a

Now, if I try to constrain it to what I'm after with

let (f : [`A | `C] -> bool * [`A | `B | `C]) = fun x -> ...

then I get a type error unless I change
	(false, x)
to
	(false, id x)
with 
	let id = function `A -> `A | `C -> `C

Is there a better way of writing this? I'm using this in the context of
several interrelated lexers where `A, `B and `C are high-level states and
certain lexers can only be called in a subset of those states but each lexer
may yield any value for the next-state. I'd quite like to eliminate the id x
bit since it's only there to "separate" x from the return value for the
type-checker.

Thanks!


David