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 > 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 ;-) 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. > Thanks, Brian. -- Rob Dockins Talk softly and drive a Sherman tank. Laugh hard, it's a long way to the bank. -- TMBG _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe