Re: Typechecking of recursive variants

From: Jacques Garrigue (garrigue@kurims.kyoto-u.ac.jp)
Date: Mon May 15 2000 - 02:33:35 MET DST

  • Next message: Markus Mottl: "Re: The performance cost of using exceptions?"

    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>



    This archive was generated by hypermail 2b29 : Mon May 15 2000 - 22:13:05 MET DST