Original Post
This is a bit of a theoretical problem: I have a set of types and a supertype relationship between them. I also have a function signature and several implementations of that function for various argument type combinations. I need to prove that, for any combination of argument types, there exists a single nonambiguous implementation that is compatible with this combination. An example:
Types : {A, B1, B2, C1, C2 } with A > B1 > B2 and A > C1 > C2 Function signature: f(A,A) Implementations: f(A,A); f(A,B1); f(B2,A); f(C1,C1); f(C2,C2) In this example, calling f with arguments of type (B2,B2) is problematic, since f(A,A); f(A,B1); f(B2,A) are all compatible with that argument combination, but there is not a single nonambiguous choice of implementation available.Note that ambiguity is not discussed in terms of distance, but rather in terms of lattices: an implementation f(x,y) is nonambiguous iff for each other implementation f(x',y') compatible with the arguments, x' ≥ x and y' ≥ y (that is, the implementation is better than all other implementations for each argument types). What efficient algorithms (or theoretical research) can I find about this problem?