4 ms·

Can you provide an example of " This happens if `bar`'s type contains negative occurences of its self-type"

catnaroek 11y ago
I inverted the roles of `foo` and `bar` with respect to my previous post. In `foo`'s definition, the self-type is `'a`. Note how `foo` has a method that takes an argument of type `'a` - a contravariant occurrence of the self-type. The consequence is that, although `bar` inherits `foo`, their associated structural types are neither a subtype of the other. lolcathost% ocaml OCaml version 4.02.3 # class foo = object (_ : 'a) method test (_ : 'a) = () end;; class foo : object ('a) method test : 'a -> unit end # class bar = object inherit foo method other = () end;; class bar : object ('a) method other : unit method test : 'a -> unit end # let f = new foo;; val f : foo = <obj> # let b = new bar;; val b : bar = <obj> # f#test f;; - : unit = () # b#test b;; - : unit = () # f#test b;; Characters 7-8: f#test b;; ^ Error: This expression has type bar but an expression was expected of type foo The second object type has no method other # b#test f;; Characters 7-8: b#test f;; ^ Error: This expression has type foo but an expression was expected of type bar The first object type has no method other #
lmm 11y ago
I guess this means contravariance, which commonly comes from having a method that accepts an argument of the same type. Consider Comparable in Java. Maybe you want to say Animal implements Comparable<Animal>. But that would mean that any Animal is comparable to any other Animal - the compiler would let you compare a Cat to a Dog. Whereas really what you want to do is reuse the implementation of Animal, but Cats are only comparable to other Cats, and Dogs are only comparable to other Dogs - so Cat and Dog should inherit from Animal, but their types won't actually be subtypes of Animal. (There's no way to express this constraint in Java).

I inverted the roles of `foo` and `bar` with respect to my previous post. In `foo`'s definition, the self-type is `'a`. Note how `foo` has a method that takes an argument of type `'a` - a contravariant occurrence of the self-type. The consequence is that, although `bar` inherits `foo`, their associated structural types are neither a subtype of the other. lolcathost% ocaml OCaml version 4.02.3 # class foo = object (_ : 'a) method test (_ : 'a) = () end;; class foo : object ('a) method test : 'a -> unit end # class bar = object inherit foo method other = () end;; class bar : object ('a) method other : unit method test : 'a -> unit end # let f = new foo;; val f : foo = <obj> # let b = new bar;; val b : bar = <obj> # f#test f;; - : unit = () # b#test b;; - : unit = () # f#test b;; Characters 7-8: f#test b;; ^ Error: This expression has type bar but an expression was expected of type foo The second object type has no method other # b#test f;; Characters 7-8: b#test f;; ^ Error: This expression has type foo but an expression was expected of type bar The first object type has no method other #

lmm 11y ago

I guess this means contravariance, which commonly comes from having a method that accepts an argument of the same type. Consider Comparable in Java. Maybe you want to say Animal implements Comparable<Animal>. But that would mean that any Animal is comparable to any other Animal - the compiler would let you compare a Cat to a Dog. Whereas really what you want to do is reuse the implementation of Animal, but Cats are only comparable to other Cats, and Dogs are only comparable to other Dogs - so Cat and Dog should inherit from Animal, but their types won't actually be subtypes of Animal. (There's no way to express this constraint in Java).