This is an attempt at writing a more succinct exploration of the topics found here; I do not claim this as original work.
In provability logic, Löb’s theorem states:
□ ( □ P → P ) → □ P
In English, “If a system has Peano arithmetic, then if for any p the statement ‘if p is provable then p is true’ is true, then p is provable.”
According to the Curry-Howard isomorphism, in type systems like that of Haskell’s types correspond to logical propositions, and functions inhabiting those types are proofs. So if a type’s definability implies its validity then it is definable.
Somebody had this bright idea of pretending □ was some functor f and encoded this property in a function called
How could this be useful? Recalling that the type
[a] is a functor,
Intuitively it’s like a spreadsheet: you take (in this case) a row of cells containing functions which assume the final spreadsheet is finished, and they can rely on each other for their final values.
\x -> x !! 0 are both functions which accept a list as an argument and return a single item of the list. The length of the
test_loeb_1 list is 2 so
length is 2, and thus
x !! 0 is 2.
Here’s a more elaborate example:
However, this is bad because
17 aren’t functions. Haskell has a standard function,
const :: a -> b -> a, which we can use to turn ordinary values into functions:
So now I run
I took the fix point of a value that didn’t exist yet and tied a very strange temporal knot. Thanks, Löb!