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 ℕ #-} 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}