On Friday 28 March 2008, Ryan Ingram wrote:
This is a really interesting idea. Sadly, I can't think of a way to make it work.
The biggest problem is the TEquality class; by putting teq in a typeclass, the decision of which teq to call (and thus, whether or not to return Just Refl or Nothing) is made at compile time. The GADT solution puts that decision off until run-time; the case statement in teq allows a decision to be made at that point.
What we'd really like to do is something like the following:
class Typeable t where data TypeRep t :: * typeRep :: TypeRep t typeEq :: forall t2. TypeRep t2 -> Maybe (TEq t t2)
instance Typeable Int where data TypeRep Int = TInt typeRep = TInt typeEq rep = case rep of TInt -> Just Refl _ -> Nothing
But you can't case analyze t2 in this way; each TypeRep is an independent data type and there's no way to determine which one you have (aside from some sort of typeable/dynamic constraint, and then we have a circular problem!)
Perhaps there is a solution, but I'm not clever enough to find it.
Yes, I thought about it a while longer after sending my mail, and I can't see an immediate way of making things work. I imagine one would need some sort of open GADTs to do the job. Currently we have two things that look close; GADTs which can hold the necessary evidence, but are closed, and type families, which are open, but don't allow inspection of values to direct typing. I suppose I was initially fooled by doing things like: cast () :: Maybe () ==> Just () Which looks just like Data.Typeable. However, when one goes to write more generic functions: foo x = case cast x of Just i -> (show :: Int -> String) i Nothing -> "Whatever." The type of foo ends up as '(TEquality a Int) => a -> String', which makes it a bit more clear that we're dealing with compile-time phenomena. I'll probably think on it some more, but I'm not holding out much hope at this point. Thanks for your thoughts, though (and, to Wolfgang, for the pointer to the other discussion, although I don't know if that or any of the new type families stuff coming in 6.10 will be the solution). -- Dan