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

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

On 01/07/2013 01:28 PM, Leo White wrote:
> 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.

Thanks, I didn't see this explain in the manual.

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

Thanks, that type makes sense now.
Could the compiler be improved to realize that [< `A of a | `B of a > `A] and [< `A of a | `B of a] are the same type?

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

Will read.

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

Best regards,
--Edwin