Martin Escardo, 8 May 2013.

We modify

http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue.lagda
http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue.html
http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue.pdf

so that Church encodings of dialogue trees are used.

This version has no comments. Also, (1) we only account for
continuity, and (2) we provide the construction the modulus of
continuity but not its correctness, but the correctness should be
clear based on the proofs given in dialogue.*.

The practical result is that the computations are indeed much faster
using Church encodings.

A theoretical use of this is made in

http://www.cs.bham.ac.uk/~mhe/dialogue/church-dialogue-internal.lagda
http://www.cs.bham.ac.uk/~mhe/dialogue/church-dialogue-internal.html

to internalize moduli of continuity, as discussed in the paper
dialogue.pdf.

\begin{code}

module church-dialogue where

Ķ : ∀{X Y : Set} → X → Y → X
Ķ x y = x

Ş : ∀{X Y Z : Set} → (X → Y → Z) → (X → Y) → X → Z
Ş f g x = f x (g x)

data ℕ : Set where
zero : ℕ
succ : ℕ → ℕ

rec : ∀{X : Set} → (X → X) → X → ℕ → X
rec f x  zero    = x
rec f x (succ n) = f(rec f x n)

data List (X : Set) : Set where
[]  : List X
_∷_ : X → List X → List X

data _≡_ {X : Set} : X → X → Set where
refl : ∀{x : X} → x ≡ x

data type : Set where
ι   : type
_⇒_ : type → type → type

data T : (σ : type) → Set where
Zero : T ι
Succ : T(ι ⇒ ι)
Rec  : ∀{σ : type}     → T((σ ⇒ σ) ⇒ σ ⇒ ι ⇒ σ)
K    : ∀{σ τ : type}   → T(σ ⇒ τ ⇒ σ)
S    : ∀{ρ σ τ : type} → T((ρ ⇒ σ ⇒ τ) ⇒ (ρ ⇒ σ) ⇒ ρ ⇒ τ)
_·_  : ∀{σ τ : type}   → T(σ ⇒ τ) → T σ → T τ

infixr 1 _⇒_
infixl 1 _·_

Set⟦_⟧ : type → Set
Set⟦ ι ⟧ = ℕ
Set⟦ σ ⇒ τ ⟧ = Set⟦ σ ⟧ → Set⟦ τ ⟧

⟦_⟧ : ∀{σ : type} → T σ → Set⟦ σ ⟧
⟦ Zero ⟧  = zero
⟦ Succ ⟧  = succ
⟦ Rec ⟧   = rec
⟦ K ⟧     = Ķ
⟦ S ⟧     = Ş
⟦ t · u ⟧ = ⟦ t ⟧ ⟦ u ⟧

D : Set → Set → Set → Set → Set
D X Y Z A = (Z → A) → ((Y → A) → X → A) → A

η : {X Y Z A : Set} → Z → D X Y Z A
η z η' β' = η' z

β : {X Y Z A : Set} → (Y → D X Y Z A) → X → D X Y Z A
β Φ x η' β' = β' (λ y → Φ y η' β') x

D-rec : ∀{X Y Z A : Set} → (Z → A) → ((Y → A) → X → A) → D X Y Z A → A
D-rec η' β' d = d η' β'

dialogue : ∀{X Y Z : Set} → D X Y Z ((X → Y) → Z) → (X → Y) → Z
dialogue = D-rec (λ z α → z) (λ Φ x α → Φ(α x) α)

B : Set → Set → Set
B = D ℕ ℕ

kleisli-extension : ∀{X Y A : Set} → (X → B Y A) → B X A → B Y A
kleisli-extension f d η' β' = d (λ x → f x η' β') β'

B-functor : ∀{X Y A : Set} → (X → Y) → B X A → B Y A
B-functor f = kleisli-extension(λ x → η(f x))

B-Set⟦_⟧ : type → Set → Set
B-Set⟦ ι ⟧ A = B(Set⟦ ι ⟧) A
B-Set⟦ σ ⇒ τ ⟧ A = B-Set⟦ σ ⟧ A → B-Set⟦ τ ⟧ A

Kleisli-extension : ∀{X A : Set} {σ : type} → (X → B-Set⟦ σ ⟧ A) → B X A → B-Set⟦ σ ⟧ A
Kleisli-extension {X} {A} {ι} = kleisli-extension
Kleisli-extension {X} {A} {σ ⇒ τ} = λ g d s → Kleisli-extension {X} {A} {τ} (λ x → g x s) d

generic : {A : Set} → B ℕ A → B ℕ A
generic = kleisli-extension(β η)

zero' : {A : Set} → B ℕ A
zero' = η zero

succ' : {A : Set} → B ℕ A → B ℕ A
succ' = B-functor succ

rec' : ∀{σ : type}{A : Set} → (B-Set⟦ σ ⟧ A → B-Set⟦ σ ⟧ A) → B-Set⟦ σ ⟧ A → B ℕ A → B-Set⟦ σ ⟧ A
rec' {σ} {A} f x = Kleisli-extension {ℕ} {A} {σ} (rec f x)

B⟦_⟧ : ∀{σ : type}{A : Set} → T σ → B-Set⟦ σ ⟧ A
B⟦ Zero ⟧    = zero'
B⟦ Succ ⟧    = succ'
B⟦ Rec {σ} ⟧ = rec' {σ}
B⟦ K ⟧       = Ķ
B⟦ S ⟧       = Ş
B⟦ t · u ⟧   = B⟦ t ⟧ B⟦ u ⟧

