An idea for a different style of metaprogramming evaluation using the optimiser
Simon Peyton Jones
simonpj at microsoft.com
Fri May 25 16:51:57 UTC 2018
(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 <matthewtpickering at gmail.com>
| Sent: 27 February 2018 11:18
| To: Simon Peyton Jones <simonpj at microsoft.com>
| 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.
|
| ```
| $$$(power (S Z) [|| x ||])
| =>
| E: power (S Z) [|| x ||]
| =>
| E: case (S Z) of
| Z -> [||| 1 |||]
| (S n) -> [||| $$$([||| x |||]) * $$$(power n [||| x |||]) |||]
| => (Case of known constructor)
| E: [||| $$$([|| x ||]) * $$$(power Z [||| x |||) |||]
| => Quote
| $$$([||| x |||]) * $$$(power Z [||| x |||])
| =>
| k * $$$(power Z [||| x |||])
| => Splice
| k * E: power Z [||| x |||]
| => Inline power as we in E
| k * E (case Z of Z -> [||| 1 |||]; S n ... ->)
| => Case of known constructor
| k * E: [||| 1 |||]
| =>
| k * 1
| ```
|
|
| Hope that clears some things up.
|
|
| Matt
|
| On Tue, Feb 27, 2018 at 10:37 AM, Simon Peyton Jones
| <simonpj at microsoft.com> wrote:
| > Matthew, I'm afraid I don't understand the proposal at all. Can you
| give a few examples?
| >
| > S
| >
| > | -----Original Message-----
| > | From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of
| > | Matthew Pickering
| > | Sent: 27 February 2018 09:59
| > | To: GHC developers <ghc-devs at haskell.org>
| > | Subject: An idea for a different style of metaprogramming
| evaluation
| > | using the optimiser
| > |
| > | 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://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.r
| > |
| eddit.com%2Fr%2Fhaskell%2Fcomments%2F7yvb43%2Fghc_compiletime_evaluati
| > |
| on%2F&data=04%7C01%7Csimonpj%40microsoft.com%7C9979850e7fb142a7e11c08d
| > |
| 57dc8dcb8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636553224038023
| > |
| 725%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTi
| > | I6Ik1haWwifQ%3D%3D%7C-
| > |
| 1&sdata=%2FOQOcFIXduGY9wtWWEkbqd3qQ1715oCdaim0pCeSgrI%3D&reserved=0)
| > |
| > | 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 at haskell.org
| > |
| https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.h
| > | askell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-
| > |
| devs&data=04%7C01%7Csimonpj%40microsoft.com%7C9979850e7fb142a7e11c08d5
| > |
| 7dc8dcb8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C6365532240380237
| > |
| 25%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI
| > | 6Ik1haWwifQ%3D%3D%7C-
| > |
| 1&sdata=CJgS3uH4hHw5Zups1fAiUtOnTzn%2ByCh1bg1auiMBcYM%3D&reserved=0
More information about the ghc-devs
mailing list