Question about type lits and optimization in ghc

30 Aug 2012

      Hello,

On Thu, Aug 23, 2012 at 2:03 AM, Simon Peyton-Jones
wrote:
...
I’m hazy about ****
**·         **the definitions of sing and fromSing
The family of singleton types, Sing, is quite general.  However,
when its parameter is of kind `Nat`, then it is simply a newtype for
`Integer`:

    data family Sing (s :: a)
    newtype instance Sing (s :: Nat) = SingN Integer

To access the `Integer` of a `Sing n` value we use the class `SingE`.
Again, this is just so that we can support arbitrary singletons, but
when the argument is of kind `Nat` we simply access the newtype's `Integer`:

    instance SingE (n :: Nat) Integer where
      fromSing (SingN x) = x

Finally, `Sing n` values are introduced with the following class:

    class SingI n where
      sing :: Sing n

The instances of this class when `n` is of kind `Nat` are built into GHC:
when GHC needs to solve constraint like `SingI 5`, the solver provides a
special piece of evidence, which is essentually 5
(actually, it is `EvLit (EvNum 5)`).  When the evidence is desugered into
Core,
this is replaced with just the integer 5.  (Aside: this is not strictly
speaking correct---it should be replace with 5 coerced into `Sing 5`, which
should then be coerced into the dictionary for `SingI 5`.  These all have
the same representation so things work for the time being, but this is
certainly
on my TODO list to correct).

·         **the transformations that are supposed to simplify (fromSing
...
(sing :: Sing c)) to c
So, now consider an expression like `fromSing (sing :: Sing 5)`.
With explicit dictionaries it becomes: `fromSing d1 (sing d2)`.

As we just discussed, `d2` is essentially 5, while `d1` will be the
function in the `fromSing` instance above, which is really just a coercion
because it accesses the field of a newtype.   But note that so are
`sing` and `fromSing` because they are methods of classes with just
a single method!  So this whole expressions really is a whole lot of
coercions around 5, which is why I'd expect this kind of pattern
to always be simplified.
...
****
**·         **the details of the two examples you describe and what isn’t
happening that you expect to happen****
**
Now for the example where I was expecting an optimization to happen
but it did not.  Consider the following program, with the two different
definitions for `x`:

    main :: IO ()
    main = print (fromInteger x :: Int)
      where
      x = 5 :: Integer
      -- x = fromSing (sing :: Sing 5)

With the first definition, where `x` is simply 5, the interesting
part of the Core looks like this:

    main2 :: String
    main2 = $wshowSignedInt 0 5 ([] @ Char)

What's nice about this is that GHC has noticed that it does not need to
make the intermediate `Integer` value, and replaced it with and `Int`.
If we use the second definition for `x`, then we get a slightly less
efficint
version:

    main3 :: Type.Integer
    main3 = __integer 5

    main2 :: String
    main2 = case integerToInt main3 of
              wild_ap2 { __DEFAULT -> $wshowSignedInt 0 wild_ap2 ([] @
Char) }

Note that, for some reason, the call to `integerToInt` is not eliminated.
I am not quite sure why that is.

-Iavor
...
**
Can you give more specifics?
S****
** **
*From:* Iavor Diatchki [mailto:iavor.diatchki@gmail.com]
*Sent:* 23 August 2012 07:21
*To:* Carter Schonwald
*Cc:* Simon Peyton-Jones
*Subject:* Re: question about type lits and optimization in ghc****
** **
Hello,****
** **
On Wed, Aug 22, 2012 at 10:15 PM, Carter Schonwald <
carter.schonwald@gmail.com> wrote:****
I'm asking about whether or no the compile time machinery of ghc will be
statically replacing "fromSing (sing :: Sing c)"  with "c" when "c" is a
specific number at compile time.  ****
** **
Yes, the intention is that this should be simplified into the
corresponding the value `c` of type `Integer`.  I just run a small test.
 This program:****
** **
main :: IO ()****
main = print (fromSing (sing :: Sing 5))****
** **
results in core which looks like this:****
** **
main3 :: Integer****
main3 = __integer 5****
** **
main2 :: [Char]****
main2 = $w$cshowsPrec 0 main3 []****
** **
main1 :: State# RealWorld -> (# State# RealWorld, () #)****
main1 = \ eta_B1 -> hPutStr2 stdout main2 True eta_B1****
** **
main4 :: State# RealWorld -> (# State# RealWorld, () #)****
main4 = \ eta_Xa -> runMainIO1 main1 eta_Xa****
** **
This is pretty much the same code that one gets for `print 5`.  I also
tried a variation:****
** **
print (fromInteger (fromSing (sing :: Sing 5)) :: Int)****
** **
While this also gets simplified to the integer 5, it does not work quite
as well as `print (fromIntegr 5 :: Int)`, which goes directly to an `Int`
without going through an `Integer` first.  I suspect that the reason for
this is that there is some RULE which is not firing, but I'll have to look
into what's going on in a bit more detail.  Perhaps Simon has an idea?****
** **
-Iavor****
** **
** **
On Thu, Aug 23, 2012 at 1:11 AM, Iavor Diatchki <
iavor.diatchki@gmail.com> wrote:****
Hello,****
** **
There are no custom optimizations specifically for type-literals but GHC's
usual optimizations should work well in examples like yours because using a
singleton value is essentially the same as writing the corresponding value
level literal.****
So, for example, the indexing function might look something like this:****
** **
index :: forall r c a. SingI c => Matrix r c a -> Integer -> Integer
-> a****
index (Matrix arr) row col = arr ! (row * fromSing (sing :: Sing c) +
col)****
** **
Here, the `SingI` constraint says that we are going to be using the
singleton value associated with type `c`.  The function `fromSing` converts
this singleton value into an ordinary `Integer`.****
** **
Now, if we use `index` in a context where the dimensions of the matrix are
known, then GHC will resolve the constraint and pass the corresponding
value to `index`.  For example, assuming that `index` gets inlined,****
the expression:****
** **
index (Matrix m :: Matrix 3 4 Int) 1 2****
** **
should end up looking something like this:****
** **
m ! (1 * 4 + 2)****
****
which should be simplified further to:****
** **
m ! 6 ****
** **
Does that answer your question?  Please ask away if something does not
make sense, or if you notice that things do not work as expected.****
** **
Cheers,****
-Iavor****
** **
On Tue, Aug 21, 2012 at 11:14 AM, Carter Schonwald <
carter.schonwald@gmail.com> wrote:****
Hey GHC folks!****
****
In the case where type lits (naturals specifically) are statically known
(rather than abstract), is it possible to have a sort of static copy
propagation / Singelton simplification happen at compile time? (Ie can GHC
do such things with  type lits as presently implemented?)****
** **
a simple example might be that a statically sized matrix, and being able
to specialize the stride and bounds checking at compile time (pseudo code
example follows)****
** **
data Mat (row::Nat) (col::Nat) elem = ... some vector representation****
** **
** **
index:: (Mat r c  el) -> (Word,Word) -> el****
index mt ix = ... some stride based indexing calculation that gets at the
"r"  and "c" numbers via the singletons  to translate the ix tuple into the
index into the underlying vector****
representation****
{-# perhaps an inline pragma? #-}****
** **
indexSpec3x3:: (Mat 3 3 el) -> (Word, Word) -> el****
indexSpec3x3 smat ix = smat `index` ix****
** **
under what circumstances can i get something like the body of indexSpec3x3
to use the static type level natural number machinery to partially
specialize the computation?****
Does my question even make sense as phrased?****
** **
thanks!****
** **
-Carter****
** **
** **
** **
** **
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users****
** **
** **
** **