Typechecking of recursive variants

Judicael Courant
 Jacques Garrigue
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20000515 (20:09) 
From:  Jacques Garrigue <garrigue@k...> 
Subject:  Re: Typechecking of recursive variants 
From: Judicael Courant <Judicael.Courant@lri.fr> > Objective Caml version 3.00 > > # let rec x n = if n = 0 then `Y else `X (x (n1));; > 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.kyotou.ac.jp <A HREF=http://wwwfun.kurims.kyotou.ac.jp/~garrigue/>JG</A>