Cheng Zhang on Nostr: I was talking to my students about inductive and coinductive data types, and she ...

I was talking to my students about inductive and coinductive data types, and she asked what about `inf = Succ inf` in Haskell, now I cannot sleep.

The naive answer is that "this is actually a corecursion, thus defines infinity". However, the uncomfortable truth is that **Haskell semantics don't know whether definition is recursive or corecursive**.

Sometimes Haskell solves the fixpoint equation `inf = Succ inf` to infinity, instead of the least solution, which should be infinite loops.
Yet in other cases, Haskell will solve the fixpoint equation into its least solution: consider the following definition, which generates a infinite fixpoint equation where the variables are `eq n m` for all `n m in Nat`
```hs
eq Zero Zero = True
eq (Succ n) (Succ m) = eq n m
eq _ _ = False
```
the variable `eq inf inf`, in this case, is solved to its least solution infinite loop, instead of `True` like a proper corecursive language.

Intuitively, Haskell tries to explore the coalgebra generated by the fixpoint equations to compute its solutions.
**It seems like that Haskell solves to the final coalgebra when the reachable state is finite (i.e. regular), but solves to infinite loop when the reachable state is infinite.**
As a corollary, neither the standard DCPO semantics nor the standard final coalgebra semantics seems to fully capture the semantics of Haskell.