A comment on Introspective-Haskell

[Levent Erkok]

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 <eric at 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20151211/5d3b4e90/attachment.html>