<div dir="ltr">Precisely.. If all goes well, one will be able to say:<div><br></div><div><table class="" style="border-collapse:collapse;border-spacing:0px;color:rgb(51,51,51);font-family:Helvetica,arial,nimbussansl,liberationsans,freesans,clean,sans-serif,'Apple Color Emoji','Segoe UI Emoji','Segoe UI Symbol';font-size:13px;line-height:18.2px"><tbody><tr><td id="LC1" class="" style="padding:0px 10px;vertical-align:top;font-family:Consolas,'Liberation Mono',Menlo,Courier,monospace;font-size:12px;white-space:pre;overflow:visible;word-wrap:normal"></td></tr><tr><td id="L5" class="" style="padding:0px 10px;width:50px;min-width:50px;white-space:nowrap;font-family:Consolas,'Liberation Mono',Menlo,Courier,monospace;font-size:12px;line-height:18px;color:rgba(0,0,0,0.298039);vertical-align:top;text-align:right;border-style:solid;border-color:rgb(238,238,238);border-width:0px 1px 0px 0px"></td><td id="LC5" class="" style="padding:0px 10px;vertical-align:top;font-family:Consolas,'Liberation Mono',Menlo,Courier,monospace;font-size:12px;white-space:pre;overflow:visible;word-wrap:normal"><span class="" style="color:rgb(167,29,93)">import</span> <span class="" style="color:rgb(0,134,179)">Data.SBV.Plugin</span></td></tr><tr><td id="L6" class="" style="padding:0px 10px;width:50px;min-width:50px;white-space:nowrap;font-family:Consolas,'Liberation Mono',Menlo,Courier,monospace;font-size:12px;line-height:18px;color:rgba(0,0,0,0.298039);vertical-align:top;text-align:right;border-style:solid;border-color:rgb(238,238,238);border-width:0px 1px 0px 0px"></td><td id="LC6" class="" style="padding:0px 10px;vertical-align:top;font-family:Consolas,'Liberation Mono',Menlo,Courier,monospace;font-size:12px;white-space:pre;overflow:visible;word-wrap:normal">
</td></tr><tr><td id="L7" class="" style="padding:0px 10px;width:50px;min-width:50px;white-space:nowrap;font-family:Consolas,'Liberation Mono',Menlo,Courier,monospace;font-size:12px;line-height:18px;color:rgba(0,0,0,0.298039);vertical-align:top;text-align:right;border-style:solid;border-color:rgb(238,238,238);border-width:0px 1px 0px 0px"></td><td id="LC7" class="" style="padding:0px 10px;vertical-align:top;font-family:Consolas,'Liberation Mono',Menlo,Courier,monospace;font-size:12px;white-space:pre;overflow:visible;word-wrap:normal">{-# ANN f theorem #-}</td></tr><tr><td id="L8" class="" style="padding:0px 10px;width:50px;min-width:50px;white-space:nowrap;font-family:Consolas,'Liberation Mono',Menlo,Courier,monospace;font-size:12px;line-height:18px;color:rgba(0,0,0,0.298039);vertical-align:top;text-align:right;border-style:solid;border-color:rgb(238,238,238);border-width:0px 1px 0px 0px"></td><td id="LC8" class="" style="padding:0px 10px;vertical-align:top;font-family:Consolas,'Liberation Mono',Menlo,Courier,monospace;font-size:12px;white-space:pre;overflow:visible;word-wrap:normal"><span class="" style="color:rgb(121,93,163)">f</span> :: <span class="" style="color:rgb(0,134,179)">Double</span> <span class="" style="color:rgb(167,29,93)">-></span> <span class="" style="color:rgb(0,134,179)">Double</span> <span class="" style="color:rgb(167,29,93)">-></span> <span class="" style="color:rgb(0,134,179)">Double</span> <span class="" style="color:rgb(167,29,93)">-></span> <span class="" style="color:rgb(0,134,179)">Bool</span></td></tr><tr><td id="L9" class="" style="padding:0px 10px;width:50px;min-width:50px;white-space:nowrap;font-family:Consolas,'Liberation Mono',Menlo,Courier,monospace;font-size:12px;line-height:18px;color:rgba(0,0,0,0.298039);vertical-align:top;text-align:right;border-style:solid;border-color:rgb(238,238,238);border-width:0px 1px 0px 0px"></td><td id="LC9" class="" style="padding:0px 10px;vertical-align:top;font-family:Consolas,'Liberation Mono',Menlo,Courier,monospace;font-size:12px;white-space:pre;overflow:visible;word-wrap:normal">f x y z <span class="" style="color:rgb(167,29,93)">=</span> x <span class="" style="color:rgb(167,29,93)">+</span> (y <span class="" style="color:rgb(167,29,93)">+</span> z) <span class="" style="color:rgb(167,29,93)">==</span> (x <span class="" style="color:rgb(167,29,93)">+</span> y) <span class="" style="color:rgb(167,29,93)">+</span> z</td></tr></tbody></table><br></div><div>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.)</div><div><br></div><div>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: <a href="http://github.com/LeventErkok/sbvPlugin/">http://github.com/LeventErkok/sbvPlugin/</a></div><div><br></div><div>-Levent.</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Dec 11, 2015 at 4:01 PM, Eric Seidel <span dir="ltr"><<a href="mailto:eric@seidel.io" target="_blank">eric@seidel.io</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Fri, Dec 11, 2015, at 15:28, Levent Erkok wrote:<br>
> My "hidden agenda" is to liberate the SBV library to work on Haskell<br>
> programs directly. (<a href="http://hackage.haskell.org/package/sbv" rel="noreferrer" target="_blank">http://hackage.haskell.org/package/sbv</a>)<br>
><br>
<br>
</span>So the idea is to translate a Haskell expression to an SBV symbolic<br>
expression, which you can then ship off to a solver? That's a perfectly<br>
good reason to use Core instead of TH :) Though it's not clear to me why<br>
you need to generate Core if your main concern is proving things (I<br>
guess the question is whether you want the proving to happen at<br>
compile-time or run-time).<br>
<span class=""><br>
> I tried TH/HSE before to see if I can let users write regular-Haskell and<br>
> have the expressions automatically made "symbolic" aware, but ran into a<br>
> lot of accidental complexity due to the extremely rich surface syntax.<br>
> I'm<br>
> currently working on a plugin to do the same, which is much nicer to work<br>
> with; though you are correct that dealing with explicitly-typed core has<br>
> its complexities as well. However, I do find it to be much easier to work<br>
> with as compared to surface Haskell.<br>
<br>
</span>The best advice I've received wrt generating Core is to generate as<br>
little as possible, and to make the generated Core as monomorphic as<br>
possible (thanks to Iavor for the advice!). This is actually not that<br>
hard to do; the trick is to write a library of helper functions that do<br>
everything you need, compile that library normally with GHC, and then<br>
generate Core that just calls the library functions. You probably<br>
already have all the library functions you need in SBV!<br>
<span class=""><br>
> I suspect you guys went down to the "stand-alone" route with<br>
> LiquidHaskell<br>
> when you had similar problems. That definitely is a great approach as<br>
> well,<br>
> though I don't have the luxury of an academic research team to pursue<br>
> that<br>
> line of thought. (LiquidHaskell rocks by the way; I'm a real fan.)<br>
<br>
</span>LiquidHaskell uses GHC as a front-end, we extract the Core from GHC and<br>
perform our type-checking on the Core. In theory we could be a Core<br>
plugin, but there are some engineering issues that we haven't worked out<br>
yet. Luckily we just *analyze* the Core, we don't try to produce any<br>
Core of our own, so the explicit typing hardly affects us at all.<br>
<br>
(I'm a big fan of SBV too)<br>
<span class="HOEnZb"><font color="#888888"><br>
Eric<br>
</font></span></blockquote></div><br></div>