(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@gmail.com> | Sent: 27 February 2018 11:18 | To: Simon Peyton Jones <simonpj@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@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@haskell.org] On Behalf Of | > | Matthew Pickering | > | Sent: 27 February 2018 09:59 | > | To: GHC developers <ghc-devs@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@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