module Stack where
fn :: Int -> (a -> a) -> a -> a
fn 0 f x = x
fn n f x = fn (n - 1) f (f x)
suc :: Int -> Int
suc n = n + 1
exp1 :: Int -> Int -> Int
exp1 m n = fn m (fn n) suc 0
--
data Fun b = Unit (b -> b) | Rec (Fun b) (Fun b -> b -> b)
call :: Fun b -> b -> b
call (Unit f) x = f x
call (Rec env f) x = f env x
fn' :: Int -> Fun b -> b -> b
fn' 0 f x = x
fn' n f x = fn' (n - 1) f (call f x)
fn1 :: Int -> Fun b -> Fun b
fn1 n f = Rec f (fn' n)
exp2 :: Int -> Int -> Int
exp2 m n = call (fn' m (Unit (fn1 n)) (Unit suc)) 0
--
data Closure b where
Exists :: a -> (a -> b -> b) -> Closure b
callC :: Closure b -> b -> b
callC (Exists x f) y = f x y
fnC :: Int -> Closure b -> b -> b
fnC 0 c x = x
fnC n c x = fnC (n - 1) c (callC c x)
fnC1 :: Int -> Closure b -> Closure b
fnC1 n c = Exists c (fnC n)
fnC1' :: Int -> () -> Closure b -> Closure b
fnC1' n () c = fnC1 n c
sucC :: () -> Int -> Int
sucC () n = n + 1
exp3 :: Int -> Int -> Int
exp3 m n = callC (fnC m (Exists () (fnC1' n)) (Exists () sucC)) 0
--
-- type Closure b c = ... | Fn (type of env) (type of env -> b -> c) | ...
-- [[\x.^n e]] = (fn, env) where
-- fn env x = [[e]]
-- env = "free vars in [[e]]"