[Haskell-cafe] Tooling for equational reasoning in Haskell

[Mathieu Boespflug]

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 at 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 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
>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>