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.]