[Haskell-cafe] Sound typeable via type families?
ryani.spam at gmail.com
Fri Mar 28 15:07:55 EDT 2008
On 3/27/08, Dan Doel <dan.doel at gmail.com> wrote:
> class Typeable t where
> data TypeRep t :: *
> typeRep :: TypeRep t
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.
More information about the Haskell-Cafe