On Thu, 27 Dec 2007 16:50:10 +0200, Lennart Augustsson wrote:

Absolutly. Every expression in Haskell denotes a value. Now, we've not agreed what "value" means, but to me it is a value. :)

It is one value, or several ? ________ Information from NOD32 ________ This message was checked by NOD32 Antivirus System for Linux Mail Servers. part000.txt - is OK http://www.eset.com

I'll have to trust you, because I cannot test it. let x=(1:x); y=(1:y) in x==y . I also cannot test this: let x=(1:x); y=1:1:y in x==y On Thu, 27 Dec 2007 17:29:12 +0200, Lennart Augustsson wrote:

One value. One "infinite" value.

On Dec 27, 2007 3:53 PM, Cristian Baboi wrote:

...

On Thu, 27 Dec 2007 16:50:10 +0200, Lennart Augustsson wrote:

...

Absolutly. Every expression in Haskell denotes a value. Now, we've not agreed what "value" means, but to me it is a value. :)

It is one value, or several ?

________ Information from NOD32 ________ This message was checked by NOD32 Antivirus System for Linux Mail Servers. part000.txt - is OK http://www.eset.com

________ Information from NOD32 ________ This message was checked by NOD32 Antivirus System for Linux Mail Servers. part000.txt - is OK part001.htm - is OK http://www.eset.com

________ Information from NOD32 ________ This message was checked by NOD32 Antivirus System for Linux Mail Servers. part000.txt - is OK http://www.eset.com

On Thu, 27 Dec 2007 17:45:04 +0200, Jonathan Cast wrote:

On 27 Dec 2007, at 9:34 AM, Cristian Baboi wrote:

...

I'll have to trust you, because I cannot test it.

let x=(1:x); y=(1:y) in x==y .

I also cannot test this:

let x=(1:x); y=1:1:y in x==y

Correct. You could try proving it.

I cannot. Can you try to prove it is raining here where I am ? ________ Information from NOD32 ________ This message was checked by NOD32 Antivirus System for Linux Mail Servers. part000.txt - is OK http://www.eset.com

Wolfgang Jeltsch wrote:

If x doesn’t equal y, x == y is False, but if x equals y, x == y might be True or undefined.

x == y may be _|_ for the False case, too, depending on its implementation (like first comparing all list elements on even indices and then comparing all list elements on odd indices). But the standard == for lists has indeed the stated property. Regards, apfelmus

Wolfgang Jeltsch wrote:

Am Donnerstag, 27. Dezember 2007 16:34 schrieb Cristian Baboi:

...

I'll have to trust you, because I cannot test it.

let x=(1:x); y=(1:y) in x==y .

I also cannot test this:

let x=(1:x); y=1:1:y in x==y

In these examples, x and y denote the same value but the result of x == y is _|_ (undefined) in both cases. So (==) is not really equality in Haskell but a kind of weak equality: If x doesn’t equal y, x == y is False, but if x equals y, x == y might be True or undefined.

[1..] == [1..] certainly isn't undefined, it always evaluates to True, just like [2..] == [2..]. It just takes ghci eternity to prove, as its runtime system doesn't even think of trying to put the axiom forall n: if x == y then x + n == y + n together with its knowledge about the equal stepping of the lists and short-circuit to True.

Jonathan Cast wrote:

On 27 Dec 2007, at 10:44 AM, Achim Schneider wrote:

...

Wolfgang Jeltsch wrote:

...

Am Donnerstag, 27. Dezember 2007 16:34 schrieb Cristian Baboi:

...

I'll have to trust you, because I cannot test it.

let x=(1:x); y=(1:y) in x==y .

I also cannot test this:

let x=(1:x); y=1:1:y in x==y

In these examples, x and y denote the same value but the result of x == y is _|_ (undefined) in both cases. So (==) is not really equality in Haskell but a kind of weak equality: If x doesn’t equal y, x == y is False, but if x equals y, x == y might be True or undefined.

[1..] == [1..] certainly isn't undefined, it always evaluates to True,

If something happens, it does eventually happen.

More importantly, we can prove that [1..] == [1..] = _|_, since

[1..] == [1..] = LUB (n >= 1) [1..n] ++ _|_ == [1..n] ++ _|_ = LUB (n >= 1) _|_ = _|_

