A comment on Introspective-Haskell

[Eric Seidel]

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