[Caml-list] Typing of recursive function with polymorphic variants

[Caml-list] Typing of recursive function with polymorphic variants

[Vincent Jacques]

Hello,

utop # let rec f1 = function
  | `A x -> f1 x
  | `B -> `B;;
val f1 : ([< `A of 'a | `B ] as 'a) -> [> `B ] = <fun>

utop # let rec f2 = function
  | `A x -> f2 (f2 x)
  | `B -> `B;;
val f2 : ([< `A of 'a | `B > `B ] as 'a) -> 'a = <fun>

but I can *see* that f2 never returns an `A so I would give it the
same type as f1.

1) Would I be right or am I missing something?

2) Assuming I'm right, can you please give me hints about this
limitation of the typing algorithm?
I have a basic understanding of the W typing algorithm. Assuming that
a similar algorithm is used for polymorphic variants, I imagine that
when I call f2 (f2 x), f2's return type is "unified" with f2's
parameter type. Why is this needed?

3) The type of f2 is more generic than the type of f1. Could I use
type annotations to help the typing algorithm choose a more specific
type?

I tried to annotate f3 (f3 x) but I get different behaviors in utop
and in the compiler. I'm lost :)

utop # let rec f3 = function
  | `A x -> ((f3 (f3 x)):[`B])
  | `B -> `B;;
Error: This pattern matches values of type [? `A of [ `B ] ]
    but a pattern was expected which matches values of type [ `B ]
    The second variant type does not allow tag(s) `A

In a .ml file:

let rec f3 = function
  | `A x -> ((f3 (f3 x)):[`B])
  | `B -> `B

let () = f3

Error: This expression has type [ `B ] -> [ `B ]
    but an expression was expected of type unit

Thank you for your help,
-- 
Vincent Jacques
http://vincent-jacques.net

"S'il n'y a pas de solution, c'est qu'il n'y a pas de problème"
            Devise Shadock

Re: [Caml-list] Typing of recursive function with polymorphic variants

[Mikhail Mandrykin]

Hello,

On пятница, 14 апреля 2017 г. 17:30:33 MSK Vincent Jacques wrote:
> utop # let rec f2 = function
> 
>   | `A x -> f2 (f2 x)
>   | `B -> `B;;
> 
> val f2 : ([< `A of 'a | `B > `B ] as 'a) -> 'a = <fun>
> 3) The type of f2 is more generic than the type of f1. Could I use
> type annotations to help the typing algorithm choose a more specific
> type?
> 
> I tried to annotate f3 (f3 x) but I get different behaviors in utop
> and in the compiler. I'm lost :)
To give the function f2 the desired type ([< `A of 'a | `B ] as 'a) -> [> `B ] 
the type-checker needs to treat the type of this function (f2) as polymorphic 
inside the body of the function to avoid unifying the result type with the 
type of the first parameter. In OCaml this can be achieved by using an explicit 
polymorphic type annotation
(https://caml.inria.fr/pub/docs/manual-ocaml/extn.html#sec227): 

let rec f2 : 'a. ([<`A of 'a | `B ] as 'a) -> [`B]= function
  | `A x -> f2 (f2 x)
  | `B -> `B;;
val f2 : ([< `A of 'a | `B ] as 'a) -> [ `B ] = <fun>

> Assuming that
> a similar algorithm is used for polymorphic variants
Indeed, polymorphic variant types are treated by using constrained 
polymorphism integrated into usual HM type system, as described in the papers 
referenced here:
(http://ocaml.org/docs/papers.html#PolymorphicVariants).

> Why is this needed?
The unification is probably done because constrained type variables are treated 
as normal unification variables. AFAIK type inference for polymorphic recursion 
is undecidable (semidecidable) in general
(there are some references in this message
http://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/msg00924.html)
and OCaml doesn't provide any incomplete support for some special cases, but 
allows to specify polymorphic types explicitly using those annotations.


--
Best,
Mikhail
> 
> utop # let rec f3 = function
> 
>   | `A x -> ((f3 (f3 x)):[`B])
>   | `B -> `B;;
> 
> Error: This pattern matches values of type [? `A of [ `B ] ]
>     but a pattern was expected which matches values of type [ `B ]
>     The second variant type does not allow tag(s) `A
> 
> In a .ml file:
> 
> let rec f3 = function
> 
>   | `A x -> ((f3 (f3 x)):[`B])
>   | `B -> `B
> 
> let () = f3
> 
> Error: This expression has type [ `B ] -> [ `B ]
>     but an expression was expected of type unit
> 
> Thank you for your help,


-- 
Mikhail Mandrykin
Linux Verification Center, ISPRAS
web: http://linuxtesting.org
e-mail: mandrykin@ispras.ru

Re: [Caml-list] Typing of recursive function with polymorphic variants

[Mikhail Mandrykin]

On пятница, 14 апреля 2017 г. 21:11:52 MSK Mikhail Mandrykin wrote:
> the desired type ([< `A of 'a | `B ] as 'a) -> [> `B]
> val f2 :                 ([< `A of 'a | `B ] as 'a) -> [ `B ] = <fun>
Actually, one more polymorphic variable:
let rec f2 : 'a 'b. ([<`A of 'a | `B ] as 'a) -> ([>`B] as 'b)= function
  | `A x -> f2 (f2 x)
  | `B -> `B;;
val f2 : ([< `A of 'a | `B ] as 'a) -> [> `B ] = <fun>

-- 
Mikhail

Re: [Caml-list] Typing of recursive function with polymorphic variants

[Vincent Jacques]

2017-04-14 20:47 GMT+02:00 Mikhail Mandrykin <mandrykin@ispras.ru>:
> let rec f2 : 'a 'b. ([<`A of 'a | `B ] as 'a) -> ([>`B] as 'b)= function
>   | `A x -> f2 (f2 x)
>   | `B -> `B;;
> val f2 : ([< `A of 'a | `B ] as 'a) -> [> `B ] = <fun>

Thank you Mikhail, this helps a lot.

I didn't know about polymorphic type annotations.

Thanks!
-- 
Vincent Jacques
http://vincent-jacques.net

"S'il n'y a pas de solution, c'est qu'il n'y a pas de problème"
            Devise Shadock