CODEWITHSUNDEEP
objectpolymorphismocamltyping
user1971598
user1971598

Reputation:

Polymorphism typing problems with OCaml objects

On 4.03.0.

I have this code, basically:

module rec First : sig

  type field
  type 'a target = <at_least_this_method: field; .. > as 'a

end = First
and Second : sig

  class foo : object
    method at_least_this_method : First.field
  end

end = Second
and Third : sig

  class usage :
    object

      method action : #Second.foo First.target -> unit

    end

end = struct

  class usage = object
    method action (a : #Second.foo First.target) = ()
  end

end

And the last line of method action fails to type with error message:

Error: Some type variables are unbound in this type:
         class usage :
           object method action : #Second.foo First.target -> unit end
       The method action has type (#Second.foo as 'a) First.target -> unit
       where 'a is unbound

I also tried something like: 

  class usage = object
    method action = fun (type t) (b : (#Second.foo as t) First.target) -> ()
  end

But that didn't type either.

Upvotes: 2

Views: 185

Answers (3)

objmagic
objmagic

Reputation: 1028

EDIT: please refer to @gariguejej's answer below for a better explanation.

I'm not an expert of type system of objects, but here are my two cents.

Change your code to:

module rec First : sig

  type field
  type 'a target = <at_least_this_method: field; .. > as 'a

end = First
and Second : sig

  class foo : object
    method at_least_this_method : First.field
  end

end = Second

and Third : sig

  class ['a] usage :
    object
      method action : 'a First.target -> unit
    end

end = struct

  class ['a] usage = object
    method action : 'a First.target -> unit = fun a -> ()
  end

end

Use ocaml -i, we can see 'a is constrained to constraint 'a = < at_least_this_method : First.field; .. >. 

module rec First :
  sig
    type field
    type 'a target = 'a constraint 'a = < at_least_this_method : field; .. >
  end
and Second :
  sig class foo : object method at_least_this_method : First.field end end
and Third :
  sig
    class ['a] usage :
      object
        constraint 'a = < at_least_this_method : First.field; .. >
        method action : 'a First.target -> unit
      end
  end

Of course, you can also manually constraint 'a to <at_least_this_method: field> if you want it to be a closed object type. For example,

module rec First : sig

  type field
  type 'a target = <at_least_this_method: field; .. > as 'a

end = First
and Second : sig

  class foo : object
    method at_least_this_method : First.field
  end

end = Second

and Third : sig

  class ['a] usage :
    object
      constraint 'a = <at_least_this_method:First.field>
      method action : 'a First.target -> unit
    end

end = struct

  class ['a] usage = object
    constraint 'a = <at_least_this_method:First.field>
    method action : 'a First.target -> unit = fun a -> ()
  end

end

See manual Chapter 3.10

Upvotes: 1

gariguejej
gariguejej

Reputation: 111

I suppose that you want to write the following code:

module rec First : sig
  type field
  class type target = object method at_least_this_method: field end
end = First
and Third : sig
  class usage :
    object
      method action : #First.target -> unit
    end
end = struct
  class usage = object
    method action : 'a. (#First.target as 'a) -> unit = fun a -> ()
  end
end

I'm not sure why you are using recursive modules here. They do not work well with classes. In particular, interfaces are not propagated to classes inside the module. This is why you need to write explicitly the type of the polymorphic method action in the body of Third.

Upvotes: 5

camlspotter
camlspotter

Reputation: 9030

Let me add an unsuccessful trial to solve the problem.

#c is an open type and it contains a type variable implicitly to express .. part of the object type, the type error comes since this hidden type variable is not quantified.

Interesting and confusing thing is that the use of #A.foo is not rejected at the signature even the hidden variable is not explicitly quantified. The following type-checks. (From the fear against the recursive module typing, I changed your example using a functor):

module Make(A : sig
  type field
  type 'a target = <at_least_this_method: field; .. > as 'a

  class foo : object
    method at_least_this_method : field
  end
end) = struct
  module type S = sig
    class usage : object
        method action : #A.foo A.target -> unit
    end
  end
  module type S' = sig
    class usage : object
        method action : 'a . (#A.foo as 'a) A.target -> unit
    end
  end

end

ocamlc -c -i shows that the class declaration of the signature S and S' are identical. The type variable inside #A.foo is quantified at the method level and make action a polymorphic method.

@objmagic's answer is to move this polymorphism to class level. Then what should we do if we want to keep the method polymorphic?:

class usage = object
  method action : 'a . (#A.foo as 'a) A.target -> unit = assert false
end

But this does not type-check:

Error: This expression has type 'a. (#A.foo as 'a) A.target -> unit
       but an expression was expected of type
         'b. (#A.foo as 'b) A.target -> unit
       The type variable 'c occurs inside 'c

The type error is completely cryptic. To me it is a sign of crossing a danger line of object typing. Whenever I see this kind of error messages, I naively think it is simply impossible to define a method of such a type, or it is a bug of object typing and retreat...

BTW, there is no problem to define a polymorphic record with that type:

type t = { action : 'a . (#A.foo as 'a) A.target -> unit }
let t = { action = fun _ -> assert false }

Upvotes: 2

Related Questions