Hello,<br><div class="gmail_quote"><div class="im"><div><br></div><div>On Thu, Aug 23, 2012 at 2:03 AM, Simon Peyton-Jones <span dir="ltr"><<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>></span> wrote:</div>
</div><div class="gmail_quote"><div class="im">
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div lang="EN-GB" link="blue" vlink="purple">
<div>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">I’m hazy about
<u></u><u></u></span></p>
<p><u></u><span style="font-size:11.0pt;font-family:Symbol;color:#1f497d"><span>·<span style="font:7.0pt "Times New Roman"">
</span></span></span><u></u><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">the definitions of sing and fromSing</span></p></div></div></blockquote></div><div><div>The family of singleton types, Sing, is quite general. However,</div>
<div>when its parameter is of kind `Nat`, then it is simply a newtype for `Integer`:</div><div><br></div><div> data family Sing (s :: a)</div><div> newtype instance Sing (s :: Nat) = SingN Integer</div><div><br></div>
<div>To access the `Integer` of a `Sing n` value we use the class `SingE`.</div><div>Again, this is just so that we can support arbitrary singletons, but</div><div>when the argument is of kind `Nat` we simply access the newtype's `Integer`:</div>
<div><br></div><div> instance SingE (n :: Nat) Integer where</div><div> fromSing (SingN x) = x</div><div><br></div><div>Finally, `Sing n` values are introduced with the following class:</div><div><br></div><div> class SingI n where</div>
<div> sing :: Sing n</div><div><br></div><div>The instances of this class when `n` is of kind `Nat` are built into GHC:</div><div>when GHC needs to solve constraint like `SingI 5`, the solver provides a</div><div>special piece of evidence, which is essentually 5</div>
<div>(actually, it is `EvLit (EvNum 5)`). When the evidence is desugered into Core,</div><div>this is replaced with just the integer 5. (Aside: this is not strictly</div><div>speaking correct---it should be replace with 5 coerced into `Sing 5`, which</div>
<div>should then be coerced into the dictionary for `SingI 5`. These all have</div><div>the same representation so things work for the time being, but this is certainly</div><div>on my TODO list to correct).</div></div>
<div class="im"><div>
<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div lang="EN-GB" link="blue" vlink="purple"><div><p><span style="font-size:11.0pt;font-family:Symbol;color:#1f497d"><span>·<span style="font:7.0pt "Times New Roman"">
</span></span></span><u></u><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">the transformations that are supposed to simplify (fromSing (sing :: Sing c)) to c</span></p>
</div></div></blockquote></div><div>So, now consider an expression like `fromSing (sing :: Sing 5)`.</div><div><div>With explicit dictionaries it becomes: `fromSing d1 (sing d2)`.</div><div><br></div><div>As we just discussed, `d2` is essentially 5, while `d1` will be the</div>
<div>function in the `fromSing` instance above, which is really just a coercion</div><div>because it accesses the field of a newtype. But note that so are</div><div>`sing` and `fromSing` because they are methods of classes with just</div>
<div>a single method! So this whole expressions really is a whole lot of</div><div>coercions around 5, which is why I'd expect this kind of pattern</div><div>to always be simplified.</div></div><div class="im"><div>
<br></div><div> </div>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div lang="EN-GB" link="blue" vlink="purple"><div><p><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"><u></u><u></u></span></p>
<p><u></u><span style="font-size:11.0pt;font-family:Symbol;color:#1f497d"><span>·<span style="font:7.0pt "Times New Roman"">
</span></span></span><u></u><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">the details of the two examples you describe and what isn’t happening that you expect to happen<u></u><u></u></span></p>
<p><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"><u></u></span></p></div></div></blockquote><div><br></div></div><div><div>Now for the example where I was expecting an optimization to happen</div>
<div>but it did not. Consider the following program, with the two different</div><div>definitions for `x`:</div><div><br></div><div> main :: IO ()</div><div> main = print (fromInteger x :: Int)</div><div> where</div>
<div> x = 5 :: Integer</div><div> -- x = fromSing (sing :: Sing 5)</div><div><br></div><div>With the first definition, where `x` is simply 5, the interesting</div><div>part of the Core looks like this:</div><div>
<br></div><div> main2 :: String</div><div> main2 = $wshowSignedInt 0 5 ([] @ Char)</div><div><br></div><div>What's nice about this is that GHC has noticed that it does not need to</div><div>make the intermediate `Integer` value, and replaced it with and `Int`.</div>
<div>If we use the second definition for `x`, then we get a slightly less efficint</div><div>version:</div><div><br></div><div> main3 :: Type.Integer</div><div> main3 = __integer 5</div><div><br></div><div> main2 :: String</div>
<div> main2 = case integerToInt main3 of</div><div> wild_ap2 { __DEFAULT -> $wshowSignedInt 0 wild_ap2 ([] @ Char) }</div><div><br></div><div>Note that, for some reason, the call to `integerToInt` is not eliminated.</div>
<div>I am not quite sure why that is.</div></div><span class="HOEnZb"><font color="#888888"><div><br></div><div><br></div><div>-Iavor</div></font></span><div><div class="h5"><div><br></div><div><br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div lang="EN-GB" link="blue" vlink="purple"><div><p><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">Can you give more specifics?<br>
<br>
S<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt">
<div>
<div style="border:none;border-top:solid #b5c4df 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span lang="EN-US" style="font-size:10.0pt;font-family:"Tahoma","sans-serif"">From:</span></b><span lang="EN-US" style="font-size:10.0pt;font-family:"Tahoma","sans-serif""> Iavor Diatchki [mailto:<a href="mailto:iavor.diatchki@gmail.com" target="_blank">iavor.diatchki@gmail.com</a>]
<br>
<b>Sent:</b> 23 August 2012 07:21<br>
<b>To:</b> Carter Schonwald<br>
<b>Cc:</b> Simon Peyton-Jones<br>
<b>Subject:</b> Re: question about type lits and optimization in ghc<u></u><u></u></span></p>
</div>
</div><div><div>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">Hello,<u></u><u></u></p>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<div>
<p class="MsoNormal">On Wed, Aug 22, 2012 at 10:15 PM, Carter Schonwald <<a href="mailto:carter.schonwald@gmail.com" target="_blank">carter.schonwald@gmail.com</a>> wrote:<u></u><u></u></p>
<div>
<p class="MsoNormal">I'm asking about whether or no the compile time machinery of ghc will be statically replacing "<span style="font-family:"Courier New"">fromSing (sing :: Sing c)</span>" with "c" when "c" is a specific number at compile time. <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">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:<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"> main :: IO ()<u></u><u></u></p>
</div>
<div>
<div>
<p class="MsoNormal"> main = print (fromSing (sing :: Sing 5))<u></u><u></u></p>
</div>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">results in core which looks like this:<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> main3 :: Integer</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> main3 = __integer 5</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> main2 :: [Char]</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> main2 = $w$cshowsPrec 0 main3 []</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> main1 :: State# RealWorld -> (# State# RealWorld, () #)</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> main1 = \ eta_B1 -> hPutStr2 stdout main2 True eta_B1</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> main4 :: State# RealWorld -> (# State# RealWorld, () #)</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> main4 = \ eta_Xa -> runMainIO1 main1 eta_Xa</span><u></u><u></u></p>
</div>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">This is pretty much the same code that one gets for `print 5`. I also tried a variation:<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> print (fromInteger (fromSing (sing :: Sing 5)) :: Int)</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">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?<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">-Iavor<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<blockquote style="border:none;border-left:solid #cccccc 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<div>
<div>
<div>
<div>
<p class="MsoNormal">On Thu, Aug 23, 2012 at 1:11 AM, Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com" target="_blank">iavor.diatchki@gmail.com</a>> wrote:<u></u><u></u></p>
<p class="MsoNormal">Hello,<u></u><u></u></p>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">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.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">So, for example, the indexing function might look something like this:<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> index :: forall r c a. SingI c => Matrix r c a -> Integer -> Integer -> a</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> index (Matrix arr) row col = arr ! (row * fromSing (sing :: Sing c) + col)</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">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`.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">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,<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">the expression:<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> index (Matrix m :: Matrix 3 4 Int) 1 2</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">should end up looking something like this:<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> m ! (1 * 4 + 2)</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">which should be simplified further to:<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> m ! 6 </span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">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.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">Cheers,<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">-Iavor<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:12.0pt"><u></u> <u></u></p>
<div>
<div>
<div>
<p class="MsoNormal">On Tue, Aug 21, 2012 at 11:14 AM, Carter Schonwald <<a href="mailto:carter.schonwald@gmail.com" target="_blank">carter.schonwald@gmail.com</a>> wrote:<u></u><u></u></p>
</div>
</div>
<blockquote style="border:none;border-left:solid #cccccc 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<div>
<div>
<p class="MsoNormal">Hey GHC folks!<u></u><u></u></p>
<div>
<p class="MsoNormal"> <u></u><u></u></p>
<div>
<p class="MsoNormal">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?)<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">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)<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">data Mat (row::Nat) (col::Nat) elem = ... some vector representation<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">index:: (Mat r c el) -> (Word,Word) -> el<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">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<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">representation<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">{-# perhaps an inline pragma? #-}<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">indexSpec3x3:: (Mat 3 3 el) -> (Word, Word) -> el<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">indexSpec3x3 smat ix = smat `index` ix<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">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?<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">Does my question even make sense as phrased?<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">thanks!<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="color:#888888"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="color:#888888">-Carter<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="color:#888888"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="color:#888888"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="color:#888888"><u></u> <u></u></span></p>
</div>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
</div>
<p class="MsoNormal" style="margin-bottom:12.0pt">_______________________________________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org" target="_blank">Glasgow-haskell-users@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/glasgow-haskell-users" target="_blank">http://www.haskell.org/mailman/listinfo/glasgow-haskell-users</a><u></u><u></u></p>
</blockquote>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
</div>
</div>
</blockquote>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
</div></div></div>
</div>
</div>
</blockquote></div></div></div><br>
</div><br>