- Paper [PDF]
Summary of review comments:
The paper describes a complex type system that can distinguish between certain object types that provide methods of the same signature, but behave differently in ways that may matter to the client. It's unclear why this particular distinction is exceptionally important: the client generally cares about all sorts of semantic properties that are not reflected in the type system. It is also generally very difficult to get complex type systems accepted into widely used programming languages. So while the paper provides a somewhat novel technique of modeling the type structure as a graph, and modeling subtyping as a graph algebra, it isn't clear that the type system is complete and solvable.
Regarding the question about the solvability of the type system, an initial idea/algorithm might be the following: compute the method interdependenies in the standard, structure-driven fashion.
ReplyDeleteFor example, let D(l) be the set of method labels on which the method l depends in an object; then for the object
[ l1 = 2, l2 = s.l1, l3 = 1 + s.l2],
we have
D(l3) = D(1) + D(s.l2)
= \emptyeset \union {l2}
={l2}
which means that the only method on which l3 depends is l2.