Typechecking of recursive variants

Typechecking of recursive variants

[Judicael Courant]

Hello,

I do not understand the following behavior of the typechecker :
match x 4 with `X z -> z | `Y -> assert false;;
- : [ `Y | `X of '_a] as 'a = `X (`X (`X `Y))

        Objective Caml version 3.00

# let rec x n = if n = 0 then `Y else `X (x (n-1));;
val x : int -> ([> `Y | `X of 'a] as 'a) = <fun>
# x 3;;
- : _[> `Y | `X of '_a] as 'a = `X (`X (`X `Y))
# match x 4 with `X z -> z | `Y -> assert false;;
- : [ `Y | `X of '_a] as 'a = `X (`X (`X `Y))


What do these underscores mean ? Anything to do with monomorphic type
variables ? Why is not there any ">" at the beginning of the latest
type ?

Judicaël.
-- 
Judicael.Courant@lri.fr, http://www.lri.fr/~jcourant/
(+33) (0)1 69 15 64 85
"Montre moi des morceaux de ton monde, et je te montrerai le mien"
Tim, matricule #929, condamné à mort.
http://rozenn.picard.free.fr/tim.html

Re: Typechecking of recursive variants

[Jacques Garrigue]

From: Judicael Courant <Judicael.Courant@lri.fr>

>         Objective Caml version 3.00
> 
> # let rec x n = if n = 0 then `Y else `X (x (n-1));;
> val x : int -> ([> `Y | `X of 'a] as 'a) = <fun>
> # x 3;;
> - : _[> `Y | `X of '_a] as 'a = `X (`X (`X `Y))
> # match x 4 with `X z -> z | `Y -> assert false;;
> - : [ `Y | `X of '_a] as 'a = `X (`X (`X `Y))
> 
> 
> What do these underscores mean ? Anything to do with monomorphic type
> variables ?

Exactly. Since "x 3" is an application, its result must be
monomorphic.
But in fact the _ in '_a is a bug :-)
In recursive variants, the monomorphism is not indicated on the
abbreviation, but on the variant type itself (like for objects).
So the right types would be
# x 3;;
- : _[> `Y | `X of 'a] as 'a = `X (`X (`X `Y))
# match x 4 with `X z -> z | `Y -> assert false;;
- : [ `Y | `X of 'a] as 'a = `X (`X (`X `Y))
Notice that there is no monomorphism annotation in the second type,
since it cannot be refined anymore.

> Why is not there any ">" at the beginning of the latest
> type ?
Your original type was [> `Y | `X of 'a], and you matched it with
cases producing the type [< `Y | `X of 'a]. By unification, the
result is [< `Y | `X of 'a > `Y | `X], or, in abbreviated form,
[`Y | `X of 'a] since all constructors are required.
Since you type was monomorphic, this unification affects the type
of "x 4", which is also the type of the argument of `X.

        Jacques
---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>