[Haskell-cafe] Tooling for equational reasoning in Haskell

[Mathieu Boespflug]

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
>