{-# language MultiParamTypeClasses #-}

module Loeb where

import Data.Proxy

-- If I have this "spreadsheet":
--
-- s = [0, 1, s!!0+s!!1, s!!1+s!!2, ...]
--
-- it can be factored into:
--
-- s = [const 0, const 1, (\s -> s!!0+s!!1), (\s -> s!!1+s!!2), ...] <*> pure s
--
-- That leads to the loeb_A function below, so that
--
-- s = loeb_A [const 0, const 1, (\s -> s!!0+s!!1), (\s -> s!!1+s!!2), ...]
--
-- And it doesn't have to be list, it can be any Applicative data structure,
-- e.g., array.
--
-- Even ZipList behaves the same because pure does the right thing:
--
--   zipWith ($) [f0, f1, f2, ...] (pure s)
-- = zipWith ($) [f0, f1, f2, ...] [s, s, s, ...]
-- = [f0 s, f1 s, f2 s, ...]
--
-- There is a reason below why both list Applicatives do the same thing: We are
-- only using Functorness.

loeb_A :: Applicative f => f (f a -> a) -> f a
loeb_A fs = let xs = fs <*> pure xs in xs

fs :: [[Integer] -> Integer]
fs = const 0 : const 1 : [ \s -> s!!(i-2) + s!!(i-1) | i <- [2 ..]]

fibs1 :: [Integer]
fibs1 = loeb_A fs

-- But we only need Functor!  From Applicative laws,
--
--   fs <*> pure s
-- = pure ($ s) <*> fs
-- = fmap ($ s) fs
--
-- Equivalently my example could have been factored this way:
--
-- s = [0, 1, s!!0+s!!1, s!!1+s!!2, ...]
-- s = fmap ($ s) [const 0, const 1, (\s -> s!!0+s!!1), (\s -> s!!1+s!!2), ...]

loeb :: Functor f => f (f a -> a) -> f a
loeb fs = let xs = fmap ($ xs) fs in xs

fibs2 :: [Integer]
fibs2 = loeb fs


-- The above looks like memoization!  How does it relate to memoizing
-- combinators?

memo_list :: ((Int -> a) -> (Int -> a)) -> Int -> a
memo_list template = (xs !!)
  where
    xs = map (\i -> template (xs !!) i) [0..]

fib_template _ 0 = 0
fib_template _ 1 = 1
fib_template f i = f(i-1) + f(i-2)

fibs3 :: Int -> Integer
fibs3 = memo_list fib_template

-- Note that the data structure functor [] used for memoization is represented
-- by Int, [] ≅ (->)Int. The type of a memoizing combinator is then isomorphic
-- to the type of loeb:
--
--   ((Int -> a) -> (Int -> a)) -> Int -> a
-- ≅ (Int -> ((Int -> a) -> a)) -> Int -> a
-- ≅ [] ([]a -> a) -> [] a
--
-- Let's implement the conversion for all representable functors!
--
-- The Representable type class from Hutton's paper
-- https://www.cs.ox.ac.uk/publications/publication10857-abstract.html
-- https://link.springer.com/chapter/10.1007/978-3-662-54434-1_21
-- but changed to multi-param class without fundep for more user freedom.
class Functor f => Representable f i where
    (!) :: f a -> (i -> a)
    tabulate :: (i -> a) -> f a
    tabulate h = fmap h positions
    positions :: f i
    positions = tabulate id
    {-# MINIMAL (!), (tabulate | positions) #-}

instance Representable [] Int where
    (!) = (!!)
    positions = [0..]

memoByLoeb :: Representable f i => p f -> ((i -> a) -> (i -> a)) -> i -> a
memoByLoeb p template = (loeb fs !)
  where
    -- fs :: f (f a -> a)
    -- fs = tabulate ((. (!)) . (flip template))
    fs = tabulate (\i xs -> template (xs !) i) `asProxyType1Of` p

asProxyType1Of :: f a -> p f -> f a
asProxyType1Of x _ = x

fibs4 :: Int -> Integer
fibs4 = memoByLoeb (Proxy :: Proxy []) fib_template

-- A direct implementation of memoization.
memo :: Representable f i => p f -> ((i -> a) -> (i -> a)) -> i -> a
memo p template = (xs !)
  where
    xs = tabulate (template (xs !)) `asProxyType1Of` p

fibs5 :: Int -> Integer
fibs5 = memo (Proxy :: Proxy []) fib_template


{-
Notes on Löb's theorem itself:

The theorem: PAproves (PAproves A -> A) -> PAproves A

PAproves induces a modal logic; PA also allows constructing and proving certain
self-referencing sentences.  Those properties prove Löb's theorem.  See
https://en.wikipedia.org/wiki/L%C3%B6b%27s_theorem

The modal operator can look like an Applicative type constructor; Haskell also
supports recursion.  There is likely a connection between the theorem and the
function.

Further reading:

<http://blog.sigfpe.com/2006/11/from-l-theorem-to-spreadsheet.html>

LobsTheorem.pdf
(retrieved from <https://web.archive.org/web/20150430235615/http://www.yudkowsky.net/assets/44/LobsTheorem.pdf>)
-}