GenericTrees.agda

module GenericTrees where
open import Agda.Builtin.String
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Primitive

variable l : Level

-- Products and sums

infixr 4 _,_
record _×_ (A : Set l) (B : Set l) : Set l where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B

≡/, : ∀ {A : Set l} {B : Set l} {a a' : A} {b b' : B} →
  a ≡ a' → b ≡ b' → (a , b) ≡ (a' , b')
≡/, refl refl = refl

transp : ∀ {A : Set l} {B : Set l} → (A ≡ B) → A → B
transp refl x = x

record ⊤ {l : Level} : Set l where
  constructor tt

data ⊥ {l : Level} : Set l where

data _⊎_ (A : Set l) (B : Set l) : Set l where
  inj₁ : A → A ⊎ B
  inj₂ : B → A ⊎ B

data Maybe (A : Set l) : Set l where
  nothing : Maybe A
  just : A → Maybe A

infixr 9 _∘_
_∘_ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
      (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
      ((x : A) → C (g x))
f ∘ g = λ x → f (g x)


--
-- Computing with Generic Trees in Agda
-- Stephen Dolan, TyDE 2022
-- 





-- Codes for finite types

infixr 20 _+_
data Fin : Set where
  none : Fin
  one : String → Fin
  _+_ : Fin → Fin → Fin


-- Interpretations of finite types

record NamedUnit (Name : String) {l} : Set l where
  constructor tt

⟦_⟧ : Fin → Set
⟦ none ⟧ = ⊥
⟦ one name ⟧ = NamedUnit name
⟦ A + B ⟧ = ⟦ A ⟧ ⊎ ⟦ B ⟧

-- Convenience functions for finding elements of a finite type

variable A : Fin

lookup : (A : Fin) → String → Maybe ⟦ A ⟧
lookup none s = nothing
lookup (one t) s with primStringEquality t s
... | false = nothing
... | true = just tt
lookup (A + B) s with lookup A s
... | just x = just (inj₁ x)
... | nothing with lookup B s
... | just x = just (inj₂ x)
... | nothing = nothing

data Found : Set where
  ⟩ : Found

inhabSet : ∀ {A : Set} → Maybe A → Set
inhabSet nothing = ⊥
inhabSet (just _) = Found

⟨ : ∀ {A : Fin} → (s : String) → inhabSet (lookup A s) → ⟦ A ⟧
⟨ {A} s with lookup A s
... | nothing = λ ()
... | just x = λ _ → x

--- Example

foobarbaz = ⟦ one "foo" + one "bar" + one "baz" ⟧
bar : foobarbaz
bar = ⟨ "bar" ⟩


-- Function types with finite domains

record One (Name : String) {l} (S : Set l) : Set l where
  constructor v
  field
    contents : S

_↦_ : (Name : String) → {l : _} {S : Set l} → S → One Name S
_ ↦ x = v x

≡/v : ∀ {n} {A : Set l} {a a' : A} → (a ≡ a') → n ↦ a ≡ n ↦ a'
≡/v refl = refl

_→°_ : Fin → Set l → Set l
none →° S = ⊤
one name →° S = One name S
(A + B) →° S = (A →° S) × (B →° S)

λ° : {S : Set l} → (⟦ A ⟧ → S) → (A →° S)
λ° {A = none} f = tt
λ° {A = one _} f = v (f tt)
λ° {A = A + B} f = λ° (f ∘ inj₁) , λ° (f ∘ inj₂)

_◃°_ : {S : Set l} → (A →° S) → (⟦ A ⟧ → S)
_◃°_ {A = one _} (v f) tt = f
_◃°_ {A = A + B} (f , g) (inj₁ x) = f ◃° x
_◃°_ {A = A + B} (f , g) (inj₂ x) = g ◃° x

beta° : {S : Set l} (f : ⟦ A ⟧ → S) (x : ⟦ A ⟧) → (λ° f ◃° x) ≡ f x
beta° {A = one _} f tt = refl
beta° {A = A + B} f (inj₁ x) = beta° (f ∘ inj₁) x
beta° {A = A + B} f (inj₂ x) = beta° (f ∘ inj₂) x

eta° : {S : Set l} (f : A →° S) → f ≡ λ° λ x → f ◃° x
eta° {A = none} tt = refl
eta° {A = one _} (v x) = refl
eta° {A = A + B} (f , g) = ≡/, (eta° f) (eta° g)

ext° : {S : Set l} (f g : ⟦ A ⟧ → S) → (eq : ∀ x → f x ≡ g x) → λ° f ≡ λ° g
ext° {A = none} f g eq = refl
ext° {A = one _} f g eq = ≡/v (eq tt)
ext° {A = A + B} f g eq =
  ≡/, (ext° (f ∘ inj₁) (g ∘ inj₁) (eq ∘ inj₁))
      (ext° (f ∘ inj₂) (g ∘ inj₂) (eq ∘ inj₂))


-- Dependent function types with finite domains (i.e. tuples)
Π° : (A : Fin) (U : A →° Set l) → Set l
Π° none U = ⊤
Π° (one name) (v U) = One name U
Π° (A + B) (U , V) = (Π° A U) × (Π° B V)


Λ° : {U : A →° Set l} → ((x : ⟦ A ⟧) → U ◃° x) → (Π° A U)
Λ° {none} f = tt
Λ° {one _} f = v (f tt)
Λ° {A + B} f = Λ° (f ∘ inj₁) , Λ° (f ∘ inj₂)

_◁°_ : {U : A →° Set l} → (Π° A U) → (a : ⟦ A ⟧) → U ◃° a
_◁°_ {one _} (v f) x = f
_◁°_ {A + B} (f , g) (inj₁ x) = f ◁° x
_◁°_ {A + B} (f , g) (inj₂ x) = g ◁° x

Beta° : {U : A →° Set l} → (f : ((x : ⟦ A ⟧) → U ◃° x)) → (a : ⟦ A ⟧) → Λ° f ◁° a ≡ f a
Beta° {one _} f tt = refl
Beta° {A + B} f (inj₁ x) = Beta° (f ∘ inj₁) x
Beta° {A + B} f (inj₂ x) = Beta° (f ∘ inj₂) x

Eta° : {U : A →° Set l} → (f : Π° A U) → f ≡ Λ° λ x → f ◁° x
Eta° {none} tt = refl
Eta° {one _} (v f) = refl
Eta° {A + B} (f , g) = ≡/, (Eta° f) (Eta° g)

Ext° : {U : A →° Set l} → (f g : (x : ⟦ A ⟧) → U ◃° x) → (eq : ∀ x → f x ≡ g x) → Λ° f ≡ Λ° g
Ext° {none} f g eq = refl
Ext° {one _} f g eq = ≡/v (eq tt)
Ext° {A + B} f g eq =
  ≡/, (Ext° (f ∘ inj₁) (g ∘ inj₁) (eq ∘ inj₁))
      (Ext° (f ∘ inj₂) (g ∘ inj₂) (eq ∘ inj₂))


-- Partitioned sets

record PSet : Set₁ where
  constructor pset
  field
    parts : Fin
    elems : parts →° Set

⟦_⟧* : PSet → Set
⟦ pset none E ⟧* = ⊥
⟦ pset (one name) (v E) ⟧* = NamedUnit name × E
⟦ pset (P + Q) (E , F) ⟧* = ⟦ pset P E ⟧* ⊎ ⟦ pset Q F ⟧*

el : ∀ {P E} → (p : ⟦ P ⟧) → (E ◃° p) → ⟦ pset P E ⟧*
el {one x} p e = tt , e
el {P + Q} (inj₁ p) e = inj₁ (el p e)
el {P + Q} (inj₂ q) e = inj₂ (el q e)

_→*_ : ∀ {l} → PSet → Set l → Set l
pset none tt →* S = ⊤
pset (one name) (v E) →* S = One name (E → S)
pset (P + Q) (E , F) →* S = ((pset P E) →* S) × ((pset Q F) →* S)

variable
  X : PSet

λ* : {S : Set l} → (⟦ X ⟧* → S) → (X →* S)
λ* {X = pset none tt} f = tt
λ* {X = pset (one n) (v E)} f = n ↦ λ x → f (tt , x)
λ* {X = pset (P + Q) (E , F)} f = λ* (f ∘ inj₁) , λ* (f ∘ inj₂)

_◃*_ : {S : Set l} → (X →* S) → ⟦ X ⟧* → S
_◃*_ {X = pset (one _) (v E)} (v f) (tt , e) = f e
_◃*_ {X = pset (P + Q) (E , F)} (f , g) (inj₁ x) = f ◃* x
_◃*_ {X = pset (P + Q) (E , F)} (f , g) (inj₂ x) = g ◃* x

beta* : {S : Set l} (f : ⟦ X ⟧* → S) (x : ⟦ X ⟧*) → (λ* f ◃* x) ≡ f x
beta* {X = pset (one _) E} f (tt , e) = refl
beta* {X = pset (A + B) E} f (inj₁ x) = beta* (f ∘ inj₁) x
beta* {X = pset (A + B) E} f (inj₂ x) = beta* (f ∘ inj₂) x

eta* : {S : Set l} (f : X →* S) → f ≡ λ* λ x → f ◃* x
eta* {X = pset none E} tt = refl
eta* {X = pset (one _) E} x = refl
eta* {X = pset (A + B) E} (f , g) = ≡/, (eta* f) (eta* g)

-- ext* requires FunExt
FunExt : (l l' : Level) → Set (lsuc l ⊔ lsuc l')
FunExt l l' = {A : Set l} {B : Set l'} {f g : A → B} → (∀ a → f a ≡ g a) → f ≡ g

