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

[Nils Becker <nils.becker@bioquant.uni-heidelberg.de>]

hi,

i am the OP of the stackoverflow question referred to by anton.

> I would suggest avoid using polymorphic variants here, using rather
> a simple encoding:
>
>    type whole = Whole
>    type general = General
>
>    type _ num =
>       | I : int -> _ num
>       | F : float -> general num

i tried this simpler proposal and it does seem to work nicely. however,
what i'm really interested in is encoding somewhat more elaborate
subtyping relationships. for example, how would you handle the case
where there is a 'rational' number type inbetween integers and reals? i
don't see how your proposal can be generalized to that?

i tried to generalize the solution proposed by anton like this:

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


and then a generalized module implementation like this:

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
    | _, N m ->
      (match a with
       | N n -> N (n * m)
       | R n -> R (n *. float_of_int m)
       | Q (n, n') -> Q (n * m, n'))
    | _,   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))
    | _, Q (m, m') ->
      (match a with
       | N n -> Q (n * m, m')
       | R n -> R (n *. float_of_int m /. float_of_int m')
       | Q (n, n') -> Q (n * m, 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

where i tried to replicate the sub-case matching to work around the
type-checker's limitations. unfortunately this does not typecheck; in
the same way that was described above:

Error: This expression has type real num but an expression was expected
of type                                                  a num

                             Type real = [ `Integer | `Rational | `Real
] is not compatible with type
         a = [> `Integer ]
       The second variant type does not allow tag(s) `Rational, `Real



so it seems that it's not really viable to try to build something along
these lines.

is there a better way to do this kind of subtyping in current ocaml?

n.