Skip to content

Instantly share code, notes, and snippets.

@LightAndLight

LightAndLight/zippery typeclass elaboration

Created February 10, 2020 23:22
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save LightAndLight/518d6c505dd6cf0375648b945d69d057 to your computer and use it in GitHub Desktop.
Save LightAndLight/518d6c505dd6cf0375648b945d69d057 to your computer and use it in GitHub Desktop.
Download ZIP
typeclasses in typechecking-in-context style?
Raw
zippery typeclass elaboration
x : ∀α₀, α₁, …, αₘ. (C₀, C₁, …, Cₙ) ⇒ τ
————–—————————————————————————————–————————————————————————————————————————————————————————————————————————————————–
(Θ ↓ x) ↦ (Θ, α₀ : *, α₁ : *, …, αₘ : *, ev₀ : C₀, ev₁ : C₁, …, evₙ : Cₙ ↑ x α₀ α₁ … αₘ ev₀ ev₁ … evₙ : τ)
—————————————————————————————————————————————————–
(Θ ↓ let x = v in e) ↦ (Θ, [let x = ⋄ in e] ↓ v)
solveConstraints(θ, Ξ) ↦ Ξ' gen(Ξ', τ) ↦ σ
—————————————————————————————————————————————————————————————
(Θ, [let x = ⋄ in e], Ξ ↑ v : τ) ↦ (θ, [let x : σ = v in ⋄] ↓ e)
solveConstraints(Θ, []) ↦ []
solveConstraints(Θ, (Ξ, ev := d)) ↦ solveConstraints(Θ, Ξ), ev := d
solveConstraints(Θ, (Ξ, ev : C)) ↦
solveConstraints(Θ, Ξ), ev := d if d : (Θ, Ξ) ⊩ C
solveConstraints(Θ, Ξ), ev : C otherwise
gen([], τ) ↦ τ
gen((Θ, α := x), τ) ↦ gen(Θ, τ[α:=x])
gen((Θ, α : *), τ) ↦ gen(Θ, ∀α. τ)
gen((Θ, ev := d), τ) ↦ gen(Θ, τ)
gen((Θ, ev : C), τ) ↦ gen(Θ, C ⇒ τ)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment