Typechecking of recursive variants

From: Judicael Courant (Judicael.Courant@lri.fr)
Date: Fri May 12 2000 - 16:34:08 MET DST

  • Next message: Amit Dubey: "The Unix module & records"

    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

    This archive was generated by hypermail 2b29 : Fri May 12 2000 - 19:17:54 MET DST