Help understanding Specialise.lhs

[David Feuer]

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.

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:

  evalInt :: Expr Int -> Int
  evalInt (N n) = n
  -- No B case, because Int is not Bool
  evalInt (Add a b) = evalNum a `+.Int` evalNum b -- Specialized addition
  evalInt (Mul a b) = evalNum a `*.Int` evalNum b -- Specialized
multiplication
  -- No EqNum case, because Int is not Bool

-- ----------------------------------------------

module Calc (checkInt, eval) where


data Expr a where
  N :: Num n => n -> Expr n
  B :: Bool -> Expr Bool
  Add :: Num n => Expr n -> Expr n -> Expr n
  Mul :: Num n => Expr n -> Expr n -> Expr n
  EqNum  :: (Num e, Eq e) => Expr e -> Expr e -> Expr Bool

infixl 6 `Add`
infixl 7 `Mul`
infix 4 `EqNum`

eval :: Expr a -> a
eval (N n) = n
eval (B b) = b
eval (Add a b) = evalNum a + evalNum b
eval (Mul a b) = evalNum a * evalNum b
eval (EqNum a b) = evalNum a == evalNum b

{-# SPECIALIZE evalNum :: Expr Int -> Int #-}
evalNum :: Num a => Expr a -> a
evalNum (N n) = n
evalNum (Add a b) = evalNum a + evalNum b
evalNum (Mul a b) = evalNum a * evalNum b

{-# SPECIALIZE check :: Int -> Int -> Int -> Bool #-}
check :: (Eq n, Num n) => n -> n -> n -> Bool
check x y z = eval $ N x `Add` N y `Mul` N z `EqNum` N z `Mul` N y `Add` N x

checkInt :: Int -> Int -> Int -> Bool
checkInt x y z = check x y z


On Mon, Oct 20, 2014 at 12:11 PM, Simon Peyton Jones <simonpj at microsoft.com>
wrote:

>  David
>
>
>
> 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.
>
>
>
> 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?
>
>
>
> Simon
>
>
>
> *From:* David Feuer [mailto:david.feuer at gmail.com]
> *Sent:* 20 October 2014 13:58
> *To:* Simon Peyton Jones
> *Cc:* ghc-devs
> *Subject:* Re: Help understanding Specialise.lhs
>
>
>
> To be super-clear about at least one aspect: I don't want Tidy Core to
> ever contain something that looks like this:
>
> GADTTest.potato
>   :: GHC.Types.Int -> GADTTest.Silly GHC.Types.Int -> GHC.Types.Int
> GADTTest.potato =
>   \ (x_asZ :: GHC.Types.Int)
>     (ds_dPR :: GADTTest.Silly GHC.Types.Int) ->
>     case ds_dPR of _ { GADTTest.Silly $dNum_aLV ds1_dPS ->
>     GHC.Num.+ @ GHC.Types.Int $dNum_aLV x_asZ x_asZ
>     }
>
> Here we see GHC.Num.+ applied to GHC.Types.Int 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.
>
>
>
> On Mon, Oct 20, 2014 at 7:53 AM, David Feuer <david.feuer at gmail.com>
> wrote:
>
> On Oct 20, 2014 5:05 AM, "Simon Peyton Jones" <simonpj at microsoft.com>
> wrote:
> > 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.
>
> 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.
>
> > There are a lot of comments at the top of Specialise.lhs.  But it is,
> I’m afraid, a tricky pass.  I could skype.
>
> I would appreciate that. What day/time are you available?
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20141020/fcbec527/attachment-0001.html>