Typing Rules for Quotient Polymorphism

Typing Rules for Quotient Polymorphism BRANDON HEWER, University of Nottingham, United Kingdom GRAHAM HUTTON, University of Nottingham, United Kingdom This document supplements the “Quotient Polymorphism” paper by providing the full set of typing rules for the core language λQ, including support for choice polymorphism for quotient types. Key Context: Γ,∆,ΣSubstitution: θMonotype: τ,τ′,τk,τ′ kPolytype: σ,σ′,σk,σ′ k Type variable: α,β,αk,βkVariable: xTerm: e,e′,ekRefinement: Φ,Ψ Equality constructor: ε,ε’ Quotient Set: Q,Q’ Quotient: QConstant: c Quotient variable: qPatterns: ρ,ρ′,ρkQualifier Set: QRespect. Theorem: ψ Set of Respect. Theorems: ϕ Well-Formed 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:σ′ Authors’ Contact Information: Brandon Hewer, University of Nottingham, Nottingham, United Kingdom, Brandon.Hewer1@ nottingham.ac.uk; Graham Hutton, University of Nottingham, Nottingham, United Kingdom, graham.hutton@nottingham. ac.uk. 2 Brandon Hewer and Graham Hutton x:{v:τ|Φ} ∈ Γ[LT-VAR] Γ⊢Qx:{v:τ|v=x} x:τ∈Γ[LT-VAR] Γ⊢Qx:τ [LT-CONST] Γ⊢Qc:ty(c) Γ,x:τ⊢Qe:τ′Γ⊢ (x:τ) → τ′ [LT-FUN] Γ⊢Qλx.e:(x:τ) → τ′ Γ|=(x:τ/Q) → τ′Γ⊢Qρi:τΓ;vars(ρi) ⊢Qei:τ′[x7→ ρi] Γ⊢σ⊑τ∀i∈ {1, . . . , n}Γ⊢QϕΓ|=ϕ⇒λ{ρ→e}{Q:: σ ρ1, . . . , ρnis a complete case analysis of τValid(JΓK⇒JϕK)[LT-CASE] Γ⊢Qλ{ρ1→e1;. . .;ρn→en}:(x:τ/Q) → τ′ Γ⊢Qf:(x:τ) → τ′Γ⊢ (x:τ) → τ′ [LT-APP] Γ⊢Qλx.e:(x:τ) → τ′ Γ⊢Qb:Bool Γ⊢Qe:τΓ⊢Qe′:τΓ⊢τ[LT-IF] Γ⊢Qif bthen eelse e′:τ Γ⊢Qe:σΓ,x:σ⊢Qe′:τΓ⊢τ[LT-LET] Γ⊢Qlet x=ein e′:τ Γ,x:τ⊢Qe:τΓ,x:σ⊢Qe′:τ′Γ⊢σ⊑τ[LT-LETREC] Γ⊢Qlet rec x=ein e′:τ′ Γ⊢Qe:σ α not free in Γ [LT-GEN] Γ⊢Qe:∀α.σ Γ⊢τΓ,q:: τ⊢Qe:τ′qis not free in Γ [LT-CHOOSE] Γ⊢Qe:choose q:τ.τ′ Γ⊢Qe:choose q:σ2.σ3Γ⊢QQ:: σ1Γ⊢σ1⊑σ2 Γ|=ϕ⇒ (e::qσ3)respects (Q:: σ2)Valid (JΓK⇒JϕK)[LT-CINST] Γ⊢Qe:τ′[q7→ Q] Subtyping Γ⊢σ<:σ′ Valid (JΓK∧JΦK⇒JΨK)[ST-BASE] Γ⊢ { x:τ|Φ}<:{x:τ|Ψ} Typing Rules for Quotient Polymorphism 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.σ′ Equality constructor subtyping Γ;∆;Σ⊢ε<:ε′ Γ,∆⊢Qρ,e:τΓ,Σ⊢Qρ′,e′:τ ρ ⊆θρ′ Valid (J∆K⇒JΣ[θ]K)Valid (JeK=Je′[θ]K)[EST-BASE] Γ;∆;Σ|=(ρ== e)<:(ρ′== e′) Γ;∆,v:τ;Σ⊢Qε<:ε′ [EST-LEFT] Γ;∆;Σ⊢Q(forall v:τin ε)<:ε′ Γ;∆;Σ,v:τ⊢Qε<:ε′ [EST-RIGHT] Γ;∆;Σ⊢Qε<:(forall v:τin ε′) Specialisation Γ⊢σ⊑σ′ Γ⊢σ<:σ′[SP-SUB] Γ⊢σ⊑σ′ τ′=τ[αi7→ τi]βinot free in ∀α1. . . αn.τ[ST-POLY] Γ⊢ ∀α1. . . αn.τ⊑ ∀β1. . . βm.τ′ Well-Formed Respectfulness Theorems Γ⊢Qϕ Γ⊢σΓ⊢Qci:Bool Γ⊢Qli:σΓ⊢Qri:σ∀i∈ {1, . . . , n} Γ⊢Q{(cj,lj,rj) | j∈ {1, . . . , n}} 4 Brandon Hewer and Graham Hutton Well-Formed Equality Constructors Γ;∆⊢Qε:: τ Γ;∆,v:τ′⊢Qε:: τ[EC-BIND] Γ;∆⊢Qforall v:τ′in ε:: τ Γ,∆⊢Qρ:τΓ,∆⊢Qe:τ[EC-BASE] Γ;∆⊢Qρ== e:: τ Well-Formed Quotients Γ⊢QQ:: σ Γ;∅ ⊢Qεi:: τiΓ⊢σ⊑τi∀i∈ {1, . . . , n}[QT-BASE] Γ⊢Q{εi|i∈ {1, . . . , n}} :: σ Γ⊢QQ:: σ α free in Γ [QT-POLY] Γ⊢QQ:: ∀α.σ q:: σ∈Γ[QT-VAR] Γ⊢Qq:: σ Equality Constructor Respectfulness Γ;∆|=ϕ⇒λ{ρ→e}{ε:: τ Γ,∆⊢Qρ′:τΓ,∆⊢Qe′:τ∃i∈ {1, . . . , n}.ρi∼θρ′ [RP-BASE] Γ;∆|=(J∆[θ]K,ei[θ],λ{ρ1→e1;. . . ;ρn→en}e′[θ]) ⇒ λ{ρ→e}{(ρ′== e′):: τ Γ⊢QϕΓ;∆,v:τ′|=ϕ⇒ (ρ→e){ε:: τ[RP-BIND] Γ;∆|=ϕ⇒λ{ρ→e}{(forall v:τ′in ε):: τ Quotient Respectfulness Γ|=ϕ⇒λ{ρ→e}{Q:: τ Γ⊢QQ:: σΓ⊢σ⊑τ∀i∈ {1, . . . , n} Γ;∅ |=ψi⇒λ{ρ→e}{εi:: τ[RP-QUOT] Γ|={ψj|j∈ {1, . . . , n} } ⇒ λ{ρ→e}{Q:: σ Polymorphic Respectfulness Γ;∆|=ϕ⇒ (e::qσ)respects (ε:: σ′) Γ⊢QϕΓ;∆,x:τ1|=ϕ⇒ (e::qτ2)respects (ε:: τ3)[PR-BIND] Γ;∆|=ϕ⇒ (e::qτ2)respects (forall x:τ1in ε:: τ3) [PR-CONST] Γ;∆|=∅ ⇒ (c::qty(c)) respects (ρ== e:: σ) x:σ∈Γ [PR-VAR] Γ;∆|=∅ ⇒ (x::qσ)respects (ρ== e:: σ′) Typing Rules for Quotient Polymorphism 5 Γ⊢σ⊑τ∀i∈ {1, . . . , n}Γ⊢Qρi:τ/qΓ⊢Qϕ′Γ⊢Qϕi Γ;∆|=ϕ′⇒λ{ρ→e}{ρ== e:: σ Γ,vars(ρi);∆|=ϕi⇒ (ei::qτ′[x7→ ρi]) respects (ρ== e:: σ)[PR-CASE] Γ;∆|=(Ð i JτK∗ϕi) ∪ ϕ′⇒ (λ{ρi→ei}::q(x:τ/q) → τ′)respects (ρ== e:: σ) Γ⊢σ⊑τ∀i∈ {1, . . . , n}Γ⊢Qρi:τ/QΓ⊢QϕiQ,q Γ,vars(ρi);∆|=ϕi⇒ (ei::qτ′[x7→ ρi]) respects (ρ== e:: σ)[PR-NCASE] Γ;∆|=Ð i JτK∗ϕi⇒ (λ{ρi→ei}::q(x:τ/Q) → τ′)respects (ρ== e:: σ) Γ⊢QϕΓ,x:τ;∆|=ϕ⇒ (e::qτ′)respects (ρ== e:: σ)[PR-FUN] Γ;∆|=JτK∗ϕ⇒ (λx.e::q(x:τ) → τ′)respects (ρ== e:: σ) Γ⊢QϕΓ;∆|=ϕ⇒ (f::q(x:τ) → τ′)respects (ρ== e:: σ) Γ⊢Qϕ′Γ;∆|=ψ⇒ (e::qτ)respects (ρ== e:: σ)[PR-APP] Γ;∆|=ϕe∪fϕ′⇒ (f e ::qτ′[x7→ e]) respects (ρ== e:: σ) Γ⊢Qb:Bool Γ⊢QϕΓ⊢Qϕ′ Γ;∆|=ϕ⇒ (e1::qτ)respects (ρ== e′:: σ) Γ;∆|=ϕ′⇒ (e2::qτ)respects (ρ== e′:: σ)[PR-IF] Γ;∆|=JbK∗ϕ∪ ¬JbK∗ψ⇒ (if bthen e1else e2::qτ)respects (ρ== e′:: σ) Γ⊢QϕΓ,x:σ;∆|=ϕ⇒ (e′::qτ)respects (ρ== e:: σ)[PR-LET] Γ;∆|=ϕ[x7→ e]⇒(let x=ein e′::qτ)respects (ρ== e:: σ) Γ⊢QϕΓ,x:σ;∆|=ϕ⇒ (e′::qτ)respects (ρ== e:: σ)[PR-LETREC] Γ;∆|=ϕ[x7→ e]⇒(let rec x=ein e′::qτ)respects (ρ== e:: σ) Polymorphic Quotient Respectfulness Γ|=ϕ⇒ (e::qσ)respects (Q:: σ′) r:: σ2∈Γ Γ ⊢σ2⊑σ′ 2[PR-QVAR] Γ|=∅ ⇒ (e::qσ1)respects (r:: σ′ 2) Γ⊢QϕiΓ;∅ |=ϕi⇒ (e::qσ)respects (εi:: τ) ∀ i∈ {1, . . . , n}[PR-QUOT] Γ|=Ð i ϕi⇒ (e::qσ)respects ({ εi|i∈ {1, . . . , n} } :: σ′)