recN-exercise

gistfile1.txt

-- Challenge: https://github.com/effectfully/random-stuff/blob/master/RecN-challenge.agda
{-# OPTIONS --type-in-type #-}

open import Agda.Primitive
open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma
open import Agda.Builtin.List

ℕ = Nat

data _≡_ {l : Level} {A : Set l} : A → A → Set where
  refl : ∀ {x : A} → x ≡ x

coerce : ∀ {l} {A B : Set l} -> A ≡ B -> A -> B
coerce refl x = x

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

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

    rec0-correct
      : (λ {R} -> coerce Rec0-correct (recN zero) {R})
      ≡ λ k f -> f
    rec1-correct
      : (λ {A R : Set} -> coerce Rec1-correct (recN 1) {A} {R})
      ≡ λ k f -> f (k λ x -> x)
    rec2-correct
      : (λ {A B R : Set} -> 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 : Set} -> 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)

CurriedFunction : List Set → Set → Set
CurriedFunction [] R = R
CurriedFunction (A ∷ rest) R = A → CurriedFunction rest R

curried-const : ∀ {args : List Set} → {R : Set} (x : R) → CurriedFunction args R
curried-const {[]} x = x
curried-const {(_ ∷ args)} x = λ _ → curried-const x

KTuple = λ (args : List Set) → (∀ {Q : Set} -> (CurriedFunction args Q) -> Q)

khead : ∀ {A args} → KTuple (A ∷ args) → A
khead k = k (λ x → curried-const x)

ktail : ∀ {A args} → KTuple (A ∷ args) → KTuple args
ktail k = (λ qf → k (λ _ → qf))

apply-curried-function : ∀ {R : Set} → (args : List Set) → (f : CurriedFunction args R) → (k : KTuple args) → R
apply-curried-function [] f k = f
apply-curried-function (A ∷ args) f k = apply-curried-function args (f (khead k)) (ktail k)

Object = Σ Set (λ A → A)

obj : ∀ {T : Set} (x : T) → Object
obj {T} x = T , x

typ : Object → Set
typ (T , _) = T

val : ∀ o → typ o
val (_ , x) = x

--  WithTypes 3 f = obj (λ {A} {B} {C} → val (f (A ∷ B ∷ C ∷ [])))
WithTypes : (n : ℕ) → (List Set → Object) → Object
WithTypes zero f = f []
WithTypes (suc n) f = obj (λ {A} → val (WithTypes n (λ v → f (A ∷ v))))

recN-obj : ℕ → Object
recN-obj = λ n → WithTypes n (λ args → obj (λ { R } →
    (λ (k : KTuple args) (f : (CurriedFunction args R)) → apply-curried-function _ f k)))

kitRecN = record {
  RecN = _;
  recN = λ n → val (recN-obj n);
  Rec0-correct = refl;
  Rec1-correct = refl;
  Rec2-correct = refl;
  Rec3-correct = refl;
  rec0-correct = refl;
  rec1-correct = refl;
  rec2-correct = refl;
  rec3-correct = refl
  }