#2439: Missed optimisation with dictionaries and loops -------------------------------------+------------------------------------- Reporter: rl | Owner: simonpj Type: bug | Status: new Priority: lowest | Milestone: 7.12.1 Component: Compiler | Version: 6.9 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Runtime | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by ekmett): Here's a worked version of the `SNat` thing I was talking about: {{{ {-# LANGUAGE RankNTypes, TypeOperators, GADTs, DataKinds #-} module SNat where import GHC.TypeLits import Unsafe.Coerce data SNat n where SNat :: KnownNat n => SNat n snatVal :: SNat n -> Integer snatVal n@SNat = natVal n instance Show (SNat n) where showsPrec d n = showsPrec d (snatVal n) newtype Magic n = Magic (KnownNat n => SNat n) add :: SNat n -> SNat m -> SNat (n + m) add n m = unsafeCoerce (Magic SNat) (snatVal n + snatVal m) mul :: SNat n -> SNat m -> SNat (n * m) mul n m = unsafeCoerce (Magic SNat) (snatVal n * snatVal m) }}} With that at the ghci prompt we can now look at `SNat`'s {{{ ghci> SNat :: SNat 32 32 }}} and I can work around the limitations of the nat solver, by helping it out as needed at the value level: {{{ ghci> add (SNat :: SNat 1) (SNat :: SNat 2) 3 }}} Then if I need the fabricated `KnownNat` instance for the sum I can just open up my `SNat` constructor and bring it into scope, like the Show instance just did. Here I had to make up my own `SNat` type as the one that is provided by GHC is actually not exported. `add` and `mul` are evil and unsafe, but here they do precisely the right thing. Their results are correct, even if the methodology is suspect. We get them by coercing `Magic n` into a function and passing it the value that is the representation of KnownNat. The core that gets generated is just that of explicit dictionary passing, same as with reflection. With `reflection` I relied on the quantifier when reifying to ensure things were generative. Here I rely on the fact that I'm working with singleton values, but the mechanism used to cheat the system is the same. The current `reflection` code looks similar, just using a different `Magic` type and some quantifier and `Proxy` noise to permit use in more situation. {{{ class Reifies s a | s -> a where reflect :: proxy s -> a newtype Magic a r = Magic (forall (s :: *). Reifies s a => Proxy s -> r) -- | Reify a value at the type level, to be recovered with 'reflect'. reify :: forall a r. a -> (forall (s :: *). Reifies s a => Proxy s -> r) -> r reify a k = unsafeCoerce (Magic k :: Magic a r) (const a) Proxy }}} In a world that was modified to make all dictionaries live inside a data type so they could be forced without consequence then I'd be changing `reify` to something more like: {{{ data Dictionary a = Dictionary a reify :: forall a r. a -> (forall (s :: *). Reifies s a => Proxy s -> r) -> r reify a k = unsafeCoerce (Magic k :: Magic a r) (Dictionary (const a)) Proxy }}} assuming that the dictionary representation and the representation of a data type with exactly one field (like `Dictionary`) were the same. I could patch around it if needed, but the proposal here seems odd to me. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/2439#comment:25 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler