Thomas: I honestly don't see why TH needs to go away. The way I viewed Richard's proposal was a means for me to get my hands on Core-splices inside my regular Haskell code. I think the two can co-exist happily. Perhaps others can opine on why we can't have both, aside from perhaps an argument about added complexity of having two different kinds of splices. If there was an effort to allow Core-splices, I'd be happy to contribute so much as I can. Whether that ends up replacing TH or a compatibility shim is actually needed is a different question in my mind. That can be decided based on the experience with having Core-splices working first? Please correct me if I'm wrong; in that TH and Core-splices cannot coexist, at least in theory, for some other reason. -Levent. On Wed, Dec 9, 2015 at 7:55 AM, Thomas Bereknyei wrote:

This should be possible to start as a custom library. Appropriately shimming the result back into TH. Then with some experience and lessons learned we can investigate replacing TH with this new approach.

I ran across many similar issues with TH, haskell-src-exts, haskell-src-meta, etc.

Levent: Would it be appropriate for us to start putting together this shim? As Simon says in ( https://ghc.haskell.org/trac/ghc/ticket/11081#comment:5) we can go a long ways with a plethora of pattern synonyms.

On Tue, Dec 8, 2015 at 9:51 PM, Levent Erkok wrote:

...

I just came across https://ghc.haskell.org/trac/ghc/ticket/11081, and the corresponding wiki-page: https://ghc.haskell.org/trac/ghc/wiki/TemplateHaskell/Introspective

I think this is a terrific idea. In the past, I've tried both TH and haskell-src-exts to do relatively simple things, but ended-up abandoning them due to the inherent complexity of source level haskell that had very little to do with what I really cared about. Being able to get your hands on Core at the regular Haskell level would truly simplify life, and I suspect would open the flood-gates for a lot of people to develop extremely cool/useful artifacts, making the GHC/Haskell experience even better.

I hope this idea is taken further and sees the light-of-day.

Richard: Did you have any further thoughts about possible plans?

-Levent.

_______________________________________________ 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

Spot on.. I really want "Template Core," independent of TH. To be honest, "GHC Plugins" already provides "Template Core" in this sense; but would be nicer if one can get his hands on the Core in the regular Haskell context, not just in a plugin context. So, perhaps "Template Core" is not the biggest priority in the big scheme of things. On Fri, Dec 11, 2015 at 2:23 PM, Richard Eisenberg wrote:

I'm seeing several different directions here, and it may be helpful to clarify what's going on:

* My original proposal was about changing the implementation of Template Haskell in a way that casual TH users wouldn't notice (by going through the compatibility shim). Once this is done, it may be possible to extend the idea to Core, but that wasn't my primary motivation.

* It seems that Levant wants Template Core. This idea is actually orthogonal from my original proposal, in that Template Core can be implemented with introspection or not. I think it will be easier with introspection, but it's just a matter of engineering either way.

* I don't think any real movement can be made on either of these issues without editing GHC itself. I don't see what a purely-external library could do.

* Yes yes yes, lots lots lots of pattern synonyms.

Does this clarify anything?

Richard

On Dec 9, 2015, at 12:28 PM, Levent Erkok wrote:

Thomas: I honestly don't see why TH needs to go away. The way I viewed Richard's proposal was a means for me to get my hands on Core-splices inside my regular Haskell code. I think the two can co-exist happily. Perhaps others can opine on why we can't have both, aside from perhaps an argument about added complexity of having two different kinds of splices.

If there was an effort to allow Core-splices, I'd be happy to contribute so much as I can. Whether that ends up replacing TH or a compatibility shim is actually needed is a different question in my mind. That can be decided based on the experience with having Core-splices working first?

Please correct me if I'm wrong; in that TH and Core-splices cannot coexist, at least in theory, for some other reason.

-Levent.

On Wed, Dec 9, 2015 at 7:55 AM, Thomas Bereknyei wrote:

...

This should be possible to start as a custom library. Appropriately shimming the result back into TH. Then with some experience and lessons learned we can investigate replacing TH with this new approach.

I ran across many similar issues with TH, haskell-src-exts, haskell-src-meta, etc.

Levent: Would it be appropriate for us to start putting together this shim? As Simon says in ( https://ghc.haskell.org/trac/ghc/ticket/11081#comment:5) we can go a long ways with a plethora of pattern synonyms.

On Tue, Dec 8, 2015 at 9:51 PM, Levent Erkok wrote:

...

I just came across https://ghc.haskell.org/trac/ghc/ticket/11081, and the corresponding wiki-page: https://ghc.haskell.org/trac/ghc/wiki/TemplateHaskell/Introspective

I think this is a terrific idea. In the past, I've tried both TH and haskell-src-exts to do relatively simple things, but ended-up abandoning them due to the inherent complexity of source level haskell that had very little to do with what I really cared about. Being able to get your hands on Core at the regular Haskell level would truly simplify life, and I suspect would open the flood-gates for a lot of people to develop extremely cool/useful artifacts, making the GHC/Haskell experience even better.

I hope this idea is taken further and sees the light-of-day.

Richard: Did you have any further thoughts about possible plans?

-Levent.

_______________________________________________ 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

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

My "hidden agenda" is to liberate the SBV library to work on Haskell programs directly. (http://hackage.haskell.org/package/sbv) SBV allows programming with symbolic values, allowing a certain class of "proofs" to be done. It uses SMT solvers to do the actual "solving." It's limited in what it can do so far as reasoning goes: It's mostly limited to number types really (Word/Int/Float/Double etc.), but when it works, it really can be effective. Right now, users of this library have to write things like this: foo x y = ite (x .> y) (x+2) (x .< y) Since I "cannot" reliably steal if-then-else (yes, I'm aware of RebindableSyntax; but it has its own problems.), nor I can just use comparison operators that insist on returning Bool that I cannot change. But those are smaller problems: The bigger issue is that I cannot support "case" expressions, pattern-matching, and all that stuff; since all that mechanism is baked into the compiler and I've no way to arrange for a pattern to "symbolically" match. This latter issue with pattern-matching and lack of support for case-expressions is why the library is sort of "hard-to-use" for a newcomer. I tried TH/HSE before to see if I can let users write regular-Haskell and have the expressions automatically made "symbolic" aware, but ran into a lot of accidental complexity due to the extremely rich surface syntax. I'm currently working on a plugin to do the same, which is much nicer to work with; though you are correct that dealing with explicitly-typed core has its complexities as well. However, I do find it to be much easier to work with as compared to surface Haskell. I suspect you guys went down to the "stand-alone" route with LiquidHaskell when you had similar problems. That definitely is a great approach as well, though I don't have the luxury of an academic research team to pursue that line of thought. (LiquidHaskell rocks by the way; I'm a real fan.) -Levent. On Fri, Dec 11, 2015 at 3:13 PM, Eric Seidel wrote:

On Fri, Dec 11, 2015, at 14:54, Levent Erkok wrote:

...

Spot on.. I really want "Template Core," independent of TH.

To be honest, "GHC Plugins" already provides "Template Core" in this sense; but would be nicer if one can get his hands on the Core in the regular Haskell context, not just in a plugin context. So, perhaps "Template Core" is not the biggest priority in the big scheme of things.

I would caution against going the Core Plugin (or Template Core) route unless you really need to work with Core, e.g. if you're doing some sort of analysis and want to save your sanity by avoiding all of the surface syntax.

Constructing and manipulating Core is quite tedious because Core is explicitly typed. This means that you have to instantiate type parameters of polymorphic functions/constructors yourself, and worse, you have to provide type-class dictionaries yourself. It's not impossible by any means, just a lot more work in my experience than working with surface syntax and letting GHC handle the rest :)

I'm curious though, what specifically were you trying to use TH/HSE for in the past, analysis or code-generation? _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Precisely.. If all goes well, one will be able to say: import Data.SBV.Plugin {-# ANN f theorem #-}f :: Double -> Double -> Double -> Boolf x y z = x + (y + z) == (x + y) + z And have that theorem proven at "compile" time. (Of course, the above is actually not true, so the user will get a counter-example and compilation will abort.) I've got this *mostly* working from a plugin, but it needs a ton more polishing before it can be released to the wild. Here's the repo, though it's in a constant state of flux for the time being and is in nowhere near sufficient quality for a more public announcement: http://github.com/LeventErkok/sbvPlugin/ -Levent. On Fri, Dec 11, 2015 at 4:01 PM, Eric Seidel wrote:

On Fri, Dec 11, 2015, at 15:28, Levent Erkok wrote:

...

My "hidden agenda" is to liberate the SBV library to work on Haskell programs directly. (http://hackage.haskell.org/package/sbv)

So the idea is to translate a Haskell expression to an SBV symbolic expression, which you can then ship off to a solver? That's a perfectly good reason to use Core instead of TH :) Though it's not clear to me why you need to generate Core if your main concern is proving things (I guess the question is whether you want the proving to happen at compile-time or run-time).

...

I tried TH/HSE before to see if I can let users write regular-Haskell and have the expressions automatically made "symbolic" aware, but ran into a lot of accidental complexity due to the extremely rich surface syntax. I'm currently working on a plugin to do the same, which is much nicer to work with; though you are correct that dealing with explicitly-typed core has its complexities as well. However, I do find it to be much easier to work with as compared to surface Haskell.

The best advice I've received wrt generating Core is to generate as little as possible, and to make the generated Core as monomorphic as possible (thanks to Iavor for the advice!). This is actually not that hard to do; the trick is to write a library of helper functions that do everything you need, compile that library normally with GHC, and then generate Core that just calls the library functions. You probably already have all the library functions you need in SBV!

...

I suspect you guys went down to the "stand-alone" route with LiquidHaskell when you had similar problems. That definitely is a great approach as well, though I don't have the luxury of an academic research team to pursue that line of thought. (LiquidHaskell rocks by the way; I'm a real fan.)

LiquidHaskell uses GHC as a front-end, we extract the Core from GHC and perform our type-checking on the Core. In theory we could be a Core plugin, but there are some engineering issues that we haven't worked out yet. Luckily we just *analyze* the Core, we don't try to produce any Core of our own, so the explicit typing hardly affects us at all.

(I'm a big fan of SBV too)

Eric