dialogue-tree : {A : Set} → T((ι ⇒ ι) ⇒ ι) → B ℕ A
dialogue-tree t = B⟦ t ⟧ generic

max : ℕ → ℕ → ℕ
max zero y = y
max x zero = x
max (succ x) (succ y) = succ(max x y)

Mod-cont : B ℕ ((ℕ → ℕ) → List ℕ) → (ℕ → ℕ) → List ℕ
Mod-cont = D-rec (λ n α → []) (λ φ n α → n ∷ φ (α n) α)

Mod-cont' : B ℕ ((ℕ → ℕ) → ℕ)  → (ℕ → ℕ) → ℕ
Mod-cont' = D-rec (λ n α → zero) (λ φ n α → max (succ n) (φ (α n) α))

mod-cont : T((ι ⇒ ι) ⇒ ι) → (ℕ → ℕ) → List ℕ
mod-cont t = Mod-cont (dialogue-tree {(ℕ → ℕ) → List ℕ} t)

mod-cont' : T((ι ⇒ ι) ⇒ ι) → (ℕ → ℕ) → ℕ
mod-cont' t = Mod-cont' (dialogue-tree {(ℕ → ℕ) → ℕ} t)

-- Experiments follow:

infixl 0 _∷_

{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC succ #-}

I : ∀{σ : type} → T(σ ⇒ σ)
I {σ} = S · K · (K {σ} {σ})
I-behaviour : ∀{σ : type}{x : Set⟦ σ ⟧} → ⟦ I ⟧ x ≡ x
I-behaviour = refl

number : ℕ → T ι
number zero = Zero
number (succ n) = Succ · (number n)

t₀ : T((ι ⇒ ι) ⇒ ι)
t₀ = K · (number 17)
t₀-interpretation : ⟦ t₀ ⟧ ≡ λ α → 17
t₀-interpretation = refl
example₀ : List ℕ
example₀ = mod-cont t₀ (λ i → i)

v : ∀{γ : type} → T(γ ⇒ γ)
v = I

infixl 1 _•_
_•_ : ∀{γ σ τ : type} → T(γ ⇒ σ ⇒ τ) → T(γ ⇒ σ) → T(γ ⇒ τ)
f • x = S · f · x

Number : ∀{γ} → ℕ → T(γ ⇒ ι)
Number n = K · (number n)

t₁ : T((ι ⇒ ι) ⇒ ι)
t₁ = v • (Number 17)
t₁-interpretation : ⟦ t₁ ⟧ ≡ λ α → α 17
t₁-interpretation = refl

t₂ : T((ι ⇒ ι) ⇒ ι)
t₂ = Rec • t₁ • t₁
t₂-interpretation : ⟦ t₂ ⟧ ≡ λ α → rec α (α 17) (α 17)
t₂-interpretation = refl
example₂' : List ℕ
example₂' = mod-cont t₂ (λ i → i)

Add : T(ι ⇒ ι ⇒ ι)
infixl 0 _+_
_+_ : ∀{γ} → T(γ ⇒ ι) → T(γ ⇒ ι) → T(γ ⇒ ι)
x + y = K · Add • x • y

t₃ : T((ι ⇒ ι) ⇒ ι)
t₃ = Rec • (v • Number 1) • (v • Number 2 + v • Number 3)
t₃-interpretation : ⟦ t₃ ⟧ ≡ λ α → rec α (α 1) (rec succ (α 2) (α 3))
t₃-interpretation = refl
example₃ : List ℕ
example₃ = mod-cont t₃ succ

length : {X : Set} → List X → ℕ
length [] = 0
length (x ∷ s) = succ(length s)

t₄ : T((ι ⇒ ι) ⇒ ι)
t₄ = Rec • ((v • (v • Number 2)) + (v • Number 3)) • t₃
t₄-interpretation : ⟦ t₄ ⟧ ≡ λ α → rec α (rec succ (α (α 2)) (α 3)) (rec α (α 1) (rec succ (α 2) (α 3)))
t₄-interpretation = refl

t₅ : T((ι ⇒ ι) ⇒ ι)
t₅ = Rec • (v • (v • t₂ + t₄)) • (v • Number 2)
t₅-explicitly : t₅ ≡   (S · (S · Rec · (S · I · (S · (S · (K · (Rec · Succ)) · (S · I · (S
· (S · Rec · (S · I · (K · (number 17)))) · (S · I · (K · (number 17))))))
· (S · (S · Rec · (S · (S · (K · (Rec · Succ)) · (S · I · (S · I · (K · (number 2)))))
· (S · I · (K · (number 3))))) · (S · (S · Rec · (S · I · (K · (number 1))))
· (S · (S · (K · (Rec · Succ)) · (S · I · (K · (number 2)))) · (S · I · (K
· (number 3))))))))) · (S · I · (K · (number 2))))
t₅-explicitly = refl
t₅-interpretation : ⟦ t₅ ⟧ ≡ λ α → rec α (α(rec succ (α(rec α (α 17) (α 17)))
(rec α (rec succ (α (α 2)) (α 3))
(rec α (α 1) (rec succ (α 2) (α 3)))))) (α 2)
t₅-interpretation = refl
example₅'' : ℕ
example₅'' = mod-cont' t₅ succ
\end{code}