[Caml-list] strange type inference for polymorphic variants

[Caml-list] strange type inference for polymorphic variants

[Török Edwin]

Hi,

If I use a polymorphic variant in a match case that has a _ branch then I get an "interesting" type inferred,
 for example: [< `A of a | `B of a > `A ], instead of: [< `A of a | `B of a ].
To make it work I have to list all possibilities instead of _, _.

I always use `A with a parameter of type a, it seems strange that OCaml would infer `A without a parameter.
Also the inferred type ([< `A of a | `B of a > `A ]) does actually accept both [`A of a] and [`B of a] as input,
and doesn't accept `A without a parameter, so what is the difference between the inferred type and the one I wrote in the signature
([< `A of a | `B of a])?

Here is some simplified code that fails to compile:

$ ocaml
        OCaml version 4.00.1

# 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


And here is some code that works:
module OK : 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 when specific (`A x) (`A y) -> ()
    | (`A _ | `B _), (`A _ | `C _ ) ->
      generic a b
end;;

Here are a few other ways to write the same code which result in an error:
module Bad1: sig
  val test: [< `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: [`A of a]) (b:[`A of a]) = false
  let test a b =
    let use_specific = match a, b with
      | `A x, `A y -> specific (`A x) (`A y)
      | _, _ -> false in
    if not use_specific then
      generic a b;;
end;;

module Bad2 : 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: [`A of a]) (b:[`A of a]) = false
  let copy a b = match a, b with
    | `A x, `A y when specific (`A x) (`A y) ->
        ()
    | _, _ ->
        generic a b
end;;

Best regards,
--Edwin

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

[Leo White]

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

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

[Török Edwin]

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

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

[Jacques Garrigue]

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

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

[Török Edwin]

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