| The following is a more flexible alternative to overloading. We | essentially define a function on types and invoke it, seemingly at run | time. No Dynamics or unsafe computations are employed. We only need | existential types, multi-parameter classes and functional | dependencies. The code also shows how to manipulate values which | cannot be manipulated. Ingenious, but unnecessarily complicated. You don't need existential types at all. (See the code below, which is considerably simpler and, I fancy, a bit more efficient.) Also, I'm not sure why you make 'Type' (which is pretty much the Typable class in the Dynamic library) into a superclass of D; it's not used. The idea of using a value (which is never evaluated) as a proxy for a type is exactly what the Typable class does. Indeed, it is a really useful technique. The clever things about your solution are a) You avoid the nasty ambiguity trap that many such schemes fall into e.g. when you see (a + b) * (c-d), what is type are the intermediate values (a+b) and (c-d). You drive the type of the result from the type of the arguments, which makes sense. (Albeit, if you you want to add two Floats and get an Int, you'll have to do a conversion at the end.) b) You separate the coercion stuff from the operations in a nice way. Simon class D a1 a2 b | a1 a2-> b where typeof :: a1 -> a2 -> b instance D Bool Bool Int instance D Int Bool Int instance D Bool Int Int instance D Int Int Int instance D () Int Int instance D Int () Int instance D () () Int instance D Int Float Float instance D () Float Float instance D Float Int Float instance D Float Float Float -- The coercion function class Coerce a b where coerce :: a -> b -> b instance Coerce () Int where coerce _ _ = 0 instance Coerce () Float where coerce _ _ = 0 instance Coerce Int Int where coerce = const instance Coerce Float Float where coerce = const instance Coerce Int Float where coerce x _ = fromInteger $ toInteger x instance Coerce Bool Int where coerce True _ = 1 coerce False _ = 0 add x y = let general_type = typeof x y x' = coerce x general_type y' = coerce y general_type in x' + y'