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
loeb :: Functor f => f (f a -> a) -> f a loeb x = fmap (\a -> a (loeb x)) x
How could this be useful? Recalling that the type
[a] is a functor,
test_loeb_1 = [ length , \x -> x !! 0 ]
ghci> loeb test_loeb_1 [2,2]
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:
test_loeb_2_bad = [ (!! 5), 3, (!! 0) + (!! 1), (!! 2) * 2, sum . take 3, 17 ]
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:
test_loeb_2 :: [[Int] -> Int] test_loeb_2 = [ (!! 5), (const 3), (\l -> (l !! 0) + (l !! 1)) , \l -> (l !! 2) * 2, sum . take 3 , (const 17 )]
So now I run
ghci> loeb test_loeb_2 [17,3,20,40,40,17]
I took the fix point of a value that didn't exist yet and tied a very strange temporal knot. Thanks, Löb!