10

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"

TheIronKnuckle
  • 7,224
  • 4
  • 33
  • 56
  • 1
    Good question, I like! But maybe it belongs to cstheory or cs.se. – mike3996 Oct 20 '16 at 04:23
  • 4
    bottom vs. true in this context are equally valid answers for slightly different questions. Both are mathematically correct for the question they answer. – John Coleman Oct 20 '16 at 04:28
  • 4
    What does "mathematically correct" mean? By the time you have answered that question carefully, you will have answered your own as well. – Daniel Wagner Oct 20 '16 at 05:52
  • The `all` function doesn't prove statements like ∀ *x* ∈ *X* . P( *x* ) for infinite sets *X*. It is impossible to produce such a proof mechanically. For finite sets it's trivial, just check whether P holds for each element of *X*. That's what `all` does. – n. m. could be an AI Oct 20 '16 at 06:17
  • 4
    The proper way to think about this is that the list type does not properly represent cyclic lists, in a way that one can observe the cycle. If you define a datatype which allows one to observe a cycle, then you will not find it too difficult to write an `all` which checks infinite cyclic lists in finite time. In certain languages with different semantics than Haskell, such a datatype may be simple to define, e.g. due to pointer equality - perhaps this is what causes your intuition to fail here. – user2407038 Oct 20 '16 at 07:16
  • @progo CS.SE may indeed be appropriate for this. TCS.SE instead is not, since it only focuses on research-level questions. – chi Oct 20 '16 at 10:00
  • @chi: yes. Sorry, I always forget which one is which – mike3996 Oct 20 '16 at 11:19
  • 3
    @user2407038 Recognizing cycles only gets you part of the way there, and doesn't seem very satisfying to me. What about `all (> 0) [1..]`? That "should" be `True`, but the list is infinite, and has no cycle you can detect to figure things out more easily. – amalloy Oct 20 '16 at 16:10

3 Answers3

24

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.

Reid Barton
  • 14,951
  • 3
  • 39
  • 49
  • How strict is it? Does optimization technique, while replacing `all (==1) [1,1..]` with `True` will broke something important? – Alexey Birukov Oct 20 '16 at 08:00
  • 4
    @AlexeyBirukov 1) Would you also be OK with the optimizer replacing `let x = True && x in x` with `True`? or `let x=x in x` with `True`? 2) The optimizer can not spot all these cases since the problem is undecidable. Having your code that suddenly stops working because some optimization no longer kick in looks quite fragile. – chi Oct 20 '16 at 10:03
  • 1
    @AlexeyBirukov: as chi says, it wouldn't make sense for the optimiser to do that kind of thing. The few cases in which this is possible are trivial like the given example, and thus wouldn't gain you much. – leftaroundabout Oct 20 '16 at 14:52
  • Ok, but what about "Loop-invariant code motion" family of optimizations? It proved to be useful, at least for C-like laguages. Can compiler do guessing beyond the denotational semantics internally, to do something like `map (2*) [1,1..]` --> `[2,2..]`? – Alexey Birukov Oct 21 '16 at 18:16
  • @AlexeyBirukov, I don't know what you mean by "beyond the denotational semantics". `map (2*) [1,1..]` and `[2,2..]` have the same denotation, so there's no problem with replacing one by the other. – Reid Barton Oct 26 '16 at 01:44
  • @Reid Barton, Let's better consider `filter (>0) [1..]` --> `[1..]`. I mean, to be able to do this code transformation, optimizer probably must use rule like `filter the_predicate the_list` = if `all the_predicate the_list` then `the_list`. – Alexey Birukov Oct 27 '16 at 13:31
  • The compiler can use whatever kind of internal logic it wants as long as the output has the same denotation as the input. It isn't restricted to "thinking in Haskell". – Reid Barton Oct 27 '16 at 15:16
3

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.

Jon Purdy
  • 53,300
  • 8
  • 96
  • 166
2

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.

mike3996
  • 17,047
  • 9
  • 64
  • 80