{-# OPTIONS --allow-unsolved-metas #-}
module A201602.Church where
open import Data.Product using (Σ ; _,_ ; proj₁ ; proj₂ ; _×_)
open import Data.Sum using (_⊎_ ; inj₁ ; inj₂)
module Rank₀ where
List : Set → Set → Set
List A B = (A → B → B) → B → B
nil : ∀{A B} → List A B
nil = λ f y₀ → y₀
cons : ∀{A B} → A → List A B → List A B
cons x xs = λ f y₀ → f x (xs f y₀)
it : ∀{A B} → List A B → (A → B → B) → B → B
it xs f y₀ = xs f y₀
rec : ∀{A B C} → List A (List A C × B) → (A → List A C → B → B) → B → B
rec xs f y₀ = proj₂ (it xs (λ xᵢ pᵢ → cons xᵢ (proj₁ pᵢ) , f xᵢ (proj₁ pᵢ) (proj₂ pᵢ)) (nil , y₀))
tail : ∀{A B} → List A (List A B × List A B) → List A B
tail xs = rec xs (λ xᵢ xsᵢ yᵢ → xsᵢ) nil
data Empty : Set where
empty : Empty
head : ∀{A} → List A (A ⊎ Empty) → A ⊎ Empty
head xs = it xs (λ xᵢ xsᵢ → inj₁ xᵢ) (inj₂ empty)
module Rank₁ where
List : Set → Set₁
List A = ∀{T} → (A → T → T) → T → T
nil : ∀{A} → List A
nil = λ f y₀ → y₀
cons : ∀{A} → A → List A → List A
cons x xs = λ f y₀ → f x (xs f y₀)
it : ∀{A B} → List A → (A → B → B) → B → B
it xs f y₀ = xs f y₀
rec : ∀{A B} → List A → (A → List A → B → B) → B → B
rec {A} {B} xs f y₀ = proj₂ (it {A} {{!List A!} × B} xs (λ xᵢ pᵢ → cons xᵢ {!proj₁ pᵢ!} , f xᵢ {!proj₁ pᵢ!} (proj₂ pᵢ)) ((nil , y₀)))
module WTF where
data List (A : Set) : Set where
nil : List A
cons : A → List A → List A