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