Can you provide an example of " This happens if `bar`'s type contains negative occurences of its self-type"
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
#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).
Java programmers would be confused the most, because they would have to unlearn the most. In Java, a class is a type on its own right. An object of class (and, hence, type) `Foo` has a very specific data structure, even if this data structure is unknown to the user. On the other hand, in OCaml, a class is just a constructor for objects of a particular structural type. Two objects with the same structural type can have completely different underlying data structures. Making things even more confusing, inheritance doesn't entail subtyping - a class `foo` can inherit from a class `bar`, without `foo`'s type being a subtype of `bar`'s type. This happens if `bar`'s type contains negative occurences of its self-type. As a result, few intuitions about Java's class system carry over to OCaml.
Python programmers would be somewhat less surprised, but if their idea of a typed object-oriented language is “something that looks like Java”, they could encounter all the difficulties mentioned in the preceding paragraph. On the other hand, if they have no experience at all with typed languages, OCaml's class system can still be a source of pain, in that inferred object types can be utterly incomprehensible for someone not familiar with how the type checker works. By contrast, the inferred type signatures for the non-object-oriented subset of OCaml are usually very tame.
---
Sorry, e_d_g_a_r, I can't reply to you directly, because the website says I'm “submitting too fast”, but here is an example: http://pastebin.com/yUmNnFD5 . By the way, this isn't a bug in OCaml's type checker - it's the way it's supposed to work.