First-class types

[Simon Peyton-Jones]

| 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=20
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
=09

class D a1 a2 b | a1 a2-> b where
  typeof :: a1 -> a2 -> b
=20
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
 =20
instance Coerce () Int where
    coerce _ _ =3D 0

instance Coerce () Float where
    coerce _ _ =3D 0

instance Coerce Int Int where
    coerce =3D const

instance Coerce Float Float where
    coerce =3D const

instance Coerce Int Float where
    coerce x _ =3D fromInteger $ toInteger x
=20
instance Coerce Bool Int where
    coerce True _ =3D 1
    coerce False _ =3D 0

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