[Caml-list] polymorphic variants in match statements

[Caml-list] polymorphic variants in match statements

[Milan Stanojević]

Hi, we're trying to understand the type inference with polymorphic
variants in match statements. This is a simplification of an actual
case that happened in practice.

1)
let f i a =
  match i, a with
  | true, `A -> `B
  | false, x -> x

fails with
File "foo.ml", line 4, characters 16-17:
Error: This expression has type [< `A ]
       but an expression was expected of type [> `B ]
       The first variant type does not allow tag(s) `B

2) changing false to _
let f i a =
  match i, a with
  | true, `A -> `B
  | _, x -> x

this succeeds with
val f : bool -> ([> `A | `B ] as 'a) -> 'a

3) changing x in (1) to _ , and using a on the right side
let f i a =
  match i, a with
  | true, `A -> `B
  | false, _ -> a

this fails in the same way as (1)

4) finally adding another case to match statement
let f i a =
  match i, a with
  | true, `A -> `B
  | false, x -> x
  | true, x -> x

this succeeds with the same type as (2)


So it seems there is some interaction between type inference and
exhaustivnest of the match statements.

Can someone shed some light on what is going on here?

Re: [Caml-list] polymorphic variants in match statements

[Jacques Garrigue]

On 2012/01/24, at 9:53, Milan Stanojević wrote:

> Hi, we're trying to understand the type inference with polymorphic
> variants in match statements. This is a simplification of an actual
> case that happened in practice.
> 
> 1)
> let f i a =
>  match i, a with
>  | true, `A -> `B
>  | false, x -> x
> 
> fails with
> File "foo.ml", line 4, characters 16-17:
> Error: This expression has type [< `A ]
>       but an expression was expected of type [> `B ]
>       The first variant type does not allow tag(s) `B
> 
> 2) changing false to _
> let f i a =
>  match i, a with
>  | true, `A -> `B
>  | _, x -> x
> 
> this succeeds with
> val f : bool -> ([> `A | `B ] as 'a) -> 'a
> 
> 3) changing x in (1) to _ , and using a on the right side
> let f i a =
>  match i, a with
>  | true, `A -> `B
>  | false, _ -> a
> 
> this fails in the same way as (1)
> 
> 4) finally adding another case to match statement
> let f i a =
>  match i, a with
>  | true, `A -> `B
>  | false, x -> x
>  | true, x -> x
> 
> this succeeds with the same type as (2)
> 
> 
> So it seems there is some interaction between type inference and
> exhaustivnest of the match statements.
> 
> Can someone shed some light on what is going on here?

