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 <e...@seidel.io> 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 >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
