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****

** **

** **

** **