[Haskell-cafe] Sound typeable via type families?

[Dan Doel]

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