[Caml-list] Confusing behaviour of type inference for polymorphic classes.

[Dmitri Boulytchev <dboulytchev@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 2252 bytes --]

     Hello everyone,

     I stumbled on the following confusing behaviour of the type 
checker: given the definitions

     type ('a, 'b) t =
        A of 'a * ('b, 'a) t
      | B of 'a

    class ['a, 'b, 'ta, 'tb] m =
      object
        method t : ('a -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t -> ('ta, 
'tb) t =
          fun fa fb s ->
            match s with
            | A (a, bat) -> A (fa a, (new m)#t fb fa bat)
            | B  a       -> B (fa a)
      end

     the following type is inferred for the class m:

     class ['a, 'b, 'ta, 'c] m :
       object
         constraint 'b = 'a  <--- why?
         constraint 'c = 'ta <--- why?
         method t : ('a -> 'ta) -> ('a -> 'ta) -> ('a, 'a) t -> ('ta, 'ta) t
       end

    Perhaps some explicit annotation is needed here (like that for the 
polymorphic recursion
for functions).
    I found the following workaround: first we abstract the instance 
creation ("new m") away:

    class ['a, 'b, 'ta, 'tb] m' f =
      object
        method t : ('a -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t -> ('ta, 
'tb) t =
          fun fa fb s ->
            match s with
            | A (a, bat) -> A (fa a, (f ())#t fb fa bat)
            | B  a       -> B (fa a)
      end

   which gives us the unconstrained type

    class ['a, 'b, 'ta, 'tb] m' :
         (unit ->
          < t : ('b -> 'tb) -> ('a -> 'ta) -> ('b, 'a) t -> ('tb, 'ta) 
t; .. >) ->
          object
            method t : ('a -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t -> ('ta, 
'tb) t
          end

   Then we construct the instance creation explicitly polymorphic function:

    let rec f : 'a 'b 'ta 'tb . unit -> <t : ('a -> 'ta) -> ('b -> 'tb) 
-> ('a, 'b) t -> ('ta, 'tb) t> =
      fun () -> new m' f

  and finally the class we're looking for:

    class ['a, 'b, 'ta, 'tb] m = ['a, 'b, 'ta, 'tb] m' f

    The complete annotated source file is attached.
    This workaround however does not solve everything: we cannot 
actually inherit
from the m since it calls hardcoded "new m"; we should inherit from m' 
(with additional parameter)
instead and "tie the knot" on the toplevel.
     Are there better solutions? Please help :)

     Best regards,
     Dmitry Boulytchev,
     St.Petersburg State University,
     Russia.



[-- Attachment #2: sample.ml --]
[-- Type: text/x-ocaml, Size: 1471 bytes --]

type ('a, 'b) t = 
    A of 'a * ('b, 'a) t 
  | B of 'a

(*
   The initial definition

   class ['a, 'b, 'ta, 'tb] m =
     object
       method t : ('a -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t -> ('ta, 'tb) t = 
         fun fa fb s ->
           match s with
           | A (a, bat) -> A (fa a, (new m)#t fb fa bat)
           | B  a       -> B (fa a)
     end

   gives us the following type:

   class ['a, 'b, 'ta, 'c] m :
     object
       constraint 'b = 'a  <--- why?
       constraint 'c = 'ta <--- why?
       method t : ('a -> 'ta) -> ('a -> 'ta) -> ('a, 'a) t -> ('ta, 'ta) t
     end
*)

(* The modified version with the "new" abstracted away: *)

class ['a, 'b, 'ta, 'tb] m' f =
  object
    method t : ('a -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t -> ('ta, 'tb) t = 
      fun fa fb s ->
        match s with
        | A (a, bat) -> A (fa a, (f ())#t fb fa bat)
        | B  a       -> B (fa a)
  end

(* Inferred type with no artificial constraints:

   class ['a, 'b, 'ta, 'tb] m' :
     (unit ->
      < t : ('b -> 'tb) -> ('a -> 'ta) -> ('b, 'a) t -> ('tb, 'ta) t; .. >) ->
      object
        method t : ('a -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t -> ('ta, 'tb) t
      end
*)

(* Instance creation function: *)

let rec f : 'a 'b 'ta 'tb . unit -> <t : ('a -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t -> ('ta, 'tb) t> = 
  fun () -> new m' f

class ['a, 'b, 'ta, 'tb] m = ['a, 'b, 'ta, 'tb] m' f

(* Ok now:
   class ['a, 'b, 'ta, 'tb] m' : ['a, 'b, 'ta, 'tb] m
*)