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

Brian Hulley brianh at metamilk.com
Sun May 28 19:17:08 EDT 2006

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
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,

Logic empowers us and Love gives us purpose.
Yet still the lukewarm dead
try hard
to destroy us.


More information about the Haskell-Cafe mailing list