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

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 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 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 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 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