As far as I understand http://www.haskell.org/haskellwiki/Bottom , only computations which cannot be successful are bottom, not those that can be successful, but aren't. Kind of idealizing reality, that is. Confusion of computations vs. reductions and whether time exists or not is included for free here. Actually, modulo mere words, I accept both your and my argument as true, but prefer mine. You _do_ accept that you won't ever see Prelude.undefined in ghci when evaluating let x=(1:x); y=(1:y) in x==y , and there won't ever be a False in the chain of &&'s, don't you? The question arises, which value is left from the possible values of Bool when you take away False and _|_? And now don't you dare to say that _|_ /= undefined.

Jonathan Cast wrote:

_|_ is the denotation of every Haskell expression whose denotation is _|_.

Mu.

Why take away _|_?

Because, when zenning about instance (Eq a) => Eq [a] where [] == [] = True (x:xs) == (y:ys) = x == y && xs == ys _xs == _ys = False and [n..] == [m..], the first thing I notice is n == m && n+1 == m+1 , which already expresses all of infinity in one instance and can be trivially cancelled to n == m , which makes the whole darn thing only _|_ if n or m is _|_, which no member of [n..] can be as long as n isn't or 1 or + has funny ideas. I finally begin to understand my love and hate relationship with formalisms: It involves cuddling with fixed points while protecting them from evil data and fixed points they don't like as well as reduction strategies that don't see their full beauty.

Achim Schneider wrote:

[n..] == [m..],

the first thing I notice is

n == m && n+1 == m+1

, which already expresses all of infinity in one instance and can be trivially cancelled to

n == m

, which makes the whole darn thing only _|_ if n or m is _|_, which no member of [n..] can be as long as n isn't or 1 or + has funny ideas.

I finally begin to understand my love and hate relationship with formalisms: It involves cuddling with fixed points while protecting them from evil data and fixed points they don't like as well as reduction strategies that don't see their full beauty.

There is a formalism that says [n..]==[n..] is true. (Look for co-induction, observational equivalence, bismulation, ...) There is a formalism that says [n..]==[n..] is _|_. We know of implemented programming languages that can give an answer according to the latter formalism. If you know of an implemented programming language that can give an answer according to the former formalism, and not just for the obvious [n..] but also map f xs == map g xs (for example), please spread the news. So it comes down to which formalism, not whether formalism. I have long known the problem with informalisms. They are full of "I know", "obviously", and "ought to be". It is too tempting to take your wit for granted. When you make a deduction, you don't easily see whether it is one of a systemtic family of deductions or you are just cunning. You only see what you can do; you don't see what you can't do, much less what you can't make a computer do. Formalisms do not tolerate such self-deception. You think something ought to be obvious? Write them down as axioms. Now with all your obviousness nailed down black on white, you have a solid ground on which to ask: what can be done, what can't be done, what can be done on a computer, how practical is it? Humility and productivity are thus restored.

There's no (valid) formalism that says that [n..]==[n..] is True. The formalism says that [n..] and [n..] are equal. But being equal does not mean that the Haskell (==) function returns True. The (==) function is just an approximation of semantic equality (by necessity). -- Lennart On Dec 28, 2007 3:38 AM, Albert Y. C. Lai wrote:

Achim Schneider wrote:

...

[n..] == [m..],

the first thing I notice is

n == m && n+1 == m+1

, which already expresses all of infinity in one instance and can be trivially cancelled to

n == m

, which makes the whole darn thing only _|_ if n or m is _|_, which no member of [n..] can be as long as n isn't or 1 or + has funny ideas.

I finally begin to understand my love and hate relationship with formalisms: It involves cuddling with fixed points while protecting them from evil data and fixed points they don't like as well as reduction strategies that don't see their full beauty.

There is a formalism that says [n..]==[n..] is true. (Look for co-induction, observational equivalence, bismulation, ...)

There is a formalism that says [n..]==[n..] is _|_.

We know of implemented programming languages that can give an answer according to the latter formalism.

If you know of an implemented programming language that can give an answer according to the former formalism, and not just for the obvious [n..] but also map f xs == map g xs (for example), please spread the news.

So it comes down to which formalism, not whether formalism.

