Isto Aho:

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 ...

In the definition, the upper function only has one argument...

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?

Using your idea of separating the lattice and conversion from the definition of multiplication, you can at least save yourself the class instances: {-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-} {-# LANGUAGE FlexibleContexts, FlexibleInstances, UndecidableInstances #-} type family Join a b :: * type instance Join Int Int = Int type instance Join Float Float = Float type instance Join Int Float = Float type instance Join Float Int = Float class Conv a b where conv :: a -> b instance Conv Int Float where conv = fromIntegral instance Conv Int Int where conv = id instance Conv Float Float where conv = id class Mul a b where mul :: a -> b -> Join a b instance (Conv a (Join a b), Conv b (Join a b), Num (Join a b)) => Mul a b where mul x y = conv x * conv y You will have to write quite a lot of type instances of Join. However, the rest of the code is as concise as you seem to want it. You could even do better with Join by using more sophisticated type- level data structures; i.e., you could define type-level association lists and define Join as a type-level lookup function, including rules for reflexivity and symmetry, on those lists. In other words, instead of hard-coding the laws of lattices into the compiler, you'd just programatically define them as part of your type-level program. This is more flexible, as I am sure there are other applications, where we don't want a lattice, but some other structure. See also Andrew Appleyard's recent BSc thesis on how a similar approach can be used to embed the type structure of a different programming language in Haskell. In his case, this was the subtyping relation of C#: http://www.cse.unsw.edu.au/~pls/thesis/aja-thesis.pdf Manuel PS: The use of UndecidableInstances in the above code is a bit unfortunate, but it is forced on us by the rather complicated instance context of Mul (even if the above set of family and class instances is of course perfectly decidable - GHC just can't tell that easily).