[Haskell-cafe] Tooling for equational reasoning in Haskell

[Paul Brauner]

There was this paper a while ago, not sure where the software can be
downloaded: http://ittc.ku.edu/~andygill/papers/IntroHERA06.pdf

On Mon Jan 19 2015 at 8:43:49 AM Mathieu Boespflug <mboes at tweag.net> wrote:

> Could Hermit be of any relief?
>
> http://ku-fpg.github.io/software/hermit/
>
> It doesn't work on the surface syntax, only on the core syntax AFAIK,
> but some would call that a feature (simpler traversals). So long as
> you're happy doing this reasoning at the level of Core, this should be
> workable. I'm not sure that it would be easy to map the result back to
> surface syntax, but maybe Andy can comment.
>
> Best,
>
> Mathieu
>
> On 19 January 2015 at 00:46, Christopher Done <chrisdone at gmail.com> wrote:
> > Hi
> >
> > I quite enjoy doing equational reasoning to prove that my functions
> satisfy
> > some laws, I like to type out each substitution step until I get back
> what I
> > started with. The only trouble is that it's rather manual and possibly
> error
> > prone.
> >
> > Is there any tooling anywhere out there that can take in a Haskell
> > expression and reduce it by one step? I only know of stepeval:
> >
> > http://bm380.user.srcf.net/cgi-bin/stepeval.cgi?expr=
> foldr+%28%2B%29+0+%5B1%2C2%2C3%5D+%3D%3D+6
> >
> > But it's just a prototype and works on a teeny weeny subset of Haskell.
> As
> > much as I like doing tooling, my bandwidth for this area is already full.
> >
> > It seems quite hard to implement such a tool with existing tooling. Real
> > compilers and interpreters tend to be distinctly far away from a simple
> > substitution model or retaining the original source code and being able
> to
> > print valid source back out.
> >
> > If such a tool existed, though, it'd be super handy and you could
> probably
> > include it as another check for your build process like your type
> checking,
> > your quickcheck properties and your unit tests. I would personally
> invest a
> > little bit of time to add interactive Emacs support for such a tool.
> >
> > Ciao
> >
> > _______________________________________________
> > Haskell-Cafe mailing list
> > Haskell-Cafe at haskell.org
> > http://www.haskell.org/mailman/listinfo/haskell-cafe
> >
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20150119/e9b7fc7f/attachment.html>