Re: [Haskell-cafe] Re: Why purely in haskell?

On Fri, 11 Jan 2008 09:16:12 +0200, Lennart Augustsson wrote:

Thank you Duncan, you took the words out of my mouth. :)

On Jan 10, 2008 5:42 PM, Duncan Coutts wrote:

...

...

So let's imagine:

ones = 1 : ones

ones' = repeat 1 where repeat n = n : repeat n

So you're suggesting that:

ones == ones = True but ones' == ones' = _|_

Well if that were the case then it is distinguishing two equal values and hence breaking referential transparency. We can fairly trivially prove that ones and ones' are equal so == is not allowed to distinguish them. Fortunately it is impossible to write == above, at least using primitives within the language.

If one can prove ones == ones = True with some method, why that method cannot be made to work on ones' ? Are you thinking about repeat (f x) by any chance ? ________ Information from NOD32 ________ This message was checked by NOD32 Antivirus System for Linux Mail Servers. part000.txt - is OK http://www.eset.com