Changes to Typeable

[Bertram Felgenhauer]

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