Robert Dockins wrote:
On Sunday 28 May 2006 05:50 pm, you wrote:
[moved to cafe]
Robert Dockins wrote:
On Sunday 28 May 2006 05:02 pm, Brian Hulley wrote:
I see my error was that I was reversing the args in eta expansion, so the correct derivation is:
FYI, eta-expansions isn't valid in Haskell. Its safe in this derivation, but it isn't always.
Am I right in thinking that this is because of _|_ ?
Yup. Well, _|_ and seq, really. IIUC, the removal of seq restores the validity of eta-conversion.
seq _|_ x = _|_
but,
seq (\z -> _|_ z) x = x
Thanks for the illustration. I now recall that Jon Fairbairn wrote in http://www.haskell.org//pipermail/haskell-cafe/2006-March/015125.html that seq shouldn't be a function so I suppose this is why.
In any case I suppose I should have instead just replaced the function with it's definition like you (view Lambda Shell) and Christophe did.
Also, is your Lambda Shell publicly available? (I had a quick look on the wiki in the Theorem provers section but couldn't find a link.)
http://www.eecs.tufts.edu/~rdocki01/lambda.html
I've never thought of it as a theorem prover before ;-)
I was just considering any kind of automated derivation to be a proof...
You can also play with it on #haskell via the lambdabot '@lam' command. I think it binds to a slightly older version, but there aren't many user-visible changes.
Best regards, Brian. -- Logic empowers us and Love gives us purpose. Yet still the lukewarm dead try hard to destroy us. http://www.metamilk.com