Hi, I'm late to reply, but I'd like to advocate a tagged type for typeRep, for a technical reason rather than usability and aesthetics. John Meacham wrote:
Proxy also has the advantage that it almost exactly mirrors what it ends up looking like in core. The application to proxy is the user visible type application.
But type applications can be safely erased by the compiler (in ghc's type class story, only dictionaries will be left -- jhc's story is different). With values, the compiler can never be sure whether they can be erased and therefore doesn't, except for some State# magic. I have been bitten by this difference when playing with type-level nats to implement modular arithmetic. I had code similar to the following. ------------------------------------------------------------------------ {-# LANGUAGE RankNTypes #-} module Nat (modulo) where data Z = Z newtype D1 a = D1 a newtype D2 a = D2 a class Nat a where nat :: a -> Integer instance Nat Z where nat = \_ -> 0 instance Nat a => Nat (D1 a) where nat = \(D1 a) -> 2*nat a + 1 instance Nat a => Nat (D2 a) where nat = \(D2 a) -> 2*nat a + 2 reflect :: (forall a . Nat a => a -> r) -> Integer -> r reflect f 0 = f Z reflect f n = case (n - 1) `divMod` 2 of (d, 0) -> reflect (f . D1) d (d, 1) -> reflect (f . D2) d ------------------------------------------------------------------------ Then I defined a type for integers modulo m, ------------------------------------------------------------------------ newtype R a = R { unR :: Integer } deriving (Eq, Ord, Show) rtag :: R a -> a rtag _ = undefined mkR :: Nat a => Integer -> R a mkR a = let res = R (a `mod` nat (rtag res)) in res instance Nat a => Num (R a) where R a + R b = mkR (a + b) R a * R b = mkR (a * b) R a - R b = mkR (a - b) fromInteger = mkR abs a = 1 signum a = a modulo :: (forall a . Num a => a) -> Integer -> Integer modulo f = reflect (unR . addR f) where addR :: Nat m => (forall a . Num a => a) -> m -> R m addR v _ = v ------------------------------------------------------------------------ The problem was, it's slow. Prelude NatP> modulo (product (map fromInteger [1..1000])) (3^500) `mod` 17 2 (0.25 secs, 426408368 bytes) Can you spot the reason? It took me a while to figure out. The problem is that due to the dummy parameter of 'nat', the modulus is recomputed all the time. One can mostly fix this (relying on let-floating) by using Proxy or changing the instances to ------------------------------------------------------------------------ instance Nat a => Nat (D1 a) where nat = \(D1 a) -> 2*nat (undefined `asTypeOf` a) + 1 instance Nat a => Nat (D2 a) where nat = \(D2 a) -> 2*nat (undefined `asTypeOf` a) + 2 ------------------------------------------------------------------------ but I feel the dummy parameter is ugly - we're representing constants by functions. The tagged representation, on the other hand, creates a class dictionary that contains the constant immediately. To wit, define Tag as ------------------------------------------------------------------------ newtype Tag t a = Tag a proxy :: (Tag t a) -> t -> a proxy (Tag a) _ = a tag :: (t -> a) -> Tag t a tag f = Tag (f undefined) ------------------------------------------------------------------------ and then we can implement the Nat typeclass as ------------------------------------------------------------------------ data Z = Z newtype D1 a = D1 a newtype D2 a = D2 a class Nat a where nat' :: Tag a Integer nat :: Nat a => a -> Integer nat = proxy nat' instance Nat Z where nat' = tag (\_ -> 0) instance Nat a => Nat (D1 a) where nat' = tag (\(D1 a) -> 2*nat a + 1) instance Nat a => Nat (D2 a) where nat' = tag (\(D2 a) -> 2*nat a + 2) reflect :: (forall a . Nat a => a -> r) -> Integer -> r reflect f 0 = f Z reflect f n = case (n - 1) `divMod` 2 of (d, 0) -> reflect (f . D1) d (d, 1) -> reflect (f . D2) d ------------------------------------------------------------------------ Note the use of 'proxy' and 'tag' to avoid most of the pain associated with using tagged types. They are small functions that are inlined and optimised away, and what remains will be the direct computation on class dictionaries that we're after. The rest of the code remains unchanged, and is much faster. Prelude NatT> modulo (product (map fromInteger [1..1000])) (3^500) `mod` 17 2 (0.01 secs, 3751624 bytes) In my view, Typeable and Nat serve a very similar purpose, namely associating a constant of some fixed type to another, varying type. Given that similarity, I feel that the same reasons as above apply to Typeable as well, suggesting to use a tagged type. Best regards, Bertram P.S. complete code is available from http://int-e.cohomology.org/~bf3/haskell/NatP.hs (dummy version) http://int-e.cohomology.org/~bf3/haskell/NatT.hs (tagged version) P.P.S. This is related to my favourite (ab)use of 'unsafeCoerce' -- ghc only -- equivalent to 'reflect', tagged version: reflect' :: (forall a . Nat a => a -> r) -> Integer -> r reflect' f = fromDict (tag f) where fromDict :: (forall a . Nat a => Tag a r) -> Integer -> r fromDict = unsafeCoerce