{-# 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.) -}