Last active
September 5, 2017 11:29
-
-
Save mbrcknl/c629596bf7763f42bb81 to your computer and use it in GitHub Desktop.
Code from BFPG talk about dependent types in Agda
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 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 ◇ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
With my insincerest apologies for the excessive Unicode.