Re: [Haskell-cafe] Tooling for equational reasoning in Haskell

In the other side I´m after something somewhat related to that: A way to extract a machine-independent representation (for example, source code) of a piece of code at runtime in order to compile and run it in another computer (or a browser). This may sound crazy, but I think that enhancing the compiler with an option which maintain a pointer from each Haskell expression to his parsed source code and then using lazy rewriting to update the source code tree, it could be possible a great number of now unthinkable applications while running the code at compilation speeds: since very detailed debugging, teaching, mobile agents, code serialization, reflection... 2015-01-28 9:28 GMT+01:00 Alberto G. Corona :

There is a interpreter of Haskell written in Maude:

http://fsl.cs.illinois.edu/images/5/5f/Bennett-2006-tr.pdf

Which potentially can do it, since Maude is an specificiation language based on rewriting logic. It has no IO neither has syntactic sugar for lists, type classes etc, But it is a different path to achieving this goal if someone is interested in developing it further

2015-01-27 11:35 GMT+01:00 Paul Brauner :

...

Stepeval is what Christopher pointed to in his first email, but he said it only works on a teeny weeny subset of Haskell.

On Tue Jan 27 2015 at 8:26:55 AM Sumit Sahrawat, Maths & Computing, IIT (BHU) wrote:

...

I found https://github.com/bmillwood/stepeval, which evaluates expressions step-by-step. It might be possible to modify it for equational reasoning.

On 27 January 2015 at 04:17, Albert Y. C. Lai wrote:

...

On 2015-01-18 06:46 PM, Christopher Done wrote:

...

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 suggest my friend Lev Naiman's proof assistant project "Netty" https://bitbucket.org/naiman/nettyproject/overview It is not specific to Haskell. It is a general-purpose calculational proof assistant.

If you want to take a look at a paper, it's somewhere on his home page: http://www.cs.utoronto.ca/~naiman/ <http://www.cs.utoronto.ca/% 7Enaiman/>

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Regards

Sumit Sahrawat _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Alberto.

-- Alberto.