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

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

Hi Leo and Torok,

A first remark is that a lot is already in the tutorial part of the manual,
with some extra details in the reference part:
http://caml.inria.fr/pub/docs/manual-ocaml-4.00/manual006.html#toc36
http://caml.inria.fr/pub/docs/manual-ocaml-4.00/types.html (Polymorphic variant types)

I agree that while the specification intends to be complete, it may not always
be sufficient to understand all the details.

On 2013/01/07, at 20:28, Leo White <lpw25@cam.ac.uk> wrote:
> 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.

I should explain a bit the rationale behind this behavior, which may seem counter-intuitive.
It is mostly about avoiding accepting meaningless programs.

At some point, OCaml did give the type [< `Bar of int | … ] to the first example, meaning that
`Bar is accepted but not required, and there may be other tags.
This actually avoided Torok's problem: [< `Bar of int | `Foo] was an instance of [ `Bar of int | … ].
However, there was a major drawback: it was extremely weak to typos.
For instance
  let f (x : [`Bar of int | `Foo]) = match x with `Bat y -> y | _ -> 3
would be accepted, but return always 3…

So I decided to remove the [< `Bar of int | … ] from the type algebra.
This means that at some point, one has to choose between [>  `Bar of int] (which allows
extra constructors, but requires `Bar), and [< `Bar of int | `Foo] (where `Foo could be replaced
by any concrete list of constructors).
Currently, this is done just after typing all the patterns.
If at that point you know the exhaustive list of tags, you get a [< something] type,
otherwise you get a [> something] type.
Note that type annotations outside of patterns are ignored for that; you should
write:
   let f = function (`Bar x : [< `Bar of _ | `Foo]) -> x | _ -> 3

> 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 omission in the syntax is intentional: this is the semantics we want to avoid.
The inability to catch typos seems to be too high a cost.
Another thing we do not allow in OCaml is empty variant types: you cannot unify [< `A] with [< `B].
Again, empty variant types could have applications, but the rationale is that usually this should be seen
as an error.

Jacques Garrigue