How many values does the fixpoint of Endo have?-CodePudding

Consider the following datatype:

newtype EndoFix = EndoFix {appEndoFix :: EndoFix -> EndoFix}

This is essentially the fixpoint of Endo from Data.Monoid. I wondered what values this type has. Some examples:

example0 = EndoFix id
example1 = EndoFix (const example0)
example2 = EndoFix (const example1)

This quickly leads us to a limit point:

import Data.Function
exampleOmega = fix (EndoFix . const)

However, I couldn't find any semidecision procedure that distinguishes these values. My intuition tells there is none, meaning that these values actually are all equal. So what's the actual topological space expressed by EndoFix?

CodePudding user response：

The only thing you can observe from this type is non-termination.

In terms of "fast and loose" reasoning, where you ignore non-termination, this type is a unit type (only one inhabitant/all inhabitants are undistinguishable). One formal argument here is that you can prove in Martin-Lof Type Theory that there cannot be a type T with an isomorphism (T -> T) <-> T and two distinct elements (x, y : T, such that x != y). (By a diagonal argument, or more abstractly, Lawvere's fixed point theorem. You might also have to assume decidable equality, which might be quite strong depending on your point of view, but still means that you will need to rely on a fancy model to exhibit a counterexample)

This means that if there is anything nontrivial about Fix Endo, it must be in the blind spot of "pretending Haskell is total / like type theory", i.e., it must involve non-termination.

We can distinguish example0, example1, and example2 by passing them some undefined arguments and forcing them.

-- force1 example0 = _|_
-- force1 example1 = () 
force1 :: EndoFix -> ()
force1 f = (f `appEndoFix` undefined) `seq` ()

-- force2 example1 = _|_
-- force2 example2 = ()
force2 :: EndoFix -> ()
force2 f = ((f `appEndoFix` undefined) `appEndoFix` undefined) `seq` ()

Using that idea, you can define infinitely many distinguishable functions: there are at least those that take n arguments and return the i-th argument.

An interpretation of EndoFix would basically be a denotational semantics for the untyped lambda calculus, with seq as an extra feature.

-- HOAS embedding of untyped lambda calculus in EndoFix
app :: EndoFix -> EndoFix -> EndoFix
lam :: (EndoFix -> EndoFix) -> EndoFix

A well-known example is given by Dana Scott in Continuous Lattices (which culminates in Theorem 4.4). The general idea is to consider F a = a -> a as an operation on lattices/CPOs, and construct EndoFix as the limit of its iterated applications F^n ∅. So one way to approach this space is to enumerate the inhabitants of F^n ∅ for small values of n.

Another relevant resource is the chapter on Denotational Semantics of Untyped Lambda Calculus in Programming Language Foundations in Agda, which gives a more concrete definition.