I have long known the problem with informalisms. They are full of "I know", "obviously", and "ought to be". It is too tempting to take your wit for granted. When you make a deduction, you don't easily see whether it is one of a systemtic family of deductions or you are just cunning. You only see what you can do; you don't see what you can't do, much less what you can't make a computer do.

Formalisms do not tolerate such self-deception. You think something ought to be obvious? Write them down as axioms. Now with all your obviousness nailed down black on white, you have a solid ground on which to ask: what can be done, what can't be done, what can be done on a computer, how practical is it? Humility and productivity are thus restored. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On 28 Dec 2007, at 2:08 AM, Cristian Baboi wrote:

On Thu, 27 Dec 2007 20:46:24 +0200, Jonathan Cast wrote:

...

Preference doesn't come into it. By definition, the denotations of Haskell functions are monotone continous functions on pointed complete partial orders.

...

You seem to think that _|_ is defined in terms of operational semantics. Haskell hasn't got an operational semantics, just a denotational semantics that implementations must produce an operational semantics to match with. _|_ is a denotational idea, defined in terms of partial orders and least upper bounds. An infinite list is the least upper bound of an infinite set of partial lists, and the value of any function (such as \x -> x == x) applied to it is the least upper bound of the values of that function applied to those partial lists.

By definition.

Questions:

The fact that Haskell functions are monotone continous functions on pointed complete partial orders imply this ?

- every domain in Haskell is a "pointed complete partial order", including domains of functions ?

Yes.

- the "structure" of a domain is preserved in the result when you apply a Haskell function to it ?

The structure is preserved by every function, but that's a global property, not really something that applies to a particular application f x.

- every domain can be enumerated ?

There exist models of Haskell where the domain representing every type is recursively enumerable, yes. But the critical thing for finding a printing function is enumerating each value /once/, which is harder to do. (I'm not aware of a way to do it). jcc

apfelmus wrote:

Ah, that's only a glitch in the wording. [1..] == [1..] is still _|_ since it loops forever.

And if it wouldn't? After all, arguing that |N == |N is undefined because it takes too long to check would earn you a straight F in any math test. It's just that I always assumed that haskell is defined by exactly those semantics (which I admittedly never really read), not by its runtime behaviour, which can change from implementation to implementation. Fuck, I'm smartassing _and_ nitpicking, and for the worst of it with the "Smart enough compiler"-argument, all of that just after stopping lurking.

The value of "let x=(1:x); y=(1:y) in x==y" definitely _|_ )bottom) and nothing else. A value of type Bool can be False, True, or _|_ and that expression does not yield a False or True. It has nothing to do with time, it's just mathematics. What might be confusing you is that _|_ is often used as a name for non-termination, undefined, error etc. -- Lennart On Dec 27, 2007 7:20 PM, Achim Schneider wrote:

Jonathan Cast wrote:

...

On 27 Dec 2007, at 10:44 AM, Achim Schneider wrote:

...

Wolfgang Jeltsch wrote:

...

Am Donnerstag, 27. Dezember 2007 16:34 schrieb Cristian Baboi:

...

I'll have to trust you, because I cannot test it.

let x=(1:x); y=(1:y) in x==y .

I also cannot test this:

let x=(1:x); y=1:1:y in x==y

In these examples, x and y denote the same value but the result of x == y is _|_ (undefined) in both cases. So (==) is not really equality in Haskell but a kind of weak equality: If x doesn't equal y, x == y is False, but if x equals y, x == y might be True or undefined.

[1..] == [1..] certainly isn't undefined, it always evaluates to True,

If something happens, it does eventually happen.

More importantly, we can prove that [1..] == [1..] = _|_, since

[1..] == [1..] = LUB (n >= 1) [1..n] ++ _|_ == [1..n] ++ _|_ = LUB (n >= 1) _|_ = _|_

As far as I understand http://www.haskell.org/haskellwiki/Bottom , only computations which cannot be successful are bottom, not those that can be successful, but aren't. Kind of idealizing reality, that is.

Confusion of computations vs. reductions and whether time exists or not is included for free here. Actually, modulo mere words, I accept both your and my argument as true, but prefer mine.

You _do_ accept that you won't ever see Prelude.undefined in ghci when evaluating let x=(1:x); y=(1:y) in x==y , and there won't ever be a False in the chain of &&'s, don't you?

The question arises, which value is left from the possible values of Bool when you take away False and _|_?

