Question about type lits and optimization in ghc

Iavor Diatchki iavor.diatchki at gmail.com
Thu Aug 30 22:48:00 CEST 2012


Hello,

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)
      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 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****
>
>  ** **
>
> ** **
>
>  ** **
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120830/9fe77925/attachment-0001.htm>


More information about the Glasgow-haskell-users mailing list