What is the mathematical significance of “all (==1

问题:

Intuitively, I would expect the "mathematical" answer to all (==1) [1,1..] to be True because all of the elements in a list that only contains 1s are equal to 1. However I understand that "computationally", the process of evaluating the infinite list in order to check that each element does in fact equal 1 will never terminate, therefore the expression instead "evaluates" to bottom or ⊥.

I find this result counter-intuitive and a little unnerving. I think the fact that the list is an infinite one confuses the issue both mathematically and computationally, and I would love to hear from anyone who has some insight and experience in this area

My question is, which is the most mathematically correct answer? ⊥ or True? Some elaboration as to why one answer is more correct than the other would also be much appreciated.

edit: This might indirectly have something to do with the Curry-Howard isomorphism (Programs are proofs and types are theorems) and Gödel's incompleteness theorems. If I remember correctly, one of the incompleteness theorems can be (incredibly roughly) summarised as saying that "sufficiently powerful formal systems (like mathematics or a programming language) cannot prove all true statements that can be expressed in the system"

回答1:

The value

all (==1) [1,1..]

is the least upper bound of the sequence

all (==1) (⊥)
all (==1) (1 : ⊥)
all (==1) (1 : 1 : ⊥)
...

and all terms of this sequence are ⊥, so the least upper bound is also ⊥. (All Haskell functions are continuous: preserve least upper bounds.)

This is using the denotational semantics for Haskell and doesn't depend (directly) on choosing any particular evaluation strategy.

回答2:

In programming, we use not classical logic, but intuitionistic (constructive) logic. We can still interpret types as theorems, but we don’t care about the truth of these theorems; instead, we talk about whether they’re constructively provable. Even though all (== 1) [1, 1 ..] is true, we can’t prove it in Haskell, so we get ⊥ (here, an infinite loop).

In constructive logic, we don’t have the law of the excluded middle, nor double negation elimination as a result. The Haskell function type all (== 1) :: [Int] -> Bool doesn’t represent the theorem [Int] → Bool, which would be a total function; it represents the theorem [Int] → ¬¬Bool. If all can prove the theorem by producing a result, then that result will be of type Bool; otherwise, the result is bottom.

回答3:

I don't know enough about computability to answer this properly, but I do draw comfort from the simplicity in the language design. In this case, I find it simple and elegant that all doesn't have to know anything about the input it's given. It's arguably easier for human to reason about the snippet that you have given.

Sure, now it would be good for the infinite list comprehension to somehow tell all that it's an infinite list of ones. But... that's what it says "by being of that value". Having a bit more generic metadata about the repeated sequence would be more successful for optimization purposes, but I think the simplicity would be reduced, and complexity introduced.