RE: An idea for a different style of metaprogramming evaluation using the optimiser

2018-05-25 Thread Simon Peyton Jones via ghc-devs
(Clearing up my inbox.)

Sorry to be slow on this Matthew.

A difficulty I see is that the optimiser must exhaustively evaluate until it 
gets to a quote.  And that is not easy if you had

   $$$(if  (reverse [1,2,3] == [3,2,1]) then .. else .. )

you'd probably get stuck.  Or at least you'd have to be able to inline reverse, 
and (==) and all the typeclass machinery for dealing with (==).

A merit of the current setup is that evaluation in a splice can call arbitrary 
libraries, including compiled ones (not just bytecode!). 

Also the current setup lets you inspect the environment a bit with the Q monad.

We already have typed and untyped TH; as yet I'm not convinced that the 
advantages of a third route would pay for the costs. But don't let me 
discourage you.  I love being convinced!

(Bandwidth to think about this is limited though, hence delay.)

Simon   

|  -Original Message-
|  From: Matthew Pickering 
|  Sent: 27 February 2018 11:18
|  To: Simon Peyton Jones 
|  Subject: Re: An idea for a different style of metaprogramming
|  evaluation using the optimiser
|  
|  Sorry I wasn't clear. I'll try to flesh out the power example in much
|  more detail. The general idea is that instead of using the bytecode
|  interpreter in order to evaluate splices, the optimiser is often
|  sufficient.
|  
|  The benefits of this are:
|  
|  1. Cross platform.
|  2. Simpler to use as you are not manually creating ASTs
|  3. More predictable as there are never any IO actions.
|  
|  The motivation is to precisely tell the inliner what to do rather than
|  trying to convince it to do what you like as it is quite
|  unpredictable.
|  
|  
|  Take the staged power example.
|  
|  ```
|  power :: Int -> R Int -> R Int
|  power n k = if n == 0
|  then .< 1 >.
|  else .< ~k * ~(power (n-1) k) >.
|  ```
|  
|  I propose introducing two new pieces of syntax $$$(..) and [||| ...
|  |||] which are pronounced splice and quote. We also introduce a new
|  type constructor R, for representation. We can informally give the
|  types
|  of quote and splice as a -> R a and R a -> a respectively.
|  
|  What are the limitations of $$$() and [||| |||]? The only way to make
|  `R` fragments is by quoting. It is also not allowed to inspect the
|  quoted code. The only way to interact with it is by splicing.
|  
|  Which would then mean we staged power like so.
|  
|  
|  ```
|  power :: Int -> R Int -> R Int
|  power n k = if n == 0
|  then [||| 1 |||].
|  else [||| $$$(k) * $$$(power k (n-1)) |||]
|  ```
|  
|  Then to use power, we might call it like..
|  
|  ```
|  $$$(power 3 [||| x |||])
|  ```
|  
|  which we hope evaluates to x * x * x * 1.
|  
|  The difference I am proposing is that instead of the bytecode
|  interpreter evaluating the splice, it is the optimiser which does the
|  evaluation.
|  
|  Concretely, we interpret a splice meaning "evaluate as much as
|  possible" and a quote as meaning "don't evaluate me any more".
|  By evaluate as much as possible, this means to be very keen to inline
|  functions including recursive ones. This sounds bad but it is the user
|  who is in control by
|  where they put the annotations.
|  
|  So in this example, we would evaluate as follows.. E marks an
|  "evaluation context" where we are very keen to evaluate.
|  
|  ```
|  $$$(power 1 [||| x |||])
|  =>
|  E: power 1 [||| x |||]
|  =>
|  E: if 1 == 0 then [||| 1 |||] else ...
|  => (Eval condition)
|  E: [||| $$$([||| x |||]) * $$$(power (1-0)) k |||]
|  => (Quote removes evaluation context)
|  $$$([||| x |||]) * $$$(power (1-0) k)
|  => (Eval $$$(k))
|  x * $$$(power  (1-0) k)
|  => (Eval $$$(power (1-0) k)
|  k * E: power (1 - 0) k
|  => (Unroll as we are in E)
|  k * E: if 0 == 0 then [||| 1 |||] ...
|  =>
|  k* E: [||| 1 |||]
|  =>
|  k * 1
|  ```
|  
|  So we can completely evaluate the splices properly in the evaluator if
|  the definitions are simple enough.
|  In this example, that isn't actually going to be the case as the
|  optimiser doesn't evaluate `3 == 0` for integers because it is
|  implemented using a primitive.
|  
|  If we rewrite the example using an inductive data type for the
|  recursive argument then we can see that it would work correctly.
|  
|  ```
|  data Nat = Z | S Nat
|  
|  power :: Nat -> R Int -> R Int
|  power n k = case n of
|  Z -> [||| 1 |||]
|  (S n) -> [||| $$$(k) * $$$(power n k) |||]
|  ```
|  
|  Then it is perhaps clearer that the optimiser is all we need in order
|  to evaluate $$$(power (S Z) [||| x |||]). The current implementation
|  of $$ and [||] would invoke the bytecode interpreter to do this
|  evaluation but it is unnecessary for this simple example which the
|  optimiser could do just as well.
|  
|  ```
|  $$$

Re: An idea for a different style of metaprogramming evaluation using the optimiser

2018-02-28 Thread Joachim Breitner
> In my hacked together implementation of this, constant folding happens
too late so only the algebraic version teminated.

ah, very good point!

Joachim 



Am 28. Februar 2018 06:26:35 EST schrieb Matthew Pickering 
:
>You have identified a small inaccuracy in my original email.
>
>It is true that ultimately 3 == 0 will be evaluated but these constant
>folding opportunities are only applied later after other inlining
>takes place.
>
>It becomes quite crucial under this scheme when different
>optimisations happen because when we inline a recursive function, we
>have to make sure to apply the right evaluation steps before trying to
>simplify the function body.
>In my hacked together implementation of this, constant folding happens
>too late so only the algebraic version teminated.
>
>Cheers,
>
>Matt
>
>On Tue, Feb 27, 2018 at 5:01 PM, Joachim Breitner
> wrote:
>> Hi,
>>
>> something like this would be great. I don’t have a sense yet of what
>> “something” should be like.
>>
>>
>> Am Dienstag, den 27.02.2018, 09:59 + schrieb Matthew Pickering:
>>> To go back to the power example, the recursive
>>> condition would have to be an inductively defined natural (data N =
>Z
>>> | S N) rather than an Int as the comparison operator for integers
>>> can't be evaluated by the optimiser.
>>
>> Sure they can:
>>
>> $ cat ConstantFolding.hs
>> {-# LANGUAGE TemplateHaskell #-}
>> {-# OPTIONS_GHC -fplugin=Test.Inspection.Plugin #-}
>> module ConstantFolding where
>>
>> import Test.Inspection
>>
>> ltInt :: Bool
>> ltInt = (3::Int) > 2
>>
>> ltInteger :: Bool
>> ltInteger = (3::Integer) > 2
>>
>> true :: Bool
>> true = True
>>
>>
>> inspect $ 'ltInt === 'true
>> inspect $ 'ltInteger === 'true
>>
>> $ ghc -O ConstantFolding.hs
>> [1 of 1] Compiling ConstantFolding  ( ConstantFolding.hs,
>> ConstantFolding.o )
>> ConstantFolding.hs:17:1: ltInt === true passed.
>> ConstantFolding.hs:18:1: ltInteger === true passed.
>> inspection testing successful
>>   expected successes: 2
>>
>>
>>
>> As  an alternative with a maybe simpler user interface (and probably
>> less power), I wonder if we can create a magic function
>>> compileTimeWHNF :: a -> a
>> or
>>> compileTimeNF :: a -> a
>> and a GHC core plugin (or eventually built-in thing) that finds these
>> magic functions and evaluates their arguments, using the simplifier.
>>
>>
>> Cheers,
>> Joachim
>>
>> --
>> Joachim Breitner
>>   m...@joachim-breitner.de
>>   http://www.joachim-breitner.de/
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: An idea for a different style of metaprogramming evaluation using the optimiser

2018-02-28 Thread Matthew Pickering
You have identified a small inaccuracy in my original email.

It is true that ultimately 3 == 0 will be evaluated but these constant
folding opportunities are only applied later after other inlining
takes place.

It becomes quite crucial under this scheme when different
optimisations happen because when we inline a recursive function, we
have to make sure to apply the right evaluation steps before trying to
simplify the function body.
In my hacked together implementation of this, constant folding happens
too late so only the algebraic version teminated.

Cheers,

Matt

On Tue, Feb 27, 2018 at 5:01 PM, Joachim Breitner
 wrote:
> Hi,
>
> something like this would be great. I don’t have a sense yet of what
> “something” should be like.
>
>
> Am Dienstag, den 27.02.2018, 09:59 + schrieb Matthew Pickering:
>> To go back to the power example, the recursive
>> condition would have to be an inductively defined natural (data N = Z
>> | S N) rather than an Int as the comparison operator for integers
>> can't be evaluated by the optimiser.
>
> Sure they can:
>
> $ cat ConstantFolding.hs
> {-# LANGUAGE TemplateHaskell #-}
> {-# OPTIONS_GHC -fplugin=Test.Inspection.Plugin #-}
> module ConstantFolding where
>
> import Test.Inspection
>
> ltInt :: Bool
> ltInt = (3::Int) > 2
>
> ltInteger :: Bool
> ltInteger = (3::Integer) > 2
>
> true :: Bool
> true = True
>
>
> inspect $ 'ltInt === 'true
> inspect $ 'ltInteger === 'true
>
> $ ghc -O ConstantFolding.hs
> [1 of 1] Compiling ConstantFolding  ( ConstantFolding.hs,
> ConstantFolding.o )
> ConstantFolding.hs:17:1: ltInt === true passed.
> ConstantFolding.hs:18:1: ltInteger === true passed.
> inspection testing successful
>   expected successes: 2
>
>
>
> As  an alternative with a maybe simpler user interface (and probably
> less power), I wonder if we can create a magic function
>> compileTimeWHNF :: a -> a
> or
>> compileTimeNF :: a -> a
> and a GHC core plugin (or eventually built-in thing) that finds these
> magic functions and evaluates their arguments, using the simplifier.
>
>
> Cheers,
> Joachim
>
> --
> Joachim Breitner
>   m...@joachim-breitner.de
>   http://www.joachim-breitner.de/
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: An idea for a different style of metaprogramming evaluation using the optimiser

2018-02-27 Thread Sebastian Graf
Hey Matt,

cool idea! Also it looks like such a tool could 'solve' stream fusion:
https://ghc.haskell.org/trac/ghc/ticket/915#comment:52

Greetings
Sebastian

2018-02-27 18:01 GMT+01:00 Joachim Breitner :

> Hi,
>
> something like this would be great. I don’t have a sense yet of what
> “something” should be like.
>
>
> Am Dienstag, den 27.02.2018, 09:59 + schrieb Matthew Pickering:
> > To go back to the power example, the recursive
> > condition would have to be an inductively defined natural (data N = Z
> > | S N) rather than an Int as the comparison operator for integers
> > can't be evaluated by the optimiser.
>
> Sure they can:
>
> $ cat ConstantFolding.hs
> {-# LANGUAGE TemplateHaskell #-}
> {-# OPTIONS_GHC -fplugin=Test.Inspection.Plugin #-}
> module ConstantFolding where
>
> import Test.Inspection
>
> ltInt :: Bool
> ltInt = (3::Int) > 2
>
> ltInteger :: Bool
> ltInteger = (3::Integer) > 2
>
> true :: Bool
> true = True
>
>
> inspect $ 'ltInt === 'true
> inspect $ 'ltInteger === 'true
>
> $ ghc -O ConstantFolding.hs
> [1 of 1] Compiling ConstantFolding  ( ConstantFolding.hs,
> ConstantFolding.o )
> ConstantFolding.hs:17:1: ltInt === true passed.
> ConstantFolding.hs:18:1: ltInteger === true passed.
> inspection testing successful
>   expected successes: 2
>
>
>
> As  an alternative with a maybe simpler user interface (and probably
> less power), I wonder if we can create a magic function
> > compileTimeWHNF :: a -> a
> or
> > compileTimeNF :: a -> a
> and a GHC core plugin (or eventually built-in thing) that finds these
> magic functions and evaluates their arguments, using the simplifier.
>
>
> Cheers,
> Joachim
>
> --
> Joachim Breitner
>   m...@joachim-breitner.de
>   http://www.joachim-breitner.de/
>
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: An idea for a different style of metaprogramming evaluation using the optimiser

2018-02-27 Thread Joachim Breitner
Hi,

something like this would be great. I don’t have a sense yet of what
“something” should be like.


Am Dienstag, den 27.02.2018, 09:59 + schrieb Matthew Pickering:
> To go back to the power example, the recursive
> condition would have to be an inductively defined natural (data N = Z
> | S N) rather than an Int as the comparison operator for integers
> can't be evaluated by the optimiser.

Sure they can:

$ cat ConstantFolding.hs
{-# LANGUAGE TemplateHaskell #-} 
{-# OPTIONS_GHC -fplugin=Test.Inspection.Plugin #-}
module ConstantFolding where

import Test.Inspection

ltInt :: Bool
ltInt = (3::Int) > 2

ltInteger :: Bool
ltInteger = (3::Integer) > 2

true :: Bool
true = True


inspect $ 'ltInt === 'true
inspect $ 'ltInteger === 'true

$ ghc -O ConstantFolding.hs 
[1 of 1] Compiling ConstantFolding  ( ConstantFolding.hs,
ConstantFolding.o )
ConstantFolding.hs:17:1: ltInt === true passed.
ConstantFolding.hs:18:1: ltInteger === true passed.
inspection testing successful
  expected successes: 2



As  an alternative with a maybe simpler user interface (and probably
less power), I wonder if we can create a magic function
> compileTimeWHNF :: a -> a
or
> compileTimeNF :: a -> a
and a GHC core plugin (or eventually built-in thing) that finds these
magic functions and evaluates their arguments, using the simplifier.


Cheers,
Joachim

-- 
Joachim Breitner
  m...@joachim-breitner.de
  http://www.joachim-breitner.de/


signature.asc
Description: This is a digitally signed message part
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


An idea for a different style of metaprogramming evaluation using the optimiser

2018-02-27 Thread Matthew Pickering
I've had an idea for a while of a different way we could evaluate
TH-like splices which
would be more lightweight and easier to work with.

The idea is to create a third quotation/splicing mechanism which has
no introspection (like MetaML) but then to evaluate these quotes and
splices in the optimiser rather than using the bytecode interpreter.

I am motivated by the many examples of recursive functions in
libraries, which when given a statically known argument should be able
to be unrolled to produce much better code. It is understandable that
the compiler doesn't try to do this itself but there should be an easy
way for the user to direct the compiler to do so. (See also
https://www.reddit.com/r/haskell/comments/7yvb43/ghc_compiletime_evaluation/)

An example to be concrete:

Take the power function such that power k n computes k^n.

power :: Int -> Int -> Int
power k n = if n == 0
then 1
else k * power k (n - 1)

If we statically know n then we can create a staged version. We use R
to indicate that an
argument is dynamically known.

power :: R Int -> Int -> R Int
power k n = if n == 0
then .< 1 >.
else .< ~k * ~(power k (n-1)) >.

One way to implement this in Haskell is to use typed template haskell
quoting and splicing.
The key thing to notice about why this works is that in order to
splice `power k (n-1)` we need to
evaluate `power k (n-1)` so that we have something of type `R Int`
which we can then splice back into the quote.

The way this is currently implemented is that the bytecode interpreter
runs these splices in order to find out what they evaluate to.

The idea is that instead, we add another mode which runs splices in
the core-to-core optimiser. The optimiser performs evaluation by beta
reduction, inlining and constant folding. For simple definitions on
algebraic data types it does a very good job of eliminating overhead.
As long as the call is not recursive. If we can just get the optimiser
to inline recursive calls in a controlled manner as well, it should do
a good job on the unrolled definition.

The benefits of this are that it works across all platforms and fits
nicely already into the compilation pipeline. It also fits in nicely
with the intuition that a "quote" means to stop evaluating and a
"splice" means to evaluate.

A disadvantage is that the optimiser is only a *partial* evaluator
rather than an evaluator. It gets stuck evaluating things containing
primitives and so on. I don't forsee this as a major issue but a
limitation that library authors should be aware of when writing their
staged programs. To go back to the power example, the recursive
condition would have to be an inductively defined natural (data N = Z
| S N) rather than an Int as the comparison operator for integers
can't be evaluated by the optimiser. It is already rather easy to
write staged programs which loop if you don't carefully consider the
staging so this seems now worse than the status quo.

Does this sound at all sensible to anyone else?

Matt
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs