gistfile1.hs

{-
Andrew Miller - RegTree.agda
An attempt at translating "Exploring the Regular Tree Types" from Epigram
http://strictlypositive.org/regular.pdf
-}


module RegTree where

open import Data.Product
open import Data.Sum
open import Data.Fin
open import Data.Unit
open import Data.Empty
open import Data.Nat

data Code : ℕ → Set₁ where
  E : ∀ {n} → Code n          -- Empty
  U : ∀ {n} → Code n          -- Unit
  K : ∀ {n} → Set → Code n    -- Constant K
  _⊗_ : ∀ {n} → Code n → Code n → Code n
  _⊕_ : ∀ {n} → Code n → Code n → Code n
  Wk  : ∀ {n} → Code n → Code (suc n)
  Z   : ∀ {n} → Code (suc n)    -- Identity
  Let : ∀ {n} → Code n → Code (suc n) → Code n


data Tel : ℕ → Set₁ where
  ε : Tel zero
  _::_ : ∀ {n} → Tel n → Code n → Tel (suc n)


⟦_⟧ : ∀ {n} → Code n → Tel n → Set
⟦ E       ⟧ Γ = ⊥
⟦ U       ⟧ Γ = ⊤
⟦ K A     ⟧ Γ = A
⟦ F ⊗ G   ⟧ Γ = ⟦ F ⟧ Γ × ⟦ G ⟧ Γ
⟦ F ⊕ G   ⟧ Γ = ⟦ F ⟧ Γ ⊎ ⟦ G ⟧ Γ
⟦ Wk T    ⟧ (Γ :: _) = ⟦ T ⟧ Γ
⟦ Z       ⟧ (Γ :: T) = ⟦ T ⟧ Γ
⟦ Let S T ⟧ Γ = ⟦ T ⟧ (Γ :: S)