Code from BFPG talk about dependent types in Agda

after.agda

-- Matthew Brecknell @mbrcknl
-- BFPG.org, March-April 2015

-- With thanks to Conor McBride (@pigworker) for his lecture series:
-- https://www.youtube.com/playlist?list=PL44F162A8B8CB7C87
-- from which I learned most of what I know about Agda, and
-- from which I stole several ideas for this talk.

open import Agda.Primitive using (_⊔_)

postulate
  String : Set

{-# BUILTIN STRING String #-}

-- data Bool = True | False

data bool : Set where
  tt : bool
  ff : bool

if_then_else_ : ∀ {ℓ} {T : bool → Set ℓ}
  → (b : bool) → T tt → T ff → T b
if tt then x else y = x
if ff then x else y = y

ex₀ : bool → String
ex₀ tt = "hi"
ex₀ ff = "bye"

-- data Nat = Zero | Succ Nat

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

_plus_ : ℕ → ℕ → ℕ
zero plus n = n
succ m plus n = succ (m plus n)

ex₁ : ℕ
ex₁ = 2 plus 3

-- data List α = Nil | Cons α (List α)

data [_] (α : Set) : Set where
  ◇ : [ α ]
  _,_ : α → [ α ] → [ α ]

infixr 6 _,_

_++_ : ∀ {α} → [ α ] → [ α ] → [ α ]
◇ ++ ys = ys
(x , xs) ++ ys = x , (xs ++ ys)

ex₂ : [ ℕ ]
ex₂ = (0 , 1 , 2 , ◇) ++ (3 , 4 , ◇)

data _≡_ {α : Set} (x : α) : α → Set where
  refl : x ≡ x

-- {-# BUILTIN EQUALITY _≡_ #-}
-- {-# BUILTIN REFL refl #-}

data One : Set where
  ◇ : One

data Zero : Set where

ex₃ : (2 plus 3) ≡ 5
ex₃ = refl

ex₄ : 0 ≡ 1 → Zero
ex₄ ()

cong : ∀ {α β : Set} {x y : α} (f : α → β) → x ≡ y → f x ≡ f y
cong {x = x} {y = .x} _ refl = refl

ex₅ : ∀ n → (n plus 0) ≡ n
ex₅ zero = refl
ex₅ (succ n) = cong succ (ex₅ n)

--
-- Sigma types
--

-- data Either a b = Left a | Right b

data _+_ (α β : Set) : Set where
  «_ : α → α + β
  »_ : β → α + β

ex₆ ex₇ : String + ℕ
ex₆ = « "hi"
ex₇ = » 42

record Σ (I : Set) (V : I → Set) : Set where
  constructor _,_
  field
    fst : I
    snd : V fst

data Σ′ (I : Set) (V : I → Set) : Set where
  _,_ : ∀ (fst : I) → V fst → Σ′ I V

_∨_ : Set → Set → Set
α ∨ β = Σ bool (λ b → if b then α else β)

tosum : ∀ {α β : Set} → α + β → α ∨ β
tosum (« x) = tt , x
tosum (» x) = ff , x

unsum : ∀ {α β : Set} → α ∨ β → α + β
unsum (tt , snd) = « snd
unsum (ff , snd) = » snd

tosum∘unsum : ∀ {α β : Set} (p : α ∨ β) → (tosum (unsum p)) ≡ p
tosum∘unsum (tt , snd) = refl
tosum∘unsum (ff , snd) = refl

unsum∘tosum : ∀ {α β : Set} (p : α + β) → (unsum (tosum p)) ≡ p
unsum∘tosum (« x) = refl
unsum∘tosum (» x) = refl

--
-- Pi types
--

record _×′_ (α β : Set) : Set where
  constructor _,_
  field
    fst : α
    snd : β

_×_ : Set → Set → Set
α × β = Σ α (λ _ → β)

ex₈ : String × ℕ
ex₈ = "hi" , 42

∏ : (A : Set) → (A → Set) → Set
∏ I V = (i : I) → V i

_∧_ : Set → Set → Set
α ∧ β = (b : bool) → if b then α else β

_,,_ : ∀ {α β : Set} → α → β → α ∧ β
_,,_ x y tt = x
_,,_ x y ff = y

ex₉ : String ∧ ℕ
ex₉ = "hi" ,, 99

tofun : ∀ {α β : Set} → α × β → α ∧ β
tofun (fst , snd) = fst ,, snd

defun : ∀ {α β : Set} → α ∧ β → α × β
defun f = f tt , f ff

tofun∘defun : ∀ {α β : Set} (p : α ∧ β) (b : bool) → tofun (defun p) b ≡ p b
tofun∘defun p tt = refl
tofun∘defun p ff = refl

defun∘tofun : ∀ {α β : Set} (p : α × β) → defun (tofun p) ≡ p
defun∘tofun p = refl

--
-- Heterogeneous lists
--

data _∈_ {α : Set} (x : α) : [ α ] → Set where
  zero : ∀ {xs} → x ∈ (x , xs)
  succ : ∀ {y xs} → x ∈ xs → x ∈ (y , xs)

exₐ : 0 ∈ (0 , 1 , 2 , ◇)
exₐ = zero

exₑ : 2 ∈ (0 , 1 , 2 , ◇)
exₑ = succ (succ zero)

exᵢ : 3 ∈ (0 , 1 , 2 , ◇) → Zero
exᵢ (succ (succ (succ ())))

data [_⊣_] {I : Set} (V : I → Set) : [ I ] → Set where
  ◇ : [ V ⊣ ◇ ]
  _,_ : ∀ {i is} → V i → [ V ⊣ is ] → [ V ⊣ i , is ]

exⱼ : [ (λ b → if b then ℕ else String) ⊣ ff , tt , ff , ◇ ]
exⱼ = "hi" , 42 , "bye" , ◇

_!_ : ∀ {I : Set} {V : I → Set} {i is} → [ V ⊣ is ] → i ∈ is → V i
(x , xs) ! zero = x
(x , xs) ! succ i = xs ! i

exᵣ : ℕ
exᵣ = exⱼ ! succ zero

--
-- STLC
--

data Type : Set where
  ι   : Type
  _▷_ : Type → Type → Type

⟨_⟩ : Type → Set
⟨ ι ⟩ = ℕ
⟨ S ▷ T ⟩ = ⟨ S ⟩ → ⟨ T ⟩

data _⊢_ (Γ : [ Type ]) : Type → Set where
  lam : ∀ {S T} → (S , Γ) ⊢ T → Γ ⊢ (S ▷ T)
  _$_ : ∀ {S T} → Γ ⊢ (S ▷ T) → Γ ⊢ S → Γ ⊢ T
  var : ∀ {T} → T ∈ Γ → Γ ⊢ T

twice : ∀ {Γ : [ Type ]} {T : Type} → Γ ⊢ ((T ▷ T) ▷ (T ▷ T))
twice = lam (lam (var (succ zero) $ (var (succ zero) $ var zero)))

⟪_⊢_⟫ : ∀ {Γ : [ Type ]} {T : Type} → [ ⟨_⟩ ⊣ Γ ] → Γ ⊢ T → ⟨ T ⟩
⟪ γ ⊢ lam d ⟫ = λ s → ⟪ s , γ ⊢ d ⟫
⟪ γ ⊢ f $ x ⟫ = ⟪ γ ⊢ f ⟫ ⟪ γ ⊢ x ⟫
⟪ γ ⊢ var i ⟫ = γ ! i

twice' : ∀ {T : Type} → let D = ⟨ T ⟩ in (D → D) → D → D
twice' = ⟪ ◇ ⊢ twice ⟫

---
--- PHOAS
---

-- See http://adam.chlipala.net/cpdt/

data _⊨_ (V : Type → Set) : Type → Set where
  lam : ∀ {S T} → (V S → V ⊨ T) → V ⊨ (S ▷ T)
  _$_ : ∀ {S T} → V ⊨ (S ▷ T) → V ⊨ S → V ⊨ T
  var : ∀ {T} → V T → V ⊨ T

thrice : ∀ {V : Type → Set} {T : Type} → V ⊨ ((T ▷ T) ▷ (T ▷ T))
thrice = lam (λ f → lam (λ x → var f $ (var f $ (var f $ var x))))

⟪_⟫ : ∀ {T : Type} → ⟨_⟩ ⊨ T → ⟨ T ⟩
⟪ lam d ⟫ = λ s → ⟪ d s ⟫
⟪ f $ x ⟫ = ⟪ f ⟫ ⟪ x ⟫
⟪ var i ⟫ = i

thrice' : ∀ {T : Type} → let D = ⟨ T ⟩ in (D → D) → D → D
thrice' = ⟪ thrice ⟫

-- Unfinished, not yet sure if I'm on the right track here.

_⇓_ : [ Type ] → Type → Set₁
◇ ⇓ T = ∀ V → V ⊨ T
(S , Γ) ⇓ T = {!!}

lower : ∀ Γ {T} → Γ ⇓ T → Γ ⊢ T
lower Γ {T} t = {!!}

↓ : ∀ {T} → (∀ V → V ⊨ T) → ◇ ⊢ T
↓ = lower ◇