30 Aug 2012 22:48

## Question about type lits and optimization in ghc

Hello,

On Thu, Aug 23, 2012 at 2:03 AM, Simon Peyton-Jones wrote:

·         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 ([] <at> Char)

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 ([] <at> 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 <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

Hello,

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?

-Iavor

On Thu, Aug 23, 2012 at 1:11 AM, Iavor Diatchki <iavor.diatchki <at> 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 <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

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

_______________________________________________

```_______________________________________________