Typing Rules o Quo ien Polymo phism
BRANDON HEWER, Uni e si y o No ingham, Uni ed Kingdom
GRAHAM HUTTON, Uni e si y o No ingham, Uni ed Kingdom
This documen supplemen s he “Quo ien Polymo phism” pape by p o iding he ull se o yping ules o
he co e language λQ, including suppo o choice polymo phism o quo ien ypes.
Key
Con ex : Γ,∆,ΣSubs i u ion: θMono ype: τ,τ′,τk,τ′
kPoly ype: σ,σ′,σk,σ′
k
Type a iable: α,β,αk,βkVa iable: xTe m: e,e′,ekRe inemen : Φ,Ψ
Equali y cons uc o : ε,ε’ Quo ien Se : Q,Q’ Quo ien : QCons an : c
Quo ien a iable: qPa e ns: ρ,ρ′,ρkQuali ie Se : QRespec . Theo em: ψ
Se o Respec . Theo ems: ϕ
Well-Fo med Types Γ⊢σ
Γ,x:τ⊢ϕ:Bool [WT-BASE]
Γ⊢ {x:τ|ϕ}
[WT-VAR]
Γ⊢α
Γ,x:τ⊢τ′
[WT-FUN]
Γ⊢ (x:τ) → τ′
Γ⊢σ[WT-POLY]
Γ⊢ ∀ α.σ
Γ⊢τΓ⊢QQ:: σΓ⊢σ⊑τ[WT-QUOT]
Γ⊢τ/Q
Γ,q:: τ⊢σ[WT-CHOOSE]
Γ⊢choose q:τ.σ
Liquid Type Checking Γ⊢Qe:σ
Γ⊢Qe:σΓ⊢σ⊑σ′Γ⊢σ′
[LT-SUB]
Γ⊢Qe:σ′
Au ho s’ Con ac In o ma ion: B andon Hewe , Uni e si y o No ingham, No ingham, Uni ed Kingdom, B andon.Hewe 1@
no ingham.ac.uk; G aham Hu on, Uni e si y o No ingham, No ingham, Uni ed Kingdom, g aham.hu on@no ingham.
ac.uk.
2 B andon Hewe and G aham Hu on
x:{ :τ|Φ} ∈ Γ[LT-VAR]
Γ⊢Qx:{ :τ| =x}
x:τ∈Γ[LT-VAR]
Γ⊢Qx:τ
[LT-CONST]
Γ⊢Qc: y(c)
Γ,x:τ⊢Qe:τ′Γ⊢ (x:τ) → τ′
[LT-FUN]
Γ⊢Qλx.e:(x:τ) → τ′
Γ|=(x:τ/Q) → τ′Γ⊢Qρi:τΓ; a s(ρi) ⊢Qei:τ′[x7→ ρi]
Γ⊢σ⊑τ∀i∈ {1, . . . , n}Γ⊢QϕΓ|=ϕ⇒λ{ρ→e}{Q:: σ
ρ1, . . . , ρnis a comple e case analysis o τValid(JΓK⇒JϕK)[LT-CASE]
Γ⊢Qλ{ρ1→e1;. . .;ρn→en}:(x:τ/Q) → τ′
Γ⊢Q :(x:τ) → τ′Γ⊢ (x:τ) → τ′
[LT-APP]
Γ⊢Qλx.e:(x:τ) → τ′
Γ⊢Qb:Bool Γ⊢Qe:τΓ⊢Qe′:τΓ⊢τ[LT-IF]
Γ⊢Qi b hen eelse e′:τ
Γ⊢Qe:σΓ,x:σ⊢Qe′:τΓ⊢τ[LT-LET]
Γ⊢Qle x=ein e′:τ
Γ,x:τ⊢Qe:τΓ,x:σ⊢Qe′:τ′Γ⊢σ⊑τ[LT-LETREC]
Γ⊢Qle ec x=ein e′:τ′
Γ⊢Qe:σ α no ee in Γ
[LT-GEN]
Γ⊢Qe:∀α.σ
Γ⊢τΓ,q:: τ⊢Qe:τ′qis no ee in Γ
[LT-CHOOSE]
Γ⊢Qe:choose q:τ.τ′
Γ⊢Qe:choose q:σ2.σ3Γ⊢QQ:: σ1Γ⊢σ1⊑σ2
Γ|=ϕ⇒ (e::qσ3) espec s (Q:: σ2)Valid (JΓK⇒JϕK)[LT-CINST]
Γ⊢Qe:τ′[q7→ Q]
Sub yping Γ⊢σ<:σ′
Valid (JΓK∧JΦK⇒JΨK)[ST-BASE]
Γ⊢ { x:τ|Φ}<:{x:τ|Ψ}
Typing Rules o Quo ien Polymo phism 3
Γ⊢τ2<:τ1Γ,x:τ2⊢τ′
1<:τ′
2[ST-FUN]
Γ⊢ (x:τ1) → τ′
1<:(x:τ2) → τ′
2
[ST-VAR]
Γ⊢α<:α
Γ⊢σ<:σ′[ST-POLY]
Γ⊢ ∀α.σ<:∀α.σ′
[ST-QBASE]
Γ⊢τ<:τ/Q
Γ⊢τ<:τ′[ST-QUOTY]
Γ⊢τ/Q<:τ′/Q
Γ;∅;∅ ⊢ Q<:Q′
[ST-QUOT]
Γ⊢τ/Q<:τ/Q′
Γ,q:: σ1⊢σ<:σ′Γ⊢σ2⊑σ1[ST-CHOOSE]
Γ⊢choose q:σ1.σ<:choose q:σ2.σ′
Equali y cons uc o sub yping Γ;∆;Σ⊢ε<:ε′
Γ,∆⊢Qρ,e:τΓ,Σ⊢Qρ′,e′:τ ρ ⊆θρ′
Valid (J∆K⇒JΣ[θ]K)Valid (JeK=Je′[θ]K)[EST-BASE]
Γ;∆;Σ|=(ρ== e)<:(ρ′== e′)
Γ;∆, :τ;Σ⊢Qε<:ε′
[EST-LEFT]
Γ;∆;Σ⊢Q( o all :τin ε)<:ε′
Γ;∆;Σ, :τ⊢Qε<:ε′
[EST-RIGHT]
Γ;∆;Σ⊢Qε<:( o all :τin ε′)
Specialisa ion Γ⊢σ⊑σ′
Γ⊢σ<:σ′[SP-SUB]
Γ⊢σ⊑σ′
τ′=τ[αi7→ τi]βino ee in ∀α1. . . αn.τ[ST-POLY]
Γ⊢ ∀α1. . . αn.τ⊑ ∀β1. . . βm.τ′
Well-Fo med Respec ulness Theo ems Γ⊢Qϕ
Γ⊢σΓ⊢Qci:Bool Γ⊢Qli:σΓ⊢Q i:σ∀i∈ {1, . . . , n}
Γ⊢Q{(cj,lj, j) | j∈ {1, . . . , n}}
4 B andon Hewe and G aham Hu on
Well-Fo med Equali y Cons uc o s Γ;∆⊢Qε:: τ
Γ;∆, :τ′⊢Qε:: τ[EC-BIND]
Γ;∆⊢Q o all :τ′in ε:: τ
Γ,∆⊢Qρ:τΓ,∆⊢Qe:τ[EC-BASE]
Γ;∆⊢Qρ== e:: τ
Well-Fo med Quo ien s Γ⊢QQ:: σ
Γ;∅ ⊢Qεi:: τiΓ⊢σ⊑τi∀i∈ {1, . . . , n}[QT-BASE]
Γ⊢Q{εi|i∈ {1, . . . , n}} :: σ
Γ⊢QQ:: σ α ee in Γ
[QT-POLY]
Γ⊢QQ:: ∀α.σ
q:: σ∈Γ[QT-VAR]
Γ⊢Qq:: σ
Equali y Cons uc o Respec ulness Γ;∆|=ϕ⇒λ{ρ→e}{ε:: τ
Γ,∆⊢Qρ′:τΓ,∆⊢Qe′:τ∃i∈ {1, . . . , n}.ρi∼θρ′
[RP-BASE]
Γ;∆|=(J∆[θ]K,ei[θ],λ{ρ1→e1;. . . ;ρn→en}e′[θ]) ⇒ λ{ρ→e}{(ρ′== e′):: τ
Γ⊢QϕΓ;∆, :τ′|=ϕ⇒ (ρ→e){ε:: τ[RP-BIND]
Γ;∆|=ϕ⇒λ{ρ→e}{( o all :τ′in ε):: τ
Quo ien Respec ulness Γ|=ϕ⇒λ{ρ→e}{Q:: τ
Γ⊢QQ:: σΓ⊢σ⊑τ∀i∈ {1, . . . , n}
Γ;∅ |=ψi⇒λ{ρ→e}{εi:: τ[RP-QUOT]
Γ|={ψj|j∈ {1, . . . , n} } ⇒ λ{ρ→e}{Q:: σ
Polymo phic Respec ulness Γ;∆|=ϕ⇒ (e::qσ) espec s (ε:: σ′)
Γ⊢QϕΓ;∆,x:τ1|=ϕ⇒ (e::qτ2) espec s (ε:: τ3)[PR-BIND]
Γ;∆|=ϕ⇒ (e::qτ2) espec s ( o all x:τ1in ε:: τ3)
[PR-CONST]
Γ;∆|=∅ ⇒ (c::q y(c)) espec s (ρ== e:: σ)
x:σ∈Γ
[PR-VAR]
Γ;∆|=∅ ⇒ (x::qσ) espec s (ρ== e:: σ′)
Typing Rules o Quo ien Polymo phism 5
Γ⊢σ⊑τ∀i∈ {1, . . . , n}Γ⊢Qρi:τ/qΓ⊢Qϕ′Γ⊢Qϕi
Γ;∆|=ϕ′⇒λ{ρ→e}{ρ== e:: σ
Γ, a s(ρi);∆|=ϕi⇒ (ei::qτ′[x7→ ρi]) espec s (ρ== e:: σ)[PR-CASE]
Γ;∆|=(Ð
i
JτK∗ϕi) ∪ ϕ′⇒ (λ{ρi→ei}::q(x:τ/q) → τ′) espec s (ρ== e:: σ)
Γ⊢σ⊑τ∀i∈ {1, . . . , n}Γ⊢Qρi:τ/QΓ⊢QϕiQ,q
Γ, a s(ρi);∆|=ϕi⇒ (ei::qτ′[x7→ ρi]) espec s (ρ== e:: σ)[PR-NCASE]
Γ;∆|=Ð
i
JτK∗ϕi⇒ (λ{ρi→ei}::q(x:τ/Q) → τ′) espec s (ρ== e:: σ)
Γ⊢QϕΓ,x:τ;∆|=ϕ⇒ (e::qτ′) espec s (ρ== e:: σ)[PR-FUN]
Γ;∆|=JτK∗ϕ⇒ (λx.e::q(x:τ) → τ′) espec s (ρ== e:: σ)
Γ⊢QϕΓ;∆|=ϕ⇒ ( ::q(x:τ) → τ′) espec s (ρ== e:: σ)
Γ⊢Qϕ′Γ;∆|=ψ⇒ (e::qτ) espec s (ρ== e:: σ)[PR-APP]
Γ;∆|=ϕe∪ ϕ′⇒ ( e ::qτ′[x7→ e]) espec s (ρ== e:: σ)
Γ⊢Qb:Bool Γ⊢QϕΓ⊢Qϕ′
Γ;∆|=ϕ⇒ (e1::qτ) espec s (ρ== e′:: σ)
Γ;∆|=ϕ′⇒ (e2::qτ) espec s (ρ== e′:: σ)[PR-IF]
Γ;∆|=JbK∗ϕ∪ ¬JbK∗ψ⇒ (i b hen e1else e2::qτ) espec s (ρ== e′:: σ)
Γ⊢QϕΓ,x:σ;∆|=ϕ⇒ (e′::qτ) espec s (ρ== e:: σ)[PR-LET]
Γ;∆|=ϕ[x7→ e]⇒(le x=ein e′::qτ) espec s (ρ== e:: σ)
Γ⊢QϕΓ,x:σ;∆|=ϕ⇒ (e′::qτ) espec s (ρ== e:: σ)[PR-LETREC]
Γ;∆|=ϕ[x7→ e]⇒(le ec x=ein e′::qτ) espec s (ρ== e:: σ)
Polymo phic Quo ien Respec ulness Γ|=ϕ⇒ (e::qσ) espec s (Q:: σ′)
:: σ2∈Γ Γ ⊢σ2⊑σ′
2[PR-QVAR]
Γ|=∅ ⇒ (e::qσ1) espec s ( :: σ′
2)
Γ⊢QϕiΓ;∅ |=ϕi⇒ (e::qσ) espec s (εi:: τ) ∀ i∈ {1, . . . , n}[PR-QUOT]
Γ|=Ð
i
ϕi⇒ (e::qσ) espec s ({ εi|i∈ {1, . . . , n} } :: σ′)
