[Haskell-cafe] Re: [Haskell] (.) . (.)

[Robert Dockins]

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