```{-# OPTIONS --guardedness-preserving-type-constructors #-}
module Talk where
{-

Eliminating Data

Thorsten Altenkirch
University of Nottingham

AIM XV
-}

{-
My goal is to demonstrate how "data" in Agda can be replaced by a fixed collection
of datatype constructors. This is very much inspired by ΠΣ, see our FLOPS 2010 paper:
http://www.cs.nott.ac.uk/~txa/publ/pisigma-new.pdf
-}

open import Coinduction
open import Data.Sum
open import Data.Unit

{- Using coinduction we can define ℕ by a recursive definition. -}

ℕ : Set
ℕ = ⊤ ⊎ Rec (♯ ℕ)

{- The constructors are derivable.-}

zero : ℕ
zero = inj₁ _

suc : ℕ → ℕ
suc n = inj₂ (fold n)

{- We can define _+_ almost as usual. Ok pattern abbrevation would be helpful here. -}

_+_ : ℕ → ℕ → ℕ
inj₁ tt + n = n
inj₂ (fold x) + n = suc (x + n)

{- One may think that this is unsound
because we can define.
-}

{-
D : Set
D = Rec (♯ D) → Rec (♯ D)
-}

{- However the termination checker colours this red
because → is only guardedness preserving in the 2nd argument.
This way we enforce strict positivity.
-}

open import Data.Product
open import Relation.Binary.PropositionalEquality

{- Using equality we can encode inductive families. -}

Vec : (A : Set) → ℕ → Set
Vec A n = (n ≡ zero)
⊎ Σ ℕ (λ m → Σ (n ≡ suc m) λ _ → Σ A λ _ → Rec (♯ (Vec A m)))

{- This doesn't work with products just now because the termination
checker doesn't unfold definitions.
Could this be fixed.
-}
--Vec A n = (n ≡ zero) ⊎ Σ ℕ (λ m → (n ≡ suc m) × A × Rec (♯ (Vec A m)))

vnil : {A : Set} → Vec A zero
vnil {A} = inj₁ refl

vcons : {A : Set}{n : ℕ} → A → Vec A n → Vec A (suc n)
vcons {A} {n} a as = inj₂ (n , refl , a , fold as)

Fin : ℕ → Set
Fin n = Σ ℕ (λ m → (n ≡ suc m)) ⊎ Σ ℕ (λ m → Σ (n ≡ suc m) λ _ →  (Rec (♯ (Fin m))))
--Fin n = Σ ℕ (λ m → (n ≡ suc m)) ⊎ Σ ℕ (λ m → (n ≡ suc m) × (Rec (♯ (Fin m))))

vzero : ∀ {m} → Fin (suc m)
vzero {m} = inj₁ (m , refl)

vsuc : ∀ {m} → Fin m → Fin (suc m)
vsuc {m} i = inj₂ (m , (refl , (fold i)))

{-
_!!_ : ∀ {n}{A} → Vec A n → Fin n → A
-- exercise.
-}

{- We can also encode inductive-recursive definitions.
Indeed, induction-recursion is now just recursion-recursion.
-}

U : Set
El : U → Set

U = ⊤ ⊎ Σ (Rec (♯ U)) (λ a → El (unfold a) → Rec (♯ U))

El (inj₁ _) = ℕ
El (inj₂ (a , b)) = (x : El (unfold a)) → El (unfold (b x))

{-
This shows that we can reduce data types to a core theory with
⊤ , ⊥ , Bool, Σ , → , ∞, ≡, Rec
We don't need pattern matching -> use eliminators.
+ guarded mutual recursive definition

Can we also eliminate the recursion?
possible answer: inductive-recursive codes ala Dybjer+Setzer
(but this seems weaker.)
-}```