Hello,

On Thu, Aug 23, 2012 at 2:03 AM, Simon Peyton-Jones <simonpj@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)
      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