Why is there only one non-strict function from Int to Int?

Question

According to this article on denotational semantics for Haskell there is only one non-strict (non-bottom prreserving) function from Int to Int.

to quote:

it happens that there is only one prototype of a non-strict function of type Integer -> Integer:

one x = 1

Its variants are constk x = k for every concrete number k. Why are these the only ones possible? Remember that one n can be no less defined than one ⊥. As Integer is a flat domain, both must be equal.

Essentially it says that the only non-strict functions of that type signature can only be the constant functions. I don't follow this argument. I'm also unsure what is meant by a flat domain, the rest of the article leads to believe that it simply means that the poset of values has only one node: bottom.

Does something similar occur for function going from A->A, or A->B? That is they must be constant functions?

Answer 1

Any function on Integer that is not const k for some constant k must inspect its argument. You can't partially inspect an Integer, which might be is what is meant by it being a "flat domain". This is a consequence of how the semantics of Integer are defined in the Haskell specs, not something that follows from the core language's semantics.

By contrast, infinitely many non-strict functions of type [a] -> [a] exist for every type a, e.g. take1:

take1 (x:_) = [x]

To show non-strictness, define

ones = 1 : ones

In terms of denotational semantics, [[ones]] = ⊥. But take1 ones evaluates to [1], so take1 is non-strict. So are take2 (x:y:_) = [x,y], take10, etc.

If you want non-strict, non-constant functions on integers, you need a different representation of the integers than Integer, e.g.:

data Bit = Zero | One
newtype BinaryInt = I [Bit]

If we interpret the list in an I as a "little-endian" binary integer, then the function

mod2 (I [])       =  I []
mod2 (I (lsb:_))  =  I [lsb]

is non-strict.

Answer 2

The intuition is that a lazy function can't inspect its argument here without forcing it (and hence become strict). If you don't inspect your argument you have to be const

The real answer in monotonicity. If you think of semantic domains as posets where the ordering relationship is one of "defined-ness", all functions are order preserving. Why? Since all bottoms are created equal, and looping forever is the same thing as bottom, a non monotonic function would be one that solves the halting problem.

Okay, so why does that imply it const creates the only lazy functions? Well, say pick an arbitrary function f such that

f :: Integer -> Integer
f ⊥ = y

since ⊥ <= x for all x, it must be that y <= f x. If y is a non bottom value, then the only solution to that inequality is f x = y

Edit: The reason why this argument holds for types like Integer and Bool but not for types like [a] is the last step: Integer in a sense only has a single ⊥ in it. That is, all Integers are equally defined except for ⊥. On the other hand, ⊥ < (⊥:⊥) while (⊥:⊥) < (⊥:[]) and (⊥:⊥) < (⊥:(⊥:⊥)) < (⊥:(⊥:(⊥:⊥))) < ... whats more, (⊥:⊥) < ('a':⊥). That is, the semantic domain of [a] is rich enough that y <= f x with y =/= ⊥ does not imply that f x = y.