## Question about type lits and optimization in ghc

2012-08-30 20:48:00 GMT

Hello,

I’m hazy about

· the definitions of sing and fromSing

· the transformations that are supposed to simplify (fromSing (sing :: Sing c)) to c

· the details of the two examples you describe and what isn’t happening that you expect to happen

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

_______________________________________________

Glasgow-haskell-users mailing list

Glasgow-haskell-users <at> haskell.org

http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users <at> haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users