Skip to content

Instantly share code, notes, and snippets.

@bobatkey
Created August 25, 2020 14:39
Show Gist options
  • Save bobatkey/72397ea77f047ab7296d17684032723e to your computer and use it in GitHub Desktop.
Save bobatkey/72397ea77f047ab7296d17684032723e to your computer and use it in GitHub Desktop.
A start on formalisation of STLC + type synonyms and newtype
module localdefs where
mutual
data ty-ctx : Set where
ε : ty-ctx
_,-_ : (Δ : ty-ctx) → defn Δ → ty-ctx
data defn : ty-ctx → Set where
synonym : ∀ {Δ} → ty Δ → defn Δ
newtype : ∀ {Δ} → ty Δ → defn Δ
data ty : ty-ctx → Set where
wk : ∀ {Δ τ} → ty Δ → ty (Δ ,- τ)
defd : ∀ {Δ τ} → ty (Δ ,- τ)
bit : ∀ {Δ} → ty Δ
_⇒_ : ∀ {Δ} → ty Δ → ty Δ → ty Δ
infixl 10 _,-_
data _≅ty_ : ∀ {Δ} → ty Δ → ty Δ → Set where
expand : ∀ {Δ τ} →
defd{Δ}{synonym τ} ≅ty wk τ
wk-bit : ∀ {Δ τ} → wk{Δ}{τ} bit ≅ty bit
wk-⇒ : ∀ {Δ τ σ₁ σ₂} → wk{Δ}{τ} (σ₁ ⇒ σ₂) ≅ty (wk{Δ}{τ} σ₁ ⇒ wk σ₂)
cong-wk : ∀ {Δ τ σ₁ σ₂} → σ₁ ≅ty σ₂ → wk{Δ}{τ} σ₁ ≅ty wk{Δ}{τ} σ₂
cong-⇒ : ∀ {Δ}{σ₁ σ₁' σ₂ σ₂' : ty Δ} → σ₁ ≅ty σ₂ → σ₁' ≅ty σ₂' → (σ₁ ⇒ σ₁') ≅ty (σ₂ ⇒ σ₂')
≅ty-refl : ∀ {Δ}{τ : ty Δ} → τ ≅ty τ
≅ty-trans : ∀ {Δ}{τ₁ τ₂ τ₃ : ty Δ} →
τ₁ ≅ty τ₂ → τ₂ ≅ty τ₃ → τ₁ ≅ty τ₃
≅ty-symm : ∀ {Δ}{τ₁ τ₂ : ty Δ} →
τ₁ ≅ty τ₂ →
τ₂ ≅ty τ₁
-- looking up newtypes
data _⊢tydef_≡_ : (Δ : ty-ctx) → ty Δ → ty Δ → Set where
zero : ∀ {Δ τ} → (Δ ,- newtype τ) ⊢tydef defd ≡ wk τ
suc : ∀ {Δ τ x σ} → Δ ⊢tydef x ≡ τ → (Δ ,- σ) ⊢tydef wk x ≡ wk τ
-- typing contexts
data ctx (Δ : ty-ctx) : Set where
ε : ctx Δ
_,-_ : ctx Δ → ty Δ → ctx Δ
data _/_⊢v_ : (Δ : ty-ctx) → ctx Δ → ty Δ → Set where
zero : ∀ {Δ Γ τ} → Δ / Γ ,- τ ⊢v τ
suc : ∀ {Δ Γ τ σ} → Δ / Γ ⊢v τ → Δ / Γ ,- σ ⊢v τ
data _/_⊢_ : (Δ : ty-ctx) → ctx Δ → ty Δ → Set where
`_ : ∀ {Δ Γ τ} →
Δ / Γ ⊢v τ →
Δ / Γ ⊢ τ
ƛ : ∀ {Δ Γ σ τ} →
Δ / Γ ,- σ ⊢ τ →
Δ / Γ ⊢ (σ ⇒ τ)
_·_ : ∀ {Δ Γ σ τ} →
Δ / Γ ⊢ (σ ⇒ τ) →
Δ / Γ ⊢ σ →
Δ / Γ ⊢ τ
`0 `1 : ∀ {Δ Γ} →
Δ / Γ ⊢ bit
mk : ∀ {Δ Γ τ σ} →
Δ ⊢tydef τ ≡ σ →
Δ / Γ ⊢ σ →
Δ / Γ ⊢ τ
proj : ∀ {Δ Γ τ σ} →
Δ ⊢tydef τ ≡ σ →
Δ / Γ ⊢ τ →
Δ / Γ ⊢ σ
conv : ∀ {Δ Γ τ₁ τ₂} →
τ₁ ≅ty τ₂ →
Δ / Γ ⊢ τ₁ →
Δ / Γ ⊢ τ₂
------------------------------------------------------------------------------
-- A context that is like the Haskell:
--
-- newtype A = A Bit
-- type B = Bit
Δ : ty-ctx
Δ = ε ,- newtype bit ,- synonym bit
-- type synonyms are resolved by expanding definitions within the
-- 'conv' rule.
synonym-seethrough : Δ / ε ⊢ (defd ⇒ bit)
synonym-seethrough = ƛ (conv (≅ty-trans expand wk-bit) (` zero))
-- newtypes need explicit 'proj' constructors to be inserted.
newtype-not-seethrough : Δ / ε ⊢ (wk defd ⇒ bit)
newtype-not-seethrough = ƛ (conv (≅ty-trans (cong-wk wk-bit) wk-bit) (proj (suc zero) (` zero)))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment