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(ι  ι  ι)
Add = Rec · Succ
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}