ext* : FunExt lzero l → {S : Set l} → (f g : ⟦ X ⟧* → S) → (eq : ∀ x → f x ≡ g x) → λ* f ≡ λ* g
ext* {X = pset none E} FE f g eq = refl
ext* {X = pset (one _) E} FE f g eq = ≡/v (FE λ x → eq _) 
ext* {X = pset (A + B) E} FE f g eq =
  ≡/, (ext* FE (f ∘ inj₁) (g ∘ inj₁) (eq ∘ inj₁))
      (ext* FE (f ∘ inj₂) (g ∘ inj₂) (eq ∘ inj₂))


-- Dependent functions with partitioned set domains

Π* : (X : PSet) (M : X →* Set l) → Set l
Π* (pset none tt) M = ⊤
Π* (pset (one name) (v E)) (v M) = One name ((x : E) → M x)
Π* (pset (P + Q) (E , F)) (M , N) = Π* (pset P E) M × Π* (pset Q F) N

Λ* : {M : X →* Set l} → ((x : ⟦ X ⟧*) → M ◃* x) → Π* X M
Λ* {X = pset none tt} f = tt
Λ* {X = pset (one n) E} f = n ↦ λ x → f (tt , x)
Λ* {X = pset (P + Q) (E , F)} f = Λ* (f ∘ inj₁) , Λ* (f ∘ inj₂)

