First-class types

[oleg@pobox.com]

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'