[Haskell-cafe] Re: Graph reduction [Was: Where is StackOverflow on the Wiki?]

[Neil Mitchell]

Hi

> > Yeah, the precise details may vary, even :) But for teaching, an
> > automatic tool that does graph reduction would be great. I don't mind
> > if it's sloppy (directly apply definitions & pattern matching VS
> > everything is a lambda abstraction) and only does simply typed lambda
> > calculus (no type applications, no type classes).
>
> Well come ON people, there's *got* to be enough big-wigs on this list to
> put *something* together! ;-)

It's been done, but never got to a released state:

http://haskell.org/haskellwiki/Haskell_Equational_Reasoning_Assistant

http://www.cs.york.ac.uk/fp/darcs/proof/ (screenshot:
http://www-users.cs.york.ac.uk/~ndm/temp/proof.png)

And neither of them will be of much use to a beginner. Haskell is too
complex to reason about formally for a beginner, and reasoning
"informally" isn't very easy to do - because its not a precise
description of what to do.

Thanks

Neil