<div dir="ltr"><div>I'll let you know as soon as I can what times I'm available Thursday/Friday. I don't know that the pattern I describe is common (now), but it's a straightforward application of constraints on GADT constructors. Whether people *like* such constraints is another question—there seem to be good reasons to use them and good reasons not to use them. At the moment, the lack of specialization is a good reason not to.<br><br>You'll see the same thing if you look at the Core for the code down below the line. By the way, I tried experimentally adding {-# SPECIALIZE eval :: Expr Int -> Int #-} and got a warning about the pragma being used on a non-overloaded function. In theory, the function is not overloaded, but in practice it effectively is; I would hope to be able to do that and get a specialized version like this:<br><br></div><div> evalInt :: Expr Int -> Int<br></div><div> evalInt (N n) = n<br></div><div> -- No B case, because Int is not Bool<br></div><div> evalInt (Add a b) = evalNum a `+.Int` evalNum b -- Specialized addition<br></div><div> evalInt (Mul a b) = evalNum a `*.Int` evalNum b -- Specialized multiplication<br></div><div> -- No EqNum case, because Int is not Bool<br></div><div><br>-- ----------------------------------------------<br><br>module Calc (checkInt, eval) where<br><br><br>data Expr a where<br> N :: Num n => n -> Expr n<br> B :: Bool -> Expr Bool<br> Add :: Num n => Expr n -> Expr n -> Expr n<br> Mul :: Num n => Expr n -> Expr n -> Expr n<br> EqNum :: (Num e, Eq e) => Expr e -> Expr e -> Expr Bool<br><br>infixl 6 `Add`<br>infixl 7 `Mul`<br>infix 4 `EqNum`<br><br>eval :: Expr a -> a<br>eval (N n) = n<br>eval (B b) = b<br>eval (Add a b) = evalNum a + evalNum b<br>eval (Mul a b) = evalNum a * evalNum b<br>eval (EqNum a b) = evalNum a == evalNum b<br><br>{-# SPECIALIZE evalNum :: Expr Int -> Int #-}<br>evalNum :: Num a => Expr a -> a<br>evalNum (N n) = n<br>evalNum (Add a b) = evalNum a + evalNum b<br>evalNum (Mul a b) = evalNum a * evalNum b<br><br>{-# SPECIALIZE check :: Int -> Int -> Int -> Bool #-}<br>check :: (Eq n, Num n) => n -> n -> n -> Bool<br>check x y z = eval $ N x `Add` N y `Mul` N z `EqNum` N z `Mul` N y `Add` N x<br><br>checkInt :: Int -> Int -> Int -> Bool<br>checkInt x y z = check x y z<br><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Oct 20, 2014 at 12:11 PM, Simon Peyton Jones <span dir="ltr"><<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div link="blue" vlink="purple" lang="EN-GB">
<div>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif"">David<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif""><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif"">If you want to suggest a couple of possible alternative 20-min slots in work time (London time zone), not Mon-Weds this week, then maybe we can find a mutually
convenient time.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif""><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif"">Do you have reason to suppose that the pattern you describe below is common? That is, if implemented, would it make a big difference to programs we care about?<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif""><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif"">Simon<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif""><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 #e1e1e1 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif"" lang="EN-US">From:</span></b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif"" lang="EN-US"> David Feuer [mailto:<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@gmail.com</a>]
<br>
<b>Sent:</b> 20 October 2014 13:58<br>
<b>To:</b> Simon Peyton Jones<br>
<b>Cc:</b> ghc-devs<br>
<b>Subject:</b> Re: Help understanding Specialise.lhs<u></u><u></u></span></p>
</div>
</div><div><div class="h5">
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:12.0pt;margin-left:0cm">
To be super-clear about at least one aspect: I don't want Tidy Core to ever contain something that looks like this:<br>
<br>
GADTTest.potato<br>
:: <a href="http://GHC.Types.Int" target="_blank">GHC.Types.Int</a> -> GADTTest.Silly
<a href="http://GHC.Types.Int" target="_blank">GHC.Types.Int</a> -> <a href="http://GHC.Types.Int" target="_blank">
GHC.Types.Int</a><br>
GADTTest.potato =<br>
\ (x_asZ :: <a href="http://GHC.Types.Int" target="_blank">GHC.Types.Int</a>)<br>
(ds_dPR :: GADTTest.Silly <a href="http://GHC.Types.Int" target="_blank">GHC.Types.Int</a>) -><br>
case ds_dPR of _ { GADTTest.Silly $dNum_aLV ds1_dPS -><br>
GHC.Num.+ @ <a href="http://GHC.Types.Int" target="_blank">GHC.Types.Int</a> $dNum_aLV x_asZ x_asZ<br>
}<u></u><u></u></p>
</div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
Here we see GHC.Num.+ applied to <a href="http://GHC.Types.Int" target="_blank">GHC.Types.Int</a> and $dNum_aLV. We therefore know that $dNum_aLV must be GHC.Num.$fNumInt, so GHC.Num.+ can eat these arguments and produce GHC.Num.$fNumInt_$c+. But for some
reason, GHC fails to recognize and exploit this fact! I would like help understanding why that is, and what I can do to fix it.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
On Mon, Oct 20, 2014 at 7:53 AM, David Feuer <<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@gmail.com</a>> wrote:<u></u><u></u></p>
<blockquote style="border:none;border-left:solid #cccccc 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<p>On Oct 20, 2014 5:05 AM, "Simon Peyton Jones" <<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>> wrote:<br>
> I’m unclear what you are trying to achieve with #9701. I urge you to write a clear specification that we all agree about before burning cycles hacking code.<u></u><u></u></p>
<p>What I'm trying to achieve is to make specialization work in a situation where it currently does not. It appears that when the type checker determines that a GADT carries a certain dictionary, the specializer happily uses it *even once the concrete type
is completely known*. What we would want to do in that case is to replace the use of the GADT-carried dictionary with a use of the known dictionary for that type.<u></u><u></u></p>
<p>> There are a lot of comments at the top of Specialise.lhs. But it is, I’m afraid, a tricky pass. I could skype.<u></u><u></u></p>
<p>I would appreciate that. What day/time are you available?<u></u><u></u></p>
</blockquote>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
</div></div></div>
</div>
</div>
</blockquote></div><br></div>