[Caml-list] GADT+polymorphic variants quirk

[Caml-list] GADT+polymorphic variants quirk

[Anton Bachin]

Hello,

Consider this code for simulating an ad-hoc polymorphic addition
function:

    type whole = [ `Integer ]
    type general = [ whole | `Float ]

    type _ num =
      | I : int -> [> whole ] num
      | F : float -> general num

    module M :
    sig
      val add : ([< general ] as 'a) num -> 'a num -> 'a num
      val to_int : whole num -> int
      val to_float : general num -> float
    end =
    struct
      let add : type a. a num -> a num -> a num = fun a b ->
        match a, b with
        | I n, I m -> I (n + m)
        | F n, I m -> F (n +. float_of_int m)
        | F n, F m -> F (n +. m)
        | _ ->
          (* ----NOTE---- *)
          match b, a with
          | F m, I n -> F (float_of_int n +. m)
          | _ -> assert false

      let to_int : whole num -> int = fun (I n) -> n

      let to_float = function
        | I n -> float_of_int n
        | F n -> n
    end

    let () =
      M.add (I 1) (I 2)  |> M.to_int   |> Printf.printf "%i\n";
      M.add (I 1) (F 2.) |> M.to_float |> Printf.printf "%f\n"

Instead of the nested match expression (marked with (* NOTE *)), I would
have expected to just write

    | I n, F m -> ...

However, if I actually do that, the result is an error on the expression
in the case:

    Error: This expression has type general num
           but an expression was expected of type a num
           Type general = [ `Float | `Integer ] is not compatible with type
             a = [> `Integer ] 
           The second variant type does not allow tag(s) `Float

While the reversed case type-checks successfully. I can imagine why this
would be so, but I want to ask the experts on the mailing list.

Is this a known quirk of the typechecker? A bug? Is there some
alternative syntax I am missing that would allow the I n pattern to be
written first?

Note that there is a way to rewrite the nested match cases to avoid _
and maintain the exhaustiveness check. I wrote them out as above for
clarity. The actual solution I have settled on for now is:

      let add : type a. a num -> a num -> a num = fun a b ->
        match a, b with
        | I n, I m -> I (n + m)
        | F n, I m -> F (n +. float_of_int m)
        | _,   F m ->
          match a with
          | I n -> F (float_of_int n +. m)
          | F n -> F (n +. m)

Best,
Anton


P.S. If interested, the code was for this Stack Overflow question:

    http://stackoverflow.com/questions/41214000

answer:

    http://stackoverflow.com/a/41334879/2482998

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

[Jacques Garrigue]

Let us just say that using polymorphic variant or object types as
indices of GADTs are not explicitly supported. In your case, it seems
that the problem is that unification including abstract rows does not
work correctly. This can be classified as a (known) bug, but it is not clear yet
when we will fix it.
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

This should avoid these problems without any real loss of expressivity.

Jacques Garrigue

On 2016/12/28 05:04, Anton Bachin wrote:
> 
> Hello,
> 
> Consider this code for simulating an ad-hoc polymorphic addition
> function:
> 
>    type whole = [ `Integer ]
>    type general = [ whole | `Float ]
> 
>    type _ num =
>      | I : int -> [> whole ] num
>      | F : float -> general num
> 
>    module M :
>    sig
>      val add : ([< general ] as 'a) num -> 'a num -> 'a num
>      val to_int : whole num -> int
>      val to_float : general num -> float
>    end =
>    struct
>      let add : type a. a num -> a num -> a num = fun a b ->
>        match a, b with
>        | I n, I m -> I (n + m)
>        | F n, I m -> F (n +. float_of_int m)
>        | F n, F m -> F (n +. m)
>        | _ ->
>          (* ----NOTE---- *)
>          match b, a with
>          | F m, I n -> F (float_of_int n +. m)
>          | _ -> assert false
> 
>      let to_int : whole num -> int = fun (I n) -> n
> 
>      let to_float = function
>        | I n -> float_of_int n
>        | F n -> n
>    end
> 
>    let () =
>      M.add (I 1) (I 2)  |> M.to_int   |> Printf.printf "%i\n";
>      M.add (I 1) (F 2.) |> M.to_float |> Printf.printf "%f\n"
> 
> Instead of the nested match expression (marked with (* NOTE *)), I would
> have expected to just write
> 
>    | I n, F m -> ...
> 
> However, if I actually do that, the result is an error on the expression
> in the case:
> 
>    Error: This expression has type general num
>           but an expression was expected of type a num
>           Type general = [ `Float | `Integer ] is not compatible with type
>             a = [> `Integer ] 
>           The second variant type does not allow tag(s) `Float
> 
> While the reversed case type-checks successfully. I can imagine why this
> would be so, but I want to ask the experts on the mailing list.
> 
> Is this a known quirk of the typechecker? A bug? Is there some
> alternative syntax I am missing that would allow the I n pattern to be
> written first?
> 
> Note that there is a way to rewrite the nested match cases to avoid _
> and maintain the exhaustiveness check. I wrote them out as above for
> clarity. The actual solution I have settled on for now is:
> 
>      let add : type a. a num -> a num -> a num = fun a b ->
>        match a, b with
>        | I n, I m -> I (n + m)
>        | F n, I m -> F (n +. float_of_int m)
>        | _,   F m ->
>          match a with
>          | I n -> F (float_of_int n +. m)
>          | F n -> F (n +. m)
> 
> Best,
> Anton
> 
> 
> P.S. If interested, the code was for this Stack Overflow question:
> 
>    http://stackoverflow.com/questions/41214000
> 
> answer:
> 
>    http://stackoverflow.com/a/41334879/2482998

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

[Jacques Garrigue]

On 2017/01/03 23:05, Nils Becker wrote:
> 
> 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

You can encode any finite set type using core types.
The idea is just to use presence and absence.

type pre = Pre
type abs = Abs

type integer = pre * abs * abs  (* integer * rational * real *)
type rational = pre * pre * abs
type real = pre * pre * pre

However, in this case we are only taking about a linear inheritance hierarchy,
which can be expressed more compactly. For instance

type real = Real
type ’a rat = Rational of ‘a
type rational = int * int rat
type integer = int rat

In general, any linear hierarchy can be encoded using type level natural numbers

type zero = Zero
type ‘a succ = Succ of ‘a

which in this case would give

type real = zero
type rational = zero succ
type integer = zero succ succ

This scheme can be extended to any n-ary tree hierarchy, using a n-ary constructor in place of succ.

Jacques

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

[Anton Bachin]

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
> 

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

[Anton Bachin]

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

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

[Nils Becker]

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.