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. As an example, we define a _function_ (not a method!) 'add' such that: Main> add True False 1 Main> add () (5::Int) 5 Main> add () (5::Float) 5.0 Main> add (4::Int) True 5 Main> add (10::Int) (5::Float) 15.0 The example works both in GHC and Hugs. The signature of add is quite revealing: forall b a2 a1. (Num b, Coerce a2 b, Coerce a1 b, D a1 a2 b) => a1 -> a2 -> b That is, 'add' is capable of adding any two _things_, provided they both can be "generalized" and "coerced" into a number. The "type function" D computes the generalization of two types -- in a manner we specify. The function add is actually quite simple:

add x y = let general_type = typeof x y x' = coerce x general_type y' = coerce y general_type in x' + y'

The function 'typeof' is also interesting. It has a type forall b a2 a1. (D a1 a2 b) => a1 -> a2 -> b Note that it returns 'b' forall b! In a sense, the function performs a type computation at run time. The code follows. We should note that we could have achieved the same effect by defining an appropriate class with the method 'add'. In our solution however, the acts of generalizing, coercion, and addition are all separated. If we later decide to subtract things rather than add them, we do not need to alter the class and all the instances. We merely need to introduce the subtraction function. This makes the maintenance of the code easier. The distinct characteristic of the following code is an indirect manipulation of an untouchable, existential value. We were able to force a value to be of a specific type without any means of accessing the value directly.

class Type a where name :: a -> String

instance Type Bool where name a = "Bool"

instance Type Int where name a = "Int"

--instance Type Char where -- name a = "Char"

instance Type () where name a = "()"

instance Type Float where name a = "Float"

-- Type generalization function: type -> type -> type class (Type b) => D a1 a2 b | 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

newtype M a1 a2 = M (forall b.(D a1 a2 b) => b) data M1 a1 a2 = M1 a1 a2 (M a1 a2) typeof v1 v2 = case (M1 v1 v2 (M undefined)) of M1 _ _ (M y) -> y typeof1 v1 v2 = case (M1 v1 v2 (M undefined)) of M1 _ _ y -> y

add x y = let general_type = typeof x y x' = coerce x general_type y' = coerce y general_type in x' + y'