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
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