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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe