A comment on Introspective-Haskell

[Levent Erkok]

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 <eric at seidel.io> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20151211/1566f2a7/attachment-0001.html>