RecN-solution.agda

{-# OPTIONS --type-in-type #-}  -- Just for convenience, not essential.

open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Nat.Base

coerce : ∀ {A B} -> A ≡ B -> A -> B
coerce refl = id

record KitRecN : Set where
  field
    RecN : ℕ -> Set
    recN : ∀ n -> RecN n

    Rec0-correct
      : RecN 0
      ≡ ∀ {R} -> (∀ {Q} -> Q -> Q) -> R -> R
    Rec1-correct
      : RecN 1
      ≡ ∀ {A R} -> (∀ {Q} -> (A -> Q) -> Q) -> (A -> R) -> R
    Rec2-correct
      : RecN 2
      ≡ ∀ {A B R} -> (∀ {Q} -> (A -> B -> Q) -> Q) -> (A -> B -> R) -> R
    Rec3-correct
      : RecN 3
      ≡ ∀ {A B C R} -> (∀ {Q} -> (A -> B -> C -> Q) -> Q) -> (A -> B -> C -> R) -> R

    rec0-correct
      : (λ {R} -> coerce Rec0-correct (recN 0) {R})
      ≡ λ k f -> f
    rec1-correct
      : (λ {A R} -> coerce Rec1-correct (recN 1) {A} {R})
      ≡ λ k f -> f (k λ x -> x)
    rec2-correct
      : (λ {A B R} -> coerce Rec2-correct (recN 2) {A} {B} {R})
      ≡ λ k f -> f (k λ x y -> x) (k λ x y -> y)
    rec3-correct
      : (λ {A B C R} -> coerce Rec3-correct (recN 3) {A} {B} {C} {R})
      ≡ λ k f -> f (k λ x y z -> x) (k λ x y z -> y) (k λ x y z -> z)

RecPattern : (Set -> Set) -> Set
RecPattern F = ∀ {R} -> (∀ {Q} -> F Q -> Q) -> F R -> R

RecOver : ((Set -> Set) -> Set) -> ℕ -> Set
RecOver K  0      = K id
RecOver K (suc n) = ∀ {A} -> RecOver (λ F -> K λ X -> A -> F X) n

RecN : ℕ -> Set
RecN = RecOver RecPattern

Bump : ((Set -> Set) -> Set) -> Set
Bump K
    = ∀ {F A}
    -> (∀ {Q} -> F Q -> F (A -> Q))
    -> (∀ {R} -> F (A -> R) -> A -> F R)
    -> F (A -> A)
    -> K F
    -> K λ X -> F (A -> X)

recOver : ∀ {K} n -> Bump K -> K id -> RecOver K n
recOver  0      bump z = z
recOver (suc n) bump z = recOver n
  (λ skip keep last -> bump (λ g y -> skip (g y)) (λ g x y -> keep (g y) x) (λ _ -> last))
  (bump const _$_ id z)

bumpRecPattern : Bump RecPattern
bumpRecPattern skip keep last r k f = r (k ∘ skip) (keep f $ k last)

recN : ∀ n -> RecN n
recN n = recOver n bumpRecPattern (λ _ f -> f)

kitRecN : KitRecN
kitRecN = record
  { RecN = RecN
  ; recN = recN
  ; Rec0-correct = refl
  ; Rec1-correct = refl
  ; Rec2-correct = refl
  ; Rec3-correct = refl
  ; rec0-correct = refl
  ; rec1-correct = refl
  ; rec2-correct = refl
  ; rec3-correct = refl
  }