3 ms·

The semantics of OO languages is really messy and complicated and probably has the least well understood theory of all sequential forms of computing.

seanmcdirmid 11y ago
Not just that, but we still don't really know how to combine subtyping and generics very well. The soundness question when considering variance is still quite open, and it shows in the poor support for type inference in OO languages (in spite of heroic efforts made in languages like Scala). Much of this has to do with the root: most of our PL theory was basically designed for FP, and applying them to OOP has been predictably difficult. Most PL theoreticians are more interested in FP than OOP, so progress is quite slow (though see work done by Ross Tate, Igarashi, etc...for progress).
- NotableAlamode 11y ago
  soundness question when considering variance What is this question? Have you got a reference?
  - AnimalMuppet 11y ago
    I'm not the one you were replying to, but maybe seanmcdirmid means this: https://en.wikipedia.org/wiki/Covariance_and_contravariance_%28computer_science%29 https://en.wikipedia.org/wiki/Covariance_and_contravariance_... But I thought that was pretty well understood, so I don't know what he thinks is open...
    - seanmcdirmid 11y ago
      For many popular type systems with generics, not really; e.g. see http://www.cs.cornell.edu/~ross/publications/mixedsite/mixed-site-tate-2013.pdf http://www.cs.cornell.edu/~ross/publications/mixedsite/mixed...
    - deleted 11y ago
      [deleted]
  - nrinaudo 11y ago
    It is possible that he's referring to mutable and covariant types being unsound. As an example, let's assume that you have two classes, Cat and Dog, both inheriting from Animal, and that you have a covariant mutable List implementation. Say you have a value of type List[Cat]. Since List is covariant, this value can legally be passed to a function that expects a parameter of type List[Animal]. Now, imagine you have a function that expects a List[Animal] and adds a Dog to it. That's a legal operation: Dog extends Animal and can thus be used this way. Putting the two together, you have a perfectly legal way of adding a Dog to a List[Cat], which a sound type system should not allow. An example of that is Java's Array, which is both covariant and mutable, and that as a result can yield type errors at runtime.
- mafribe 11y ago
  I suspect that combining generics with subtyping might always lead you into the land on undecidable type-inference. After all, pure genericity (System F) is already undecidable.

seanmcdirmid 11y ago

Not just that, but we still don't really know how to combine subtyping and generics very well. The soundness question when considering variance is still quite open, and it shows in the poor support for type inference in OO languages (in spite of heroic efforts made in languages like Scala). Much of this has to do with the root: most of our PL theory was basically designed for FP, and applying them to OOP has been predictably difficult. Most PL theoreticians are more interested in FP than OOP, so progress is quite slow (though see work done by Ross Tate, Igarashi, etc...for progress).

NotableAlamode 11y ago
soundness question when considering variance What is this question? Have you got a reference?
- AnimalMuppet 11y ago
  I'm not the one you were replying to, but maybe seanmcdirmid means this: https://en.wikipedia.org/wiki/Covariance_and_contravariance_%28computer_science%29 https://en.wikipedia.org/wiki/Covariance_and_contravariance_... But I thought that was pretty well understood, so I don't know what he thinks is open...
  - seanmcdirmid 11y ago
    For many popular type systems with generics, not really; e.g. see http://www.cs.cornell.edu/~ross/publications/mixedsite/mixed-site-tate-2013.pdf http://www.cs.cornell.edu/~ross/publications/mixedsite/mixed...
  - deleted 11y ago
    [deleted]
- nrinaudo 11y ago
  It is possible that he's referring to mutable and covariant types being unsound. As an example, let's assume that you have two classes, Cat and Dog, both inheriting from Animal, and that you have a covariant mutable List implementation. Say you have a value of type List[Cat]. Since List is covariant, this value can legally be passed to a function that expects a parameter of type List[Animal]. Now, imagine you have a function that expects a List[Animal] and adds a Dog to it. That's a legal operation: Dog extends Animal and can thus be used this way. Putting the two together, you have a perfectly legal way of adding a Dog to a List[Cat], which a sound type system should not allow. An example of that is Java's Array, which is both covariant and mutable, and that as a result can yield type errors at runtime.
mafribe 11y ago
I suspect that combining generics with subtyping might always lead you into the land on undecidable type-inference. After all, pure genericity (System F) is already undecidable.