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

["Török Edwin" <edwin+ml-ocaml@etorok.net>]

On 01/08/2013 07:19 AM, Jacques Garrigue wrote:
> 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.

Thanks for the detailed explanation, it was very useful.

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

Could some of this be added to the advanced use part of the manual?

> 
>> 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.

Agreed. I don't want any changes to the language either, I'm happy with the way OCaml implement polymorphic variants;
now that I understand more about how it works.

The type errors given by the compiler could provide more details though.
I've opened a bug on mantis with a patch that implements more detailed errors, like:

       Values do not match:
         val foo : [< `A of int | `B of string > `A ] -> unit
       is not included in
         val foo : [< `A of int | `B of string ] -> unit
       Type component [ `A of int ] does not match [< `A of int ]
       Types for tag `A are incompatible: the tag is mandatory in the first type only

       Values do not match:
         val f : [> `Bat of int ] -> int
       is not included in
         val f : [< `Bar of int ] -> int
       Type component [> `Bat of int ] does not match [< `Bar of int ]
       The second variant type is missing mandatory tag(s) `Bat

Best regards,
--Edwin