Re: [Caml-list] GADT+polymorphic variants quirk

[Anton Bachin <antronbachin@gmail.com>]

Nils, actually, you can get the expanded M to typecheck as well:

    type integer = [ `Integer ]
    type rational = [ integer | `Rational ]
    type real = [ rational | `Real ]

    type _ num =
     | N : int -> [> integer ] num
     | Q : int * int -> [> rational ] num
     | R : float -> real num

    module M :
    sig
     val mult : ([< real] as 'a) num -> 'a num -> 'a num

     val to_int : integer num -> int
     val to_num_denom : rational num -> int * int
     val to_float : real num -> float
    end =
    struct
     let mult : type a. a num -> a num -> a num = fun a b ->
       match a, b with
       (* When b = N _, the first pattern decides the type of the result. *)
       | N n, N m -> N (n * m)
       | Q (n, n'), N m -> Q (n * m, n')
       | R n, N m -> R (n *. float_of_int m)

       (* This case must be here, not inside the b = Q _ nested match
          expression, to ensure that the typechecker sees real num before
          [> rational ] num. *)
       | R n, Q (m, m') -> R (n *. float_of_int m /. float_of_int m')
       (* These are cases in which we want the typechecker to see b = Q _
          first. *)
       | _, Q (m, m') ->
         (match a with
         (* Harder to get an exhaustiveness check here, didn't fully think
            through it. *)
         | N n -> Q (n * m, m')
         | Q (n, n') -> Q (n * m, n' * m')
         | _ -> assert false)

       (* When b = R _, the second pattern decides the type of the result,
          and that type is real num. *)
       | _, R m ->
         (match a with
          | N n -> R (float_of_int n *. m)
          | R n -> R (n *. m)
          | Q (n, n') -> R (float_of_int n /. float_of_int n' *. m))

     let to_int : integer num -> int = fun (N n) -> n

     let to_num_denom : rational num -> int * int = function
       | N n -> (n, 1)
       | (Q (n, n')) -> (n, n')

     let to_float = function
       | N n -> float_of_int n
       | Q (n, n') -> float_of_int n /. float_of_int n'
       | R n -> n
    end

    let () =
      M.(mult (R 2.) (Q (3, 2)) |> to_float) |> Printf.printf "%f\n”

I added some comments in the match expressions to try to clarify why
they must be written as above. The scheme is, while unifying the
patterns, you want the first pattern the typechecker encounters to have
the same type as the result. Again, I’m not sure how far you can take
this, and keep in mind Jacques’ warning, but there it is :)

Best,
Anton