type E a = a -> a                 -- endomorphisms
type N a = E (E a)                -- natural / iterators
type C a b = (a -> b) -> b        -- continuation

one :: E a
one = id
zero :: b -> E a -- N a  -- E (E a)  -- b -> E a
zero = const id

-- this a useful trick for printing values of functions.
type G = Integer
s :: E G 
s = (+1)
z :: G
z = 0 

pdsuc  :: E (E (E G)) 
pdsuc m g = const (g (m s z))  -- 33))  -- gives pd (n+1) = 33 + n

pd    :: E (E (E (E G)))  -> G
-- pd n =  n suCC zero id z  -- 97 -- gives pd 0 = 97
-- pd n =  ($ z) (n suCC zero id)  
-- pd n =  ($ z) (($ id) (n suCC zero))  
pd n =  (($ z) . ($ id)) (n pdsuc zero)
-- pd' = gen zero id
-- sg  = gen zero (const one)
-- sgbar = gen one (const zero)

{-
gensuc :: E (E (E (E G))) --
-- gensuc f m g = const (g (f m s z))  
gensuc f m g _ = g (f m s z)

gen
  :: E (E G)  -- a 
     -> E (E (E G)) -- f 
     -> E (E (E (E G))) -- n
     -> G
-- I express it in the form of a "lens"     
gen a f n = (($ (a s z)) . ($ id))      -- postponent
            (n (gensuc f) zero)         -- use iteration at a higher type
-}
-- gensuc :: E (E (E (E x))) --
-- gensuc f m g = const (g (f m s z))  
gensuc  :: E a -> a ->                     -- s z
          E (E (E a)) ->                   -- f is here restricted to be a polynomial
          E (E a) ->                       -- m
          E a ->                           -- g
          b -> a
-- with reordering of arguments, that could be      
-- E (E (E a)) -> E (E a) -> E a -> b -> E (E a)
gensuc s z f m g _  = g (f m s z)
gensuc'  :: E a -> a ->
          E (E (E a)) -> E (E a) -> E a ->
          b -> a
gensuc' s z f m g
   -- = const (g (f m s z))
   -- = (const . g) (f m s z)
   -- = (const . g) (z `pow` (s `pow` f m))
   =  let h x = (const . g) (z `pow` (s `pow` x))
          h'  = ((const . g) . (z `pow`) . (s `pow`))
          j g  = const  ((f m s z) `pow` g)
          -- j' g  = const  (pow (f m s z) g)
          j'   = const . (pow (f m s z))
          k m  = const . (pow ( z `pow` (s `pow` (f m))) )
          foo  = (pow z) . (pow s)
          k' m  = const . ( pow ( foo (f m)))  -- z `pow` (s `pow` (f m))
          k''   = (const .) . ( (pow . foo . f) )   -- z `pow` (s `pow` (f m))
          l f   = (const .) . ( (pow . foo . f) )   
          l' f   = ((const .) .) ( (pow . foo . f) )
          l'' f   = ((const .) .) ( ((pow .) . (foo .)) f )
          l'''    = ((const .) .) . (pow .) . (foo .)
      in  l''' f m g -- k'' m g -- j' g -- h' (f m)
-- Note the type of f. The function has to be denotable.
gen  :: E (E x)  -- a 
     -> E (E (E x)) -- f (of higher type)
     -> E (E (E (E x))) -- n
     -> E (E x)
-- I express it in the form of a "lens"     
gen a f n s z = postponent (iteration n)
                where postponent = (($ (a s z)) . ($ id))
                      iteration n = n (gensuc s z f) zero


-- some basic arithmetic: typing
times :: E a -> E (E a)
-- one :: E a
plus  :: E (E a) -> E (E (E a))
-- zero :: b -> E a
pow   :: a -> E a -> a   -- E a -> E (E a) -> E a
inc   :: E (E (E a) )     -- a denotable function.
-- basic arithmetic definitions 
inc n f = f . n f -- inc n = n `plus` one
a `pow` b = b a
a `times` b = b . a
a `plus` b = \x -> (x `pow` a) `times` (x `pow` b)

-- Examples

egs :: [ E (E a) ]
egs = [zero,one,two,three,four,five,six,seven,eight,nine,ten]

two f  = f . f
three f = f . f . f
four = two two
five = two `plus` three
six = three `times` two
seven = three `plus` four
eight = two `pow` three
nine = three `pow` two
ten = nine `plus` one

{-
(2^) n {X} s z = n {e X} (two {X}) s z 
(2^) n {X}     = n {e X} (two {X})
(2^) n         = S (n . e) two

(2^) n (phi X)    = n (phi (e X)) (two (phi X))
(2^) n . phi      = S (n . phi . e) (two . phi)
                  = 

-}
sc a b c = a c (b c)


-- Some ideas for exploration

t1 = let f = gen zero id
     in [ f n s z | n <- egs ] 

t2 = let f = gen eight (times ten)
     in [ f n s z | n <- egs ] 

t3 = let f = gen zero zero  -- 0,1,1,1....
     in [ f n s z | n <- egs ]

t4 = let f = gen one (const zero)   -- [1,0,0,0,0,0,0,0,0,0,0]
      in [ f n s z | n <- egs ]

t5 = let f = gen (ten two) (plus seven) -- [1024,7,8,9,10,11,12,13,14,15,16]
     in [ f n s z | n <- egs ]



{-
How to use a universe. (I cannot express this in Haskell.)
See the file CN.lagda

We need a universe type (operator) U that builds above any set X
an indexed family of sets {T i | i : U} closed under the endomorphism operator E. We
might call this a type of *pure* sets above X.

  U : set
  g : U  , e : U -> U   -- (e,g) : U + 1  -> U
  T g = X    : set 
  T u = E (T u) : set 

To define tetra_2 n = (2^)^n 0 (0 not certain. 1?) we need
to use n as an iterator over U.

     e^n g -- n'th pure type above X
     n {U} (e,g)

basic equation (use uncurried form). Note (z ^) : E X -> X

    (a ^ b) {X} (s,z)           = (z ^) . b {endo X} (a {X}, s)
    (2 ^ n) {X} (s,z)           = (z ^) . n {endo X} (two {X}, s)
    (2 ^ n) {e^m g} (s,z)       = (z ^) . n {e^{m+1} g} (two {e^m g}, s)
    (2 ^ n) {m {U} (e,g)} (s,z) = (z ^) . n {(m+1) {U} (e,g)} (two {m {U} (e,g)}, s)
 
-}

-- pd'' :: E (E (E G)) -> G
pd'' n s z = n (\ m _ -> m s z) id z