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

[Mikhail Mandrykin <mandrykin@ispras.ru>]

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