Re: [Caml-list] strange type inference for polymorphic variants

[Leo White <lpw25@cam.ac.uk>]

Hi

This is an interesting example of one the problems with how polymorphic 
variants are implemented in OCaml.

However, firstly I must address your confusion over the meaning of [< `A of 
a | `B of a > `A ]. The "> `A" here means that the type must include an `A 
tag. It is a lower bound for the variant types that can be used. Since the 
upper bound of the type ("< `A of a | `B of a") already tells us what type 
the `A tag must have there is no need to include that information in the 
lower bound.

>Here is some simplified code that fails to compile:
># type a = string * string;;
>type a = string * string
># module Bad3 : sig
>  val copy: [< `A of a | `B of a ] -> [< `A of a | `C of a] -> unit
>end = struct
>  let generic (a: [< `A of a | `B of a]) (b: [< `A of a | `C of a]) = ()
>  let specific a b = false
>  let copy a b = match a, b with
>  | `A x, `A y ->
>      if not (specific (`A x) (`A y)) then
>        generic a b
>  | _, _ ->
>      generic a b
>end;;
>Error: Signature mismatch:
>       ...
>       Values do not match:
>         val copy :
>           [< `A of a | `B of a > `A ] -> [< `A of a | `C of a > `A ] -> 
> unit
>       is not included in
>         val copy : [< `A of a | `B of a ] -> [< `A of a | `C of a ] -> 
> unit

The problem here is with how OCaml handles matches with default cases. 
Given the code:

  match foo with
    `Bar x -> x + 1
  | _ -> 0

OCaml will conclude that foo has the type [> `Bar of int]. This means that 
foo must have a type that includes a Bar tag, since Bar is in the lower 
bound of the type.

Conversly, given the code:

  match foo with
    `Bar x -> x +1
  | `Foo -> 0

OCaml will conclude that foo has the type [< `Bar of int | `Foo ]. This 
means that foo does not have to have a type that includes a Bar tag, since 
Bar is only part of the upper bound.

This is why your example includes a spurious "> `A". The match gives "a" 
the type [> `A of a], while the use of "generic" gives "a" the type [< `A 
of a | `B of a], when these are unified they become [< `A of a | `B of a > 
`A].


Interestingly, this problem is actually due to the syntax of OCaml. The 
formal system on which the implementation of polymorphic variants is based 
(see Section 6 of "Programming with Polymorphic Variants" by Jacques 
Garrique) is capable of expressing the type that a match with a default 
case should have. However, the OCaml syntax has no means to express this 
type

In the syntax used in that paper, the example I gave above should actually 
have the type [0 < T | Bar: int]. In other words, "foo" can have any 
variant tags (there are essentially no lower or upper bounds), but if it 
has a Bar tag then that tag has an int type.

I don't think that it would be difficult to use such a type within OCaml, 
but as I said the syntax has no means to express it.

This is also the reason why a type such as [ `A of int or float ] 
(analagous to the [ `A of int & float ] that OCaml does support) can not be 
supported in OCaml.

Personally, I wouldn't mind replacing the current polymorphic variant 
syntax with a more expressive one (and then slowly depreciating the old 
one). However, I imagine most people would consider this too large a change 
for too small a gain.

Regards,

Leo