_◁*_ : {M : X →* Set l} → (Π* X M) → (x : ⟦ X ⟧*) → M ◃* x
_◁*_ {X = pset (one n) (v E)} (v f) (tt , e) = f e
_◁*_ {X = pset (P + Q) (E , F)} (f , g) (inj₁ x) = f ◁* x
_◁*_ {X = pset (P + Q) (E , F)} (f , g) (inj₂ x) = g ◁* x

Beta* : {U : X →* Set l} → (f : ((x : ⟦ X ⟧*) → U ◃* x)) → (a : ⟦ X ⟧*) → Λ* f ◁* a ≡ f a
Beta* {X = pset (one _) E} f (tt , e) = refl
Beta* {X = pset (A + B) E} f (inj₁ x) = Beta* (f ∘ inj₁) x
Beta* {X = pset (A + B) E} f (inj₂ x) = Beta* (f ∘ inj₂) x

Eta* : {U : X →* Set l} → (f : Π* X U) → f ≡ Λ* λ x → f ◁* x
Eta* {X = pset none E} tt = refl
Eta* {X = pset (one _) E} x = refl
Eta* {X = pset (A + B) E} (f , g) = ≡/, (Eta* f) (Eta* g)

-- Ext* requries DepFunExt
DepFunExt : (l l' : Level) → Set (lsuc l ⊔ lsuc l')
DepFunExt l l' = {A : Set l} {B : A → Set l'} {f g : (x : A) → B x} → (∀ a → f a ≡ g a) → f ≡ g

Ext* : DepFunExt lzero l → {U : X →* Set l} → (f g : (x : ⟦ X ⟧*) → U ◃* x) → (eq : ∀ x → f x ≡ g x) → Λ* f ≡ Λ* g
Ext* {X = pset none E} FE f g eq = refl
Ext* {X = pset (one _) (v E)} FE f g eq = ≡/v (FE λ x → eq _)
Ext* {X = pset (A + B) E} FE f g eq =
  ≡/, (Ext* FE (f ∘ inj₁) (g ∘ inj₁) (eq ∘ inj₁))
      (Ext* FE (f ∘ inj₂) (g ∘ inj₂) (eq ∘ inj₂))

-- Finitary W-types

data W° (Sh : Set) (Pl : Sh → Fin) : Set where
  sup : (sh : Sh) → (Pl sh →° W° Sh Pl) → W° Sh Pl


elim° : ∀ {Sh Pl} (R : W° Sh Pl → Set) →
  (F : (sh : Sh) →
       (sub : Pl sh →° W° Sh Pl) →
       (subR : Π° (Pl sh) (λ° λ p → R (sub ◃° p))) →
       R (sup sh sub)) →
  (x : W° Sh Pl) → R x
