# Is it possible to type Ackermann function with (stratified variant of) System F?

I was surprised to find no open-source implementation of Ackermann function in pure System F as an illustrative example. I finally managed to implement it myself in Haskell using Church encoding:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ImpredicativeTypes #-}

type Nat = forall a . (a -> a) -> (a -> a)

succ :: Nat -> Nat
succ n = \s z -> n s (s z)

c0 :: Nat
c1 :: Nat

c0 = \_s z -> z
c1 = succ c0

exp :: Nat -> Nat -> Nat
exp = \n m -> n m

tetr :: Nat -> Nat -> Nat
tetr k n = n @Nat (\x -> x k) c1

iter :: (Nat -> Nat) -> (Nat -> Nat)
iter f n = (n @Nat) f c1

ack :: Nat -> Nat -> Nat
ack = \m -> (m @(Nat -> Nat)) iter succ


You can notice a variant of tetration on the way.

Can Ackermann function (and tetration) be defined as a pure lambda term without inductive types in a predicative system?

For instance in Agda with level polymorphism?

If not, what other type-theory tools apart from inductive types, can help us define non-primitive-recursive functions?

• For a part of the latter question it seems to me that type level (smallest) fixed point would allow to encode Scott numerals and with that encode easily Ackermann function and more. Fixed point feels very powerful. – Łukasz Lew Jun 10 '18 at 15:19
• As a first step, I would recommend trying to transcribe your implementation in Agda itself! You might have to define several versions of Nat, say Nat₁, Nat₂, etc. Long story short, I think you can define the Ackermann function with just 3 "stacks" of universes, but haven't tried myself. – cody Jun 12 '18 at 14:32
• I learned Agda to try it :). I got exponentiation to work, even tetration, but pentation seems impossible, not even getting close to Ackermann's function. I'll post a separate question. – Łukasz Lew Jun 13 '18 at 15:03
• – Łukasz Lew Jun 13 '18 at 15:15