<div dir="ltr"><div>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). <br><br></div>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...<br></div><div class="gmail_extra"><br><div class="gmail_quote">2015-01-28 9:28 GMT+01:00 Alberto G. Corona <span dir="ltr"><<a href="mailto:agocorona@gmail.com" target="_blank">agocorona@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div>There is a interpreter of Haskell written in Maude:<br><br><a href="http://fsl.cs.illinois.edu/images/5/5f/Bennett-2006-tr.pdf" target="_blank">http://fsl.cs.illinois.edu/images/5/5f/Bennett-2006-tr.pdf</a><br><br></div>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<br><br></div><br></div><div class="gmail_extra"><div><div class="h5"><br><div class="gmail_quote">2015-01-27 11:35 GMT+01:00 Paul Brauner <span dir="ltr"><<a href="mailto:polux2001@gmail.com" target="_blank">polux2001@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Stepeval is what Christopher pointed to in his first email, but he said it only works on a teeny weeny subset of Haskell. <br></div><div><div><br><div class="gmail_quote">On Tue Jan 27 2015 at 8:26:55 AM Sumit Sahrawat, Maths & Computing, IIT (BHU) <<a href="mailto:sumit.sahrawat.apm13@iitbhu.ac.in" target="_blank">sumit.sahrawat.apm13@iitbhu.ac.in</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">I found <a href="https://github.com/bmillwood/stepeval" target="_blank">https://github.com/bmillwood/stepeval</a>, which evaluates expressions step-by-step. It might be possible to modify it for equational reasoning.</div><div class="gmail_extra"></div><div class="gmail_extra"><br><div class="gmail_quote">On 27 January 2015 at 04:17, Albert Y. C. Lai <span dir="ltr"><<a href="mailto:trebla@vex.net" target="_blank">trebla@vex.net</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span>On 2015-01-18 06:46 PM, Christopher Done wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
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.<br>
<br>
Is there any tooling anywhere out there that can take in a Haskell expression and reduce it by one step?<br>
</blockquote>
<br></span>
I suggest my friend Lev Naiman's proof assistant project "Netty"<br>
<a href="https://bitbucket.org/naiman/nettyproject/overview" target="_blank">https://bitbucket.org/naiman/<u></u>nettyproject/overview</a><br>
It is not specific to Haskell. It is a general-purpose calculational proof assistant.<br>
<br>
If you want to take a look at a paper, it's somewhere on his home page:<br>
<a href="http://www.cs.utoronto.ca/~naiman/" target="_blank">http://www.cs.utoronto.ca/~<u></u>naiman/</a> <<a href="http://www.cs.utoronto.ca/%7Enaiman/" target="_blank">http://www.cs.utoronto.ca/%<u></u>7Enaiman/</a>><div><div><br>
<br>
______________________________<u></u>_________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/<u></u>mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br><br clear="all"><div><br></div></div><div class="gmail_extra">-- <br><div><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div>Regards</div><div dir="ltr"><div><br></div><div>Sumit Sahrawat</div></div></div></div></div></div></div>
</div>
______________________________<u></u>_________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/<u></u>mailman/listinfo/haskell-cafe</a><br>
</blockquote></div>
</div></div><br>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
<br></blockquote></div><br><br clear="all"><br>-- <br></div></div><span class="HOEnZb"><font color="#888888"><div>Alberto.</div>
</font></span></div>
</blockquote></div><br><br clear="all"><br>-- <br><div class="gmail_signature">Alberto.</div>
</div>