Zhixuan Yang on Nostr: > Sometimes Haskell solves the fixpoint equation `inf = Succ inf` to infinity, ...

> Sometimes Haskell solves the fixpoint equation `inf = Succ inf` to infinity, instead of the least solution, which should be infinite loops.

There might be a misunderstanding here. If Nat is defined as `data Nat = Zero | Succ Nat`. This datatype in Haskell has as elements: (1) a bottom, (2) Zero, and (3) `Succ n` for an existing `n`. Modulo the usual boring statement "Haskell doesn't have a formal semantics!", we can view Nat as an equation N ~= F (1 + U N) in the category DCPPO of dcppos and non-strict continuous functions, where F : DCPO -> DCPPO freely adds a bottom element, + of dcpos is just taking their disjoint union, and U : DCPPO -> DCPO forgets the bottom. The least solution of N has the following elements:
* ⊥
* Zero
* Succ ⊥
* Succ Zero
* Succ (Succ ⊥)
* Succ (Succ Zero)
...
* ∞
with the order n ⊑ m if m = ∞ or m can be obtained by replacing a ⊥ in n with another element. In this dcppo N, the least solution 'inf = Succ inf' is already ∞, rather than ⊥.