Coercion as homomorphism: type inference in a system with subtyping and overloading

A type system with atomic subtyping and a special form of operator overloading, which we call oset-homomorphism is proposed. A set of operator overloadings is said to be oset-homomorphic when for each pair of overloadings the coercion function realises a homomorphism of types and at the same time certain conditions on the operator type signa- ture are satised. We demonstrate that oset-homomorphic overloading has sucient power for supporting a compre- hensive set of array operations in a declarative language. The problem of inferring the least types in our type system is proven to be equivalent to the shortest path problem for weighted, directed graphs with non-negative cycle weights, which has a computationally ecient solution.