Changes to Typeable
Bertram Felgenhauer
bertram.felgenhauer at googlemail.com
Mon Mar 12 08:32:00 CET 2012
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
More information about the Libraries
mailing list