Skip to content

Instantly share code, notes, and snippets.

@larrytheliquid
Last active May 13, 2018 15:52
Show Gist options
  • Save larrytheliquid/7938611 to your computer and use it in GitHub Desktop.
Save larrytheliquid/7938611 to your computer and use it in GitHub Desktop.
Labelled types demo ala "The view from the left" by McBride & McKinna. Labels are a cheap alternative to dependent pattern matching. You can program with eliminators but the type of your goal reflects the dependent pattern match equation that you would have done. Inductive hypotheses are also labeled, and hence you get more type safety from usin…
open import Data.Nat
open import Data.String
open import Function
open import LabelledTypes
module LabelledAdd1 where
----------------------------------------------------------------------
add : (m n : ℕ) → ⟨ "add" ∙ m ∙ n ∙ ε ∶ ℕ ⟩
add m n = elimℕ (λ m' → ⟨ "add" ∙ m' ∙ n ∙ ε ∶ ℕ ⟩)
(return n) -- Goal 1
(λ m' ih → return (suc (call ih))) -- Goal 2
m
{-
Goal 1: ⟨ "add" ∙ 0 ∙ n ∙ ε ∶ ℕ ⟩
————————————————————————————————————————————————————————————
n : ℕ
m : ℕ
Goal 2: ⟨ "add" ∙ suc m' ∙ n ∙ ε ∶ ℕ ⟩
————————————————————————————————————————————————————————————
ih : ⟨ "add" ∙ m' ∙ n ∙ ε ∶ ℕ ⟩
m' : ℕ
n : ℕ
m : ℕ
-}
----------------------------------------------------------------------
open import Data.Nat
open import Data.String
open import Function
open import LabelledTypes
module LabelledAdd2 where
----------------------------------------------------------------------
Add : (m n : ℕ) → Set
Add m n = ⟨ "add" ∙ m ∙ n ∙ ε ∶ ℕ ⟩
add : (m n : ℕ) → Add m n
add m = elimℕ (Add m)
(return zero) -- Goal 1
(λ n ih → return (suc (call ih))) -- Goal 2
{-
Goal 1: ⟨ "add" ∙ m ∙ 0 ∙ ε ∶ ℕ ⟩
————————————————————————————————————————————————————————————
m : ℕ
Goal 2: ⟨ "add" ∙ m ∙ suc n ∙ ε ∶ ℕ ⟩
————————————————————————————————————————————————————————————
ih : ⟨ "add" ∙ m ∙ n ∙ ε ∶ ℕ ⟩
n : ℕ
m : ℕ
-}
----------------------------------------------------------------------
{-# OPTIONS --type-in-type #-}
open import Data.Nat
open import Data.String
open import Function
module LabelledTypes where
----------------------------------------------------------------------
elimℕ : (P : ℕ → Set)
(pz : P zero)
(ps : (m : ℕ) → P m → P (suc m))
(n : ℕ)
→ P n
elimℕ P pz ps zero = pz
elimℕ P pz ps (suc n) = ps n (elimℕ P pz ps n)
----------------------------------------------------------------------
infixr 4 _∙_
data Spine : Set where
ε : Spine
_∙_ : {A : Set} → A → Spine → Spine
data Label : Set where
_∙_ : String → Spine → Label
data ⟨_∶_⟩ : Label → Set → Set where
return : ∀{l A} → A → ⟨ l ∶ A ⟩
call : {l : Label} {A : Set} → ⟨ l ∶ A ⟩ → A
call (return a) = a
----------------------------------------------------------------------
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment