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

[Anton Bachin <antronbachin@gmail.com>]

I suppose one improvement to that assert false case would be to use
R _ for the pattern instead of _, but it’s not the ultimate solution.

> El ene 3, 2017, a las 9:09, Anton Bachin <antronbachin@gmail.com> escribió:
> 
> 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
>