First-class types

[Jan-Willem Maessen]

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