And now don't you dare to say that _|_ /= undefined.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Am Freitag, 28. Dezember 2007 07:49 schrieben Sie:

On Thu, 27 Dec 2007 18:19:47 +0200, Wolfgang Jeltsch wrote:

...

Am Donnerstag, 27. Dezember 2007 16:34 schrieb Cristian Baboi:

...

I'll have to trust you, because I cannot test it.

let x=(1:x); y=(1:y) in x==y .

I also cannot test this:

let x=(1:x); y=1:1:y in x==y

In these examples, x and y denote the same value but the result of x == y is _|_ (undefined) in both cases. So (==) is not really equality in Haskell but a kind of weak equality: If x doesn’t equal y, x == y is False, but if x equals y, x == y might be True or undefined.

Thank you.

I can only notice that y always has an even number of 1, which is not the case for x :-)

Both have an infinite number of 1. Why do you say “always”? It seems that you think of x and y as “variables” whose values change over time. This is not the case. They both have a single value for all time: the infinite list consisting only of 1. Best wishes, Wolfgang

Am Freitag, 28. Dezember 2007 17:27 schrieb Achim Schneider:

...

Both have an infinite number of 1. Why do you say “always”? It seems that you think of x and y as “variables” whose values change over time. This is not the case. They both have a single value for all time: the infinite list consisting only of 1.

Does that then mean that [1] = [1,1] ?

No, it means you cannot distinguish (repeat 1) from (cycle [1,1]). Is infinity an even number or an odd one? Cheers, Daniel

On Fri, 28 Dec 2007 18:27:29 +0200, Achim Schneider wrote:

Wolfgang Jeltsch wrote:

...

Am Freitag, 28. Dezember 2007 07:49 schrieben Sie:

...

On Thu, 27 Dec 2007 18:19:47 +0200, Wolfgang Jeltsch wrote:

...

Am Donnerstag, 27. Dezember 2007 16:34 schrieb Cristian Baboi:

...

I'll have to trust you, because I cannot test it.

let x=(1:x); y=(1:y) in x==y .

I also cannot test this:

let x=(1:x); y=1:1:y in x==y

In these examples, x and y denote the same value but the result of x == y is _|_ (undefined) in both cases. So (==) is not really equality in Haskell but a kind of weak equality: If x doesn’t equal y, x == y is False, but if x equals y, x == y might be True or undefined.

Thank you.

I can only notice that y always has an even number of 1, which is not the case for x :-)

Both have an infinite number of 1. Why do you say “always”? It seems that you think of x and y as “variables” whose values change over time. This is not the case. They both have a single value for all time: the infinite list consisting only of 1.

Does that then mean that [1] = [1,1]

No. If you try to learn Haskell don't listen to me. :-)

Am Donnerstag, 27. Dezember 2007 15:53 schrieb Cristian Baboi:

On Thu, 27 Dec 2007 16:50:10 +0200, Lennart Augustsson

wrote:

...

Absolutly. Every expression in Haskell denotes a value. Now, we've not agreed what "value" means, but to me it is a value. :)

It is one value, or several ?

It is one value with parts that are values themselves. Best wishes, Wolfgang

Am Freitag, 28. Dezember 2007 07:49 schrieben Sie:

On Thu, 27 Dec 2007 18:14:53 +0200, Wolfgang Jeltsch

wrote:

...

Am Donnerstag, 27. Dezember 2007 15:53 schrieb Cristian Baboi:

...

On Thu, 27 Dec 2007 16:50:10 +0200, Lennart Augustsson

wrote:

...

Absolutly. Every expression in Haskell denotes a value. Now, we've not agreed what "value" means, but to me it is a value. :)

It is one value, or several ?

It is one value with parts that are values themselves.

It is one value or a SET of values ? What are the parts ?

A set of values is again a value. So is a list of values. This is similar to C++ where a field of an object can again be an object. [1..] is a value of type [Int] and every element can be considered a part of this value. Best wishes, Wolfgang P.S.: Didn’t send this to the list in the first place. I don’t like mailing lists which don’t set the Reply-To: field.

On 27 Dec 2007, at 8:28 AM, Cristian Baboi wrote:

How about x below:

let x=(1:x) in x ?

Is x a single value in Haskell ?

(let x=1:x in x) is. x went out of scope a couple of lines back. jcc