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