Tooling for equational reasoning in Haskell
Hi 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 only know of stepeval: http://bm380.user.srcf.net/cgi-bin/stepeval.cgi?expr=foldr+%28%2B%29+0+%5B1%... But it's just a prototype and works on a teeny weeny subset of Haskell. As much as I like doing tooling, my bandwidth for this area is already full. It seems quite hard to implement such a tool with existing tooling. Real compilers and interpreters tend to be distinctly far away from a simple substitution model or retaining the original source code and being able to print valid source back out. If such a tool existed, though, it'd be super handy and you could probably include it as another check for your build process like your type checking, your quickcheck properties and your unit tests. I would personally invest a little bit of time to add interactive Emacs support for such a tool. Ciao
Could Hermit be of any relief? http://ku-fpg.github.io/software/hermit/ It doesn't work on the surface syntax, only on the core syntax AFAIK, but some would call that a feature (simpler traversals). So long as you're happy doing this reasoning at the level of Core, this should be workable. I'm not sure that it would be easy to map the result back to surface syntax, but maybe Andy can comment. Best, Mathieu On 19 January 2015 at 00:46, Christopher Done <chrisdone@gmail.com> wrote:
Hi
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 only know of stepeval:
http://bm380.user.srcf.net/cgi-bin/stepeval.cgi?expr=foldr+%28%2B%29+0+%5B1%...
But it's just a prototype and works on a teeny weeny subset of Haskell. As much as I like doing tooling, my bandwidth for this area is already full.
It seems quite hard to implement such a tool with existing tooling. Real compilers and interpreters tend to be distinctly far away from a simple substitution model or retaining the original source code and being able to print valid source back out.
If such a tool existed, though, it'd be super handy and you could probably include it as another check for your build process like your type checking, your quickcheck properties and your unit tests. I would personally invest a little bit of time to add interactive Emacs support for such a tool.
Ciao
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
There was this paper a while ago, not sure where the software can be downloaded: http://ittc.ku.edu/~andygill/papers/IntroHERA06.pdf On Mon Jan 19 2015 at 8:43:49 AM Mathieu Boespflug <mboes@tweag.net> wrote:
Could Hermit be of any relief?
http://ku-fpg.github.io/software/hermit/
It doesn't work on the surface syntax, only on the core syntax AFAIK, but some would call that a feature (simpler traversals). So long as you're happy doing this reasoning at the level of Core, this should be workable. I'm not sure that it would be easy to map the result back to surface syntax, but maybe Andy can comment.
Best,
Mathieu
On 19 January 2015 at 00:46, Christopher Done <chrisdone@gmail.com> wrote:
Hi
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 only know of stepeval:
http://bm380.user.srcf.net/cgi-bin/stepeval.cgi?expr= foldr+%28%2B%29+0+%5B1%2C2%2C3%5D+%3D%3D+6
But it's just a prototype and works on a teeny weeny subset of Haskell. As much as I like doing tooling, my bandwidth for this area is already full.
It seems quite hard to implement such a tool with existing tooling. Real compilers and interpreters tend to be distinctly far away from a simple substitution model or retaining the original source code and being able to print valid source back out.
If such a tool existed, though, it'd be super handy and you could probably include it as another check for your build process like your type checking, your quickcheck properties and your unit tests. I would personally invest a little bit of time to add interactive Emacs support for such a tool.
Ciao
_______________________________________________ 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
Ah, interesting. That last paper demonstration seems promising. I like that it lets you state laws like the monad law. I see it's also Core driven. I'll try it out. I've got a type I want to prove is Applicative and Alternative. Andy, what's your assessment on the difficulty of working with plain Haskell? For example, what if you took your HOOD project and used HSE or TH to annotate a whole source tree from expressions to patterns (with view patterns)? One thing I pondered was, e.g. if you have this program: \x -> x 01234678 -- these are the columns you could transform it to: observe "(0,0)-(1,8)" (\(observe "(0,1)-(0,2)" -> x) -> observe "(0,7)-(0,8)" x) Which would allow you to map back to the original source. But now instead of storing just locations, you want rather than just to see what things are being forced, you want to produce a series of valid source programs. So maybe you store kind of diff instructions, like this: http://lpaste.net/114511 You get something like: orig_ex = (\x -> (\y -> x * y)) 5 7 translated_ex = seq (push (Reset "(\\x -> (\\y -> x * y)) 5 7") ((\x -> (push (Set 0 25 ("(\\y -> " ++ show x ++ " * y)")) (\y -> push (Set 0 13 (show x ++ " * " ++ show y)) (x * y)))) 5 7)) stack λ> readIORef translated_ex >>= mapM_ putStrLn . interpret (\x -> (\y -> x * y)) 5 7 (\y -> 5 * y) 5 * 7 I think the problem I encountered was that I'd need alpha conversion, which would need something like haskell-names to resolve names. A little more involved as a project to pursue. There's probably some fatal flaw that means it's a terrible idea. Presumably you've already considered things like this in your research. Ciao On 19 January 2015 at 10:18, Paul Brauner <polux2001@gmail.com> wrote:
There was this paper a while ago, not sure where the software can be downloaded: http://ittc.ku.edu/~andygill/papers/IntroHERA06.pdf
On Mon Jan 19 2015 at 8:43:49 AM Mathieu Boespflug <mboes@tweag.net> wrote:
Could Hermit be of any relief?
http://ku-fpg.github.io/software/hermit/
It doesn't work on the surface syntax, only on the core syntax AFAIK, but some would call that a feature (simpler traversals). So long as you're happy doing this reasoning at the level of Core, this should be workable. I'm not sure that it would be easy to map the result back to surface syntax, but maybe Andy can comment.
Best,
Mathieu
On 19 January 2015 at 00:46, Christopher Done <chrisdone@gmail.com> wrote:
Hi
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 only know of stepeval:
http://bm380.user.srcf.net/cgi-bin/stepeval.cgi?expr= foldr+%28%2B%29+0+%5B1%2C2%2C3%5D+%3D%3D+6
But it's just a prototype and works on a teeny weeny subset of Haskell. As much as I like doing tooling, my bandwidth for this area is already full.
It seems quite hard to implement such a tool with existing tooling. Real compilers and interpreters tend to be distinctly far away from a simple substitution model or retaining the original source code and being able to print valid source back out.
If such a tool existed, though, it'd be super handy and you could probably include it as another check for your build process like your type checking, your quickcheck properties and your unit tests. I would personally invest a little bit of time to add interactive Emacs support for such a tool.
Ciao
_______________________________________________ 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
As far as core to surface syntax is concerned, there is the precedent of the Chameleon compiler (which is now dead, unfortunately). It used to be here: http://www.comp.nus.edu.sg/~sulzmann/chameleon. The compiler would do type checking on the core language, not the surface language. As a result, the type checker was smaller. It would embed links in the core AST to the surface AST in order to map back to the surface AST when reporting errors, etc. On 19 January 2015 at 11:11, Christopher Done <chrisdone@gmail.com> wrote:
Ah, interesting. That last paper demonstration seems promising. I like that it lets you state laws like the monad law. I see it's also Core driven. I'll try it out. I've got a type I want to prove is Applicative and Alternative.
Andy, what's your assessment on the difficulty of working with plain Haskell?
For example, what if you took your HOOD project and used HSE or TH to annotate a whole source tree from expressions to patterns (with view patterns)? One thing I pondered was, e.g. if you have this program:
\x -> x 01234678 -- these are the columns
you could transform it to:
observe "(0,0)-(1,8)" (\(observe "(0,1)-(0,2)" -> x) -> observe "(0,7)-(0,8)" x)
Which would allow you to map back to the original source. But now instead of storing just locations, you want rather than just to see what things are being forced, you want to produce a series of valid source programs. So maybe you store kind of diff instructions, like this: http://lpaste.net/114511 You get something like:
orig_ex = (\x -> (\y -> x * y)) 5 7
translated_ex = seq (push (Reset "(\\x -> (\\y -> x * y)) 5 7") ((\x -> (push (Set 0 25 ("(\\y -> " ++ show x ++ " * y)")) (\y -> push (Set 0 13 (show x ++ " * " ++ show y)) (x * y)))) 5 7)) stack
λ> readIORef translated_ex >>= mapM_ putStrLn . interpret (\x -> (\y -> x * y)) 5 7 (\y -> 5 * y) 5 * 7
I think the problem I encountered was that I'd need alpha conversion, which would need something like haskell-names to resolve names. A little more involved as a project to pursue. There's probably some fatal flaw that means it's a terrible idea.
Presumably you've already considered things like this in your research.
Ciao
On 19 January 2015 at 10:18, Paul Brauner <polux2001@gmail.com> wrote:
There was this paper a while ago, not sure where the software can be downloaded: http://ittc.ku.edu/~andygill/papers/IntroHERA06.pdf
On Mon Jan 19 2015 at 8:43:49 AM Mathieu Boespflug <mboes@tweag.net> wrote:
Could Hermit be of any relief?
http://ku-fpg.github.io/software/hermit/
It doesn't work on the surface syntax, only on the core syntax AFAIK, but some would call that a feature (simpler traversals). So long as you're happy doing this reasoning at the level of Core, this should be workable. I'm not sure that it would be easy to map the result back to surface syntax, but maybe Andy can comment.
Best,
Mathieu
On 19 January 2015 at 00:46, Christopher Done <chrisdone@gmail.com> wrote:
Hi
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 only know of stepeval:
http://bm380.user.srcf.net/cgi-bin/stepeval.cgi?expr=foldr+%28%2B%29+0+%5B1%...
But it's just a prototype and works on a teeny weeny subset of Haskell. As much as I like doing tooling, my bandwidth for this area is already full.
It seems quite hard to implement such a tool with existing tooling. Real compilers and interpreters tend to be distinctly far away from a simple substitution model or retaining the original source code and being able to print valid source back out.
If such a tool existed, though, it'd be super handy and you could probably include it as another check for your build process like your type checking, your quickcheck properties and your unit tests. I would personally invest a little bit of time to add interactive Emacs support for such a tool.
Ciao
_______________________________________________ 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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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/>
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@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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- Regards Sumit Sahrawat
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@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@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@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
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@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@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@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@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.
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@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@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@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@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@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.
participants (6)
-
Albert Y. C. Lai -
Alberto G. Corona -
Christopher Done -
Mathieu Boespflug -
Paul Brauner -
Sumit Sahrawat, Maths & Computing, IIT (BHU)