[Haskell-cafe] Tooling for equational reasoning in Haskell

[Christopher Done]

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 at 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 at 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 at 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 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
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20150119/85e077c6/attachment.html>