Hi all, I was trying to solve a problem and by chance found texts on functional dependencies and then on type families (papers, ghc docs). Please, consider the example 03 of "Understanding functional dependencies via Constraint Handling rules" by Sulzmann, Duck, Peyton-Jones and Stuckey. There we are defining a multiplication over different numeric types: class Mul a b c | a b -> c where (*) :: a -> b -> c instance Mul Int Int Int where ... instance Mul Int Float Float where ... Ok, we could add instance Mul Float Int Float where ... but if we want to make everything work nicely together, Integer, Complex, Rational etc, there will be a lot of instances, especially if we have to give both "Float Int" and "Int Float" instances. And now the question on "lattices of types" (didn't know any better name to refer to the following): Is the following possible? Or can something similar achieved with type families (easily)? type lattice T a b -- Each of the following gives a "<"-relation between types, -- "upper" gives a method, how we get the larger (2nd) from -- the smaller (1st). lattice instance T Int Integer where upper = fromIntegral lattice instance T Int Float where upper = fromIntegral lattice instance T Integer (Ratio Integer) where upper = ... lattice instance T (Ratio Integer) Double where ... lattice instance T Float Double ... lattice instance T Double (Complex Double) ... -- e.g. Now the compiler can check that the top type is -- unique and that there is a path from every type to the top type. -- If the compiler founds this not to be the case, an error is output. -- But otherwise there can be types that are not comparable but -- the common top is quaranteed to exist. class Mul a b c where lattice T (*) :: a -> b -> c (*) x y = (upper x y x) * (upper x y y) -- Now there is no need for the instances like. instance Mul Int Float Float where ... instance Mul Float (Ratio Integer) Double where ... The compiler can generate those instances, because we have given the "upper"-methods. There is always the top available. Function (*) x y = (upper x y x) * (upper x y y) might could be replaced with (*) x y = x * y because of the presence of lattice T and thus, the "upper"-function. If this were possible, the benefits would be: - No need to state "Int Float" and "Float Int" instances on cases where the operands do commute. - No need to write a large number of instances if you have several "types on lattice" (e.g. some more or less well defined relation). - If the relation between types is not clear, we could define another lattice T2 to our Mul2 class for the other uses. Continuing the idea: we could override the default instances generated by the compiler with our own instances when needed. Ok, so, is it possible to write something like that already? (I just wouldn't like write a lot of instances...) If not, would it be possible to extend, say ghc, to work that way or are there too much inconsistencies in the above presentation? (Yes, where is the bottom. Why top and not bottom? Should it be possible to tell, which one to use, if both present? e.g.) Thanks for reading this far! -- br, Isto