[Haskell-cafe] Tooling for equational reasoning in Haskell

[Alberto G. Corona]

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 <agocorona at gmail.com>:

> 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 <polux2001 at gmail.com>:
>
>> 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) <sumit.sahrawat.apm13 at iitbhu.ac.in> 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 <trebla at vex.net> 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 at haskell.org
>>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>>
>>>
>>>
>>>
>>> --
>>> Regards
>>>
>>> Sumit Sahrawat
>>>  _______________________________________________
>>> Haskell-Cafe mailing list
>>> Haskell-Cafe at haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
>
>
> --
> Alberto.
>



-- 
Alberto.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20150128/70a5e384/attachment.html>