| 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'
Simon PJ replies:
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.
I agree. I like it when this sort of thing can be reduced to just a few lines of code. I suspect it is possible to turn "coerce" and/or "typeof" into some sort of "asTypeOf"-like operator and avoid the creation of undefined proxies for the result type. Indeed, perhaps we want a definition such as this (untested, but probably subtly wrong):
class (Coerce a1 b, Coerce a2 b) => D a1 a2 b | a1 a2 -> b where lift2 :: (b -> b -> b) -> a1 -> a2 -> b lift2 op = op' where op' a b = op (coerce a) (coerce b)
class Coerce a b where coerce :: a -> b
-- lots of instances here.
add = lift2 (+) sub = lift2 (-)
In general, if D is being used only to define coercions on a binary operation, thenin my opinion the class method ought to be a coercion on a binary operation. But I had a couple of questions for the avid type-hackers out there, motivated by this example and by similar examples from my own tinkerings: 1) Coerce a a can be defined as coerce=id for all a. However, this may of course lead to overlap in the type structure, so we must write a separate instance definition for Coerce Int Int, Coerce Double Double, etc. if we want types to be decidable. I'd love for some clever person to solve this little difficulty. 2) When we define D a b c, we know that D b a c is also allowed. Again, decidability prevents us from asserting this directly. Again, a clever solution could save us a lot of code and even more debugging. I suspect this may be a marginally easier nut to crack than the previous one. So, type hackers, can you come up with a Byzantine set of classes which encode these restrictions nicely and decidably? -Jan-Willem Maessen [Note that I suspect that it maybe possible to *prove* that you can't, at least for case 1. If you're really ambitious, you might want to attack transitivity of coercion, too.]
participants (2)
-
Jan-Willem Maessen -
Simon Peyton-Jones