<div dir="ltr">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.<div><br></div><div>Andy, what's your assessment on the difficulty of working with plain Haskell?</div><div><br></div><div>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:</div><div><br></div><div><font face="monospace, monospace">\x -> x</font></div><div><font face="monospace, monospace">01234678 -- these are the columns</font></div><div><br></div><div>you could transform it to:</div><div><br></div><div><font face="monospace, monospace">observe "(0,0)-(1,8)"</font></div><div><font face="monospace, monospace"> (\(observe "(0,1)-(0,2)" -> x) -></font></div><div><font face="monospace, monospace"> observe "(0,7)-(0,8)" x)</font></div><div><br></div><div>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: <a href="http://lpaste.net/114511">http://lpaste.net/114511</a> You get something like:</div><div><br></div><div><font face="monospace, monospace">orig_ex = (\x -> (\y -> x * y)) 5 7</font><br></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace"><div>translated_ex =</div><div> seq (push (Reset "(\\x -> (\\y -> x * y)) 5 7")</div><div> ((\x -></div><div> (push (Set 0 25 ("(\\y -> " ++ show x ++ " * y)"))</div><div> (\y -></div><div> push (Set 0 13 (show x ++ " * " ++ show y))</div><div> (x * y)))) 5 7))</div><div> stack</div></font></div><div><br></div><div><div><font face="monospace, monospace">λ> readIORef translated_ex >>= mapM_ putStrLn . interpret</font></div><div><font face="monospace, monospace">(\x -> (\y -> x * y)) 5 7</font></div><div><font face="monospace, monospace">(\y -> 5 * y)</font></div><div><font face="monospace, monospace">5 * 7</font></div></div><div><br></div><div>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.</div><div><br></div><div>Presumably you've already considered things like this in your research.</div><div><br></div><div>Ciao</div></div><div class="gmail_extra"><br><div class="gmail_quote">On 19 January 2015 at 10:18, Paul Brauner <span dir="ltr"><<a href="mailto:polux2001@gmail.com" target="_blank">polux2001@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">There was this paper a while ago, not sure where the software can be downloaded: <a href="http://ittc.ku.edu/~andygill/papers/IntroHERA06.pdf" target="_blank">http://ittc.ku.edu/~andygill/papers/IntroHERA06.pdf</a><div class="HOEnZb"><div class="h5"><br><br><div class="gmail_quote">On Mon Jan 19 2015 at 8:43:49 AM Mathieu Boespflug <<a href="mailto:mboes@tweag.net" target="_blank">mboes@tweag.net</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Could Hermit be of any relief?<br>
<br>
<a href="http://ku-fpg.github.io/software/hermit/" target="_blank">http://ku-fpg.github.io/<u></u>software/hermit/</a><br>
<br>
It doesn't work on the surface syntax, only on the core syntax AFAIK,<br>
but some would call that a feature (simpler traversals). So long as<br>
you're happy doing this reasoning at the level of Core, this should be<br>
workable. I'm not sure that it would be easy to map the result back to<br>
surface syntax, but maybe Andy can comment.<br>
<br>
Best,<br>
<br>
Mathieu<br>
<br>
On 19 January 2015 at 00:46, Christopher Done <<a href="mailto:chrisdone@gmail.com" target="_blank">chrisdone@gmail.com</a>> wrote:<br>
> Hi<br>
><br>
> I quite enjoy doing equational reasoning to prove that my functions satisfy<br>
> some laws, I like to type out each substitution step until I get back what I<br>
> started with. The only trouble is that it's rather manual and possibly error<br>
> prone.<br>
><br>
> Is there any tooling anywhere out there that can take in a Haskell<br>
> expression and reduce it by one step? I only know of stepeval:<br>
><br>
> <a href="http://bm380.user.srcf.net/cgi-bin/stepeval.cgi?expr=foldr+%28%2B%29+0+%5B1%2C2%2C3%5D+%3D%3D+6" target="_blank">http://bm380.user.srcf.net/<u></u>cgi-bin/stepeval.cgi?expr=<u></u>foldr+%28%2B%29+0+%5B1%2C2%<u></u>2C3%5D+%3D%3D+6</a><br>
><br>
> But it's just a prototype and works on a teeny weeny subset of Haskell. As<br>
> much as I like doing tooling, my bandwidth for this area is already full.<br>
><br>
> It seems quite hard to implement such a tool with existing tooling. Real<br>
> compilers and interpreters tend to be distinctly far away from a simple<br>
> substitution model or retaining the original source code and being able to<br>
> print valid source back out.<br>
><br>
> If such a tool existed, though, it'd be super handy and you could probably<br>
> include it as another check for your build process like your type checking,<br>
> your quickcheck properties and your unit tests. I would personally invest a<br>
> little bit of time to add interactive Emacs support for such a tool.<br>
><br>
> Ciao<br>
><br>
> ______________________________<u></u>_________________<br>
> Haskell-Cafe mailing list<br>
> <a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
> <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/<u></u>mailman/listinfo/haskell-cafe</a><br>
><br>
______________________________<u></u>_________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/<u></u>mailman/listinfo/haskell-cafe</a><br>
</blockquote></div>
</div></div></blockquote></div><br></div>