Re: [GHC] #2439: Missed optimisation with dictionaries and loops

8 Jul 2015

      #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