Iavor Diatchki | 30 Aug 22:48 2012

Question about type lits and optimization in ghc


On Thu, Aug 23, 2012 at 2:03 AM, Simon Peyton-Jones <simonpj <at> microsoft.com> 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)
      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 ([] <at> 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

    main3 :: Type.Integer
    main3 = __integer 5

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

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




Can you give more specifics?



From: Iavor Diatchki [mailto:iavor.diatchki <at> 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




On Wed, Aug 22, 2012 at 10:15 PM, Carter Schonwald <carter.schonwald <at> 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?





On Thu, Aug 23, 2012 at 1:11 AM, Iavor Diatchki <iavor.diatchki <at> gmail.com> wrote:



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.





On Tue, Aug 21, 2012 at 11:14 AM, Carter Schonwald <carter.schonwald <at> 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


{-# 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?









Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org




Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org