elim° {Sh} {Pl} R F (sup sh t) = F sh t (IH t)
  where
    IH : ∀ {Ps} → (t : Ps →° W° Sh Pl) →
         Π° Ps (λ° (λ p → R (t ◃° p)))
    IH {none} t = tt
    IH {one n} (v t) = n ↦ elim° R F t
    IH {Ps₁ + Ps₂} (t₁ , t₂) = IH t₁ , IH t₂


-- Infinitary partitioned W-types

data W* (Sh : Set) (Pl : Sh → PSet) : Set where
  sup : (sh : Sh) → (Pl sh →* W* Sh Pl) → W* Sh Pl

elim* : ∀ {Sh Pl} (R : W* Sh Pl → Set) →
  (F : (sh : Sh) →
       (sub : (Pl sh) →* W* Sh Pl) →
       (subR : Π* (Pl sh) (λ* λ p → R (sub ◃* p))) →
       R (sup sh sub)) →
  (x : W* Sh Pl) → R x
elim* {Sh} {Pl} R F (sup sh t) = F sh t (IH t)
  where
    IH : ∀ {Ps} → (t : Ps →* W* Sh Pl) →
         Π* Ps (λ* (λ p → R (t ◃* p)))
    IH {pset none Es} t = tt
    IH {pset (one n) Es} (v t) = n ↦ λ e → elim* R F (t e)
    IH {pset (Ps₁ + Ps₂) Es} (t₁ , t₂) = IH t₁ , IH t₂

-- Example of a finitary W-type

cases : {B : ⟦ A ⟧ → Set l} → (Π° A (λ° B)) → (a : ⟦ A ⟧) → B a
cases f a = transp (beta° _ a) (f ◁° a)

Nat = W°
  ⟦ one "zero" + one "succ" ⟧
  (cases
   ("zero" ↦ none ,
    "succ" ↦ one "x"))

zero : Nat
zero = sup (⟨"zero"⟩) tt

succ : Nat → Nat
succ x = sup (⟨"succ"⟩) ("x" ↦ x)

nat-ind :
  (R : Nat → Set)
  (Pzero : R zero)
  (Psucc : ∀ n → R n → R (succ n)) →
  ∀ x → R x
nat-ind R Pzero Psucc =
  elim° R (cases (
    "zero" ↦ (λ _ _ → Pzero) ,
    "succ" ↦ λ { (v x) (v Rx) → Psucc x Rx }))
--  λ { (inj₁ tt) _ _ → Pzero ;
--      (inj₂ tt) (v x) (v Rx) → Psucc x Rx }

nat-ind-zero :
  ∀ { R Pzero Psucc } → nat-ind R Pzero Psucc zero ≡ Pzero
nat-ind-zero = refl

nat-ind-succ :
  ∀ { R Pzero Psucc x } → nat-ind R Pzero Psucc (succ x) ≡ Psucc x (nat-ind R Pzero Psucc x)
nat-ind-succ = refl


-- An an infinitary one (Brouwer ordinal trees)

Ord = W*
  ⟦ one "zero" + one "succ" + one "lim" ⟧
  ( cases
   ("zero" ↦ pset none tt ,
    "succ" ↦ pset (one "x") ("x" ↦ ⊤) ,
    "lim" ↦ pset (one "f") ("f" ↦ Nat)))

ozero : Ord
ozero = sup (⟨"zero"⟩) tt

osucc : Ord → Ord
osucc x = sup (⟨"succ"⟩) ("x" ↦ λ _ → x)

olim : (Nat → Ord) → Ord
olim f = sup (⟨"lim"⟩) ("f" ↦ f)

ord-ind :
  (R : Ord → Set)
  (Pzero : R ozero)
  (Psucc : ∀ n → R n → R (osucc n))
  (Plim : ∀ f → (∀ n → R (f n)) → R (olim f)) →
  ∀ x → R x
ord-ind R Pzero Psucc Plim =
  elim* R (cases (
    "zero" ↦ (λ _ _ → Pzero) ,
    "succ" ↦ (λ { (v x) (v Rx) → Psucc (x tt) (Rx tt) }) ,
    "lim" ↦ (λ { (v f) (v Rf) → Plim f Rf })))

ord-ind-zero :
  ∀ { R Pzero Psucc Plim } → ord-ind R Pzero Psucc Plim ozero ≡ Pzero
ord-ind-zero = refl

ord-ind-succ :
  ∀ { R Pzero Psucc Plim x } → ord-ind R Pzero Psucc Plim (osucc x) ≡ Psucc x (ord-ind R Pzero Psucc Plim x)
ord-ind-succ = refl

ord-ind-lim :
  ∀ { R Pzero Psucc Plim f } → ord-ind R Pzero Psucc Plim (olim f) ≡ Plim f (λ n → ord-ind R Pzero Psucc Plim (f n))
ord-ind-lim = refl