Indeed. The basic idea is to close variant types when leaving them
open would make the pattern matching non-exhaustive.
Here, if we assume that a has type [`A | `B], then the pattern-matching
becomes non-exhaustive, so the type inferred is just [`A]
(i.e. the list of all constructors appearing inside the patterns at this position).

Actually, the theory is a bit more complicated, and the full details are
in the following paper, but you should just expect the above behavior
in practice.

	Typing deep pattern-matching in presence of polymorphic variants.
	http://www.math.nagoya-u.ac.jp/~garrigue/papers/index.html

Note that there is also another way to make (1) type, without adding
new cases

  let f i a =
    match i, a with
    | true, `A -> `B
    | false, (`A as x) -> x;;
  val f : bool -> [< `A ] -> [> `A | `B ] = <fun>

Here we have removed the connection between a and the output,
allowing `A to be combine with `B without changing the type of a.

Hope this helps.

Jacques Garrigue

Re: [Caml-list] polymorphic variants in match statements

[Milan Stanojević]

Thanks a lot, Jacques!
This helped my understanding a lot.

I only wonder if maybe this (and other type checking issues) could be
documented in a better way. For example I couldn't find any links to
your papers on OCaml website


2012/1/23 Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>:
> On 2012/01/24, at 9:53, Milan Stanojević wrote:
>
>> Hi, we're trying to understand the type inference with polymorphic
>> variants in match statements. This is a simplification of an actual
>> case that happened in practice.
>>
>> 1)
>> let f i a =
>>  match i, a with
>>  | true, `A -> `B
>>  | false, x -> x
>>
>> fails with
>> File "foo.ml", line 4, characters 16-17:
>> Error: This expression has type [< `A ]
>>       but an expression was expected of type [> `B ]
>>       The first variant type does not allow tag(s) `B
>>
>> 2) changing false to _
>> let f i a =
>>  match i, a with
>>  | true, `A -> `B
>>  | _, x -> x
>>
>> this succeeds with
>> val f : bool -> ([> `A | `B ] as 'a) -> 'a
>>
>> 3) changing x in (1) to _ , and using a on the right side
>> let f i a =
>>  match i, a with
>>  | true, `A -> `B
>>  | false, _ -> a
>>
>> this fails in the same way as (1)
>>
>> 4) finally adding another case to match statement
>> let f i a =
>>  match i, a with
>>  | true, `A -> `B
>>  | false, x -> x
>>  | true, x -> x
>>
>> this succeeds with the same type as (2)
>>
>>
>> So it seems there is some interaction between type inference and
>> exhaustivnest of the match statements.
>>
>> Can someone shed some light on what is going on here?
>
> Indeed. The basic idea is to close variant types when leaving them
> open would make the pattern matching non-exhaustive.
> Here, if we assume that a has type [`A | `B], then the pattern-matching
> becomes non-exhaustive, so the type inferred is just [`A]
> (i.e. the list of all constructors appearing inside the patterns at this position).
>
> Actually, the theory is a bit more complicated, and the full details are
> in the following paper, but you should just expect the above behavior
> in practice.
>
>        Typing deep pattern-matching in presence of polymorphic variants.
>        http://www.math.nagoya-u.ac.jp/~garrigue/papers/index.html
>
> Note that there is also another way to make (1) type, without adding
> new cases
>
>  let f i a =
>    match i, a with
>    | true, `A -> `B
>    | false, (`A as x) -> x;;
>  val f : bool -> [< `A ] -> [> `A | `B ] = <fun>
>
> Here we have removed the connection between a and the output,
> allowing `A to be combine with `B without changing the type of a.
>
> Hope this helps.
>
> Jacques Garrigue
>

Re: [Caml-list] polymorphic variants in match statements

[Jacques Garrigue]

On 2012/01/25, at 2:42, Milan Stanojević wrote:

> Thanks a lot, Jacques!
> This helped my understanding a lot.
>
> I only wonder if maybe this (and other type checking issues) could be
> documented in a better way. For example I couldn't find any links to
> your papers on OCaml website

Actually they are there, but maybe not so visible.
There is a "papers" section in the "about" part of the site.
(Follow the link under the title)

http://caml.inria.fr/about/papers.en.html

Curiously there is no direct link from the "comprehensive"  
documentation index :-)

Jacques Garrigue

Re: [Caml-list] polymorphic variants in match statements

[Milan Stanojević]

A small follow-up question

Polymorphic variant types are not allowed to have non-regular
recursion, i.e. the following type definition gives an error

type 'a t = [ `A of 'a | `B of ('a * 'a) t ]

Error: In the definition of t, type ('a * 'a) t should be 'a t

I guess the reason why this is not allowed has something to do with
our previous discussion, but I'm struggling to connect the dots.

Can you please explain this restriction?




2012/1/24 Milan Stanojević <milanst@gmail.com>:
> Thanks a lot, Jacques!
> This helped my understanding a lot.
>
> I only wonder if maybe this (and other type checking issues) could be
> documented in a better way. For example I couldn't find any links to
> your papers on OCaml website
>
>
> 2012/1/23 Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>:
>> On 2012/01/24, at 9:53, Milan Stanojević wrote:
>>
>>> Hi, we're trying to understand the type inference with polymorphic
>>> variants in match statements. This is a simplification of an actual
>>> case that happened in practice.
>>>
>>> 1)
>>> let f i a =
>>>  match i, a with
>>>  | true, `A -> `B
>>>  | false, x -> x
>>>
>>> fails with
>>> File "foo.ml", line 4, characters 16-17:
>>> Error: This expression has type [< `A ]
>>>       but an expression was expected of type [> `B ]
>>>       The first variant type does not allow tag(s) `B
>>>
>>> 2) changing false to _
>>> let f i a =
>>>  match i, a with
>>>  | true, `A -> `B
>>>  | _, x -> x
>>>
>>> this succeeds with
>>> val f : bool -> ([> `A | `B ] as 'a) -> 'a
>>>
>>> 3) changing x in (1) to _ , and using a on the right side
>>> let f i a =
>>>  match i, a with
>>>  | true, `A -> `B
>>>  | false, _ -> a
>>>
>>> this fails in the same way as (1)
>>>
>>> 4) finally adding another case to match statement
>>> let f i a =
>>>  match i, a with
>>>  | true, `A -> `B
>>>  | false, x -> x
>>>  | true, x -> x
>>>
>>> this succeeds with the same type as (2)
>>>
>>>
>>> So it seems there is some interaction between type inference and
>>> exhaustivnest of the match statements.
>>>
>>> Can someone shed some light on what is going on here?
>>
>> Indeed. The basic idea is to close variant types when leaving them
>> open would make the pattern matching non-exhaustive.
>> Here, if we assume that a has type [`A | `B], then the pattern-matching
>> becomes non-exhaustive, so the type inferred is just [`A]
>> (i.e. the list of all constructors appearing inside the patterns at this position).
>>
>> Actually, the theory is a bit more complicated, and the full details are
>> in the following paper, but you should just expect the above behavior
>> in practice.
>>
>>        Typing deep pattern-matching in presence of polymorphic variants.
>>        http://www.math.nagoya-u.ac.jp/~garrigue/papers/index.html
>>
>> Note that there is also another way to make (1) type, without adding
>> new cases
>>
>>  let f i a =
>>    match i, a with
>>    | true, `A -> `B
>>    | false, (`A as x) -> x;;
>>  val f : bool -> [< `A ] -> [> `A | `B ] = <fun>
>>
>> Here we have removed the connection between a and the output,
>> allowing `A to be combine with `B without changing the type of a.
>>
>> Hope this helps.
>>
>> Jacques Garrigue
>>

Re: [Caml-list] polymorphic variants in match statements

[Jacques Garrigue]

On 2012/02/11, at 7:20, Milan Stanojević wrote:

> A small follow-up question
> 
> Polymorphic variant types are not allowed to have non-regular
> recursion, i.e. the following type definition gives an error
> 
> type 'a t = [ `A of 'a | `B of ('a * 'a) t ]
> 
> Error: In the definition of t, type ('a * 'a) t should be 'a t
> 
> I guess the reason why this is not allowed has something to do with
> our previous discussion, but I'm struggling to connect the dots.
> 
> Can you please explain this restriction?

Actually, this is not directly related.
The problem here is with type inference of recursive types.
To do that, we need to do type inference on (possibly infinite) recursive trees.
This is easy for regular trees (which can be represent as a directed graph),
as the usual algorithm for first-order unification works.
So what ocaml does is building such a regular tree on the fly, by creating a
back edge to a previous ['a t] node when it meets another ['b t] node below it.

So for instance, with definition
  type 'a t = [ `A of 'a | `B of 'a t ]

the type [int t] would expand to ([`A of int | `B of 'r] as 'r)

However, for this to work, any occurrence of t inside its own definition
should have identical parameters. Hence the enforced restriction.

	Jacques Garrigue