[Haskell-cafe] Tooling for equational reasoning in Haskell

[Christopher Done]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20150119/2015d278/attachment.html>