README (7288B)
1 System QFω ("quantified system Fω") is a substructural lambda calculus that 2 tracks data flow with "quantities" from a "quantity algebra". Unlike previous 3 systems that only annotate binders with quantities (e.g., Quantitative Type 4 Theory), which require CPSed code to place restrictions on the return values 5 of functions, System QFω can naturally track data flow both in and out of a 6 function. And unlike systems with graded modal types (e.g., Bounded Linear 7 Logic, Granule), which require a linear core language (?) (and hence suffer 8 from ergonomic problems), System QFω makes quantities and types "independent", 9 so we can, for example, simply choose to only work with an unrestricted 10 quantity (like in normal functional programming), yet without having to deal 11 with the "boxing" and "unboxing" of graded modal types. 12 13 14 TODO: Explain the economic interpretation of programs, and connect it to the 15 sequent calculus. 16 17 18 -------------------------------------------------------------------------------- 19 Quantity algebras 20 21 See Algebra.hs. 22 23 TODO: Give a better explanation. 24 25 26 -------------------------------------------------------------------------------- 27 Grammar (parameterized by a quantity algebra) 28 29 This is not exactly the concrete syntax accepted by the implementation. The 30 point of this presentation is merely to present the rules. 31 32 33 Quantity ∋ q,r 34 35 Kinds ∋ k,l ::= $ (quantities) 36 | * (proper types) 37 | $* (pairs of a quantity and a proper type) 38 | k => k (type-level functions) 39 40 Types ∋ T,U,Q,R,Z ::= X (type variable) 41 | T :: k (kind annotation) 42 | q (canonical quantity) 43 | T + T (quantity sum) 44 | T ⋅ T (quantity multiply) 45 | T -> T (function type) 46 | ∀X::k. T (forall type) 47 | T ! T (pair) 48 | T.$ (pair left projection) 49 | T.* (pair right projection) 50 | λX. T (type-level function abstraction) 51 | T T (type-level function application) 52 53 Terms ∋ t,u ::= x (term variable) 54 | t : T (type annotation) 55 | λx. t (term-level function abstraction) 56 | t t (term-level function application) 57 | ΛX. t (forall abstraction) 58 | t [T] (forall application) 59 60 Type contexts ∋ Θ ::= ⋄ 61 | Θ, X::k 62 63 Term contexts ∋ Γ ::= ⋄ 64 | Γ, x:T 65 66 Ledgers ∋ Σ ::= ⋄ 67 | Σ, x~Q 68 69 70 TODO: Explain ledgers 71 72 73 In the kinding and typing rules, we adopt the convention that type contexts Θ 74 and term contexts Γ are unordered and omit mention of the standard side 75 conditions regarding variable freshness. 76 77 78 -------------------------------------------------------------------------------- 79 Kinding rules 80 81 We define the judgement forms "Θ ⊢ T ↓ k" and "Θ ⊢ T ↑ k", respectively meaning 82 "type T checks against kind k in type context Θ" and "we infer kind k for type 83 T in type context Θ". Both Θ and T are always inputs, but k is an input to the 84 former and output of the latter. 85 86 87 X::k ∈ Θ 88 ---------- 89 Θ ⊢ X ↑ k 90 91 Θ ⊢ T ↓ k 92 -------------- 93 Θ ⊢ T :: k ↑ k 94 95 ---------- 96 Θ ⊢ q ↑ $ 97 98 Θ ⊢ q ↓ $ Θ ⊢ r ↓ $ 99 --------------------- 100 Θ ⊢ q + r ↑ $ 101 102 Θ ⊢ q ↓ $ Θ ⊢ r ↓ $ 103 --------------------- 104 Θ ⊢ q ⋅ r ↑ $ 105 106 Θ ⊢ T ↓ $* Θ ⊢ U ↓ $* 107 ----------------------- 108 Θ ⊢ T -> U ↑ * 109 110 Θ, X::k ⊢ T ↓ $* 111 ---------------- 112 Θ ⊢ ∀X::k. T ↑ * 113 114 Θ ⊢ Q ↓ $ Θ ⊢ T ↓ * 115 --------------------- 116 Θ ⊢ Q ! T ↑ $* 117 118 Θ ⊢ Z ↓ $* 119 ----------- 120 Θ ⊢ Z.$ ↑ $ 121 122 Θ ⊢ Z ↓ $* 123 ----------- 124 Θ ⊢ Z.* ↑ * 125 126 Θ, X::k ⊢ Τ ↓ l 127 ------------------ 128 Θ ⊢ λX. T ↓ k => l 129 130 Θ ⊢ T ↑ k => l Θ ⊢ U ↓ k 131 -------------------------- 132 Θ ⊢ T U ↑ l 133 134 135 -------------------------------------------------------------------------------- 136 Typing rules 137 138 We define the judgement forms "Θ; Γ ⊢ t ~ Q ↓ T ⊣ Σ" and "Θ; Γ ⊢ t ~ Q ↑ T ⊣ Σ", 139 respectively meaning "term t checks against type T with demand Q in type 140 context Θ and term context Γ, resulting in demands Σ on (a subset of) the 141 variables in Γ" and "we infer type T for term t with demand Q type context Θ 142 and term context Γ, resulting in demands Σ on (a subset of) the variables in 143 Γ". All of Θ, Γ, t, and Q are always inputs and Σ is always an output, but T 144 is an input to the former and and output of the latter. 145 146 147 x:T ∈ Γ 148 ---------------------- 149 Θ; Γ ⊢ x ~ Q ↑ T ⊣ x~Q 150 151 Θ; Γ ⊢ t ~ Q ↓ T ⊣ Σ 152 ------------------------ 153 Θ; Γ ⊢ t : T ~ Q ↑ T ⊣ Σ 154 155 Θ; Γ, x:U.* ⊢ t ~ T.$ ↓ T.* ⊣ Σ, x~R ⊢ T.$ >= R 156 ------------------------------------------------- 157 Θ; Γ ⊢ λx. t ~ Q ↓ U -> T ⊣ Q ⋅ Σ 158 159 Θ; Γ ⊢ t ~ 1 ↑ U -> T ⊣ Σ0 Θ; Γ ⊢ u ~ U.$ ↓ U.* ⊣ Σ1 ⊢ T.$ >= Q 160 ------------------------------------------------------------------- 161 Θ; Γ ⊢ t u ~ Q ↑ T ⊣ Σ0 + Σ1 162 163 Θ, X::k; Γ ⊢ t ~ T.$ ↓ T.* ⊣ Σ 164 ----------------------------------- 165 Θ; Γ ⊢ ΛX. t ~ Q ↓ ∀X::k. T ⊣ Q ⋅ Σ 166 167 Θ; Γ ⊢ t ~ 1 ↑ ∀X::k. T ⊣ Σ Θ ⊢ U ↓ k ⊢ T.$ >= Q 168 ---------------------------------------------------- 169 Θ; Γ ⊢ t [U] ~ Q ↑ T.*[U/X] ⊣ Σ 170 171 172 TODO: Discuss rules 173 174 175 The auxiliary judgement "⊢ Q >= R" means "the quantity Q (viewed as a supply) 176 is greater than the quantity R (viewed as a demand)". We should at least have 177 the rule 178 179 -------- 180 ⊢ q >= r 181 182 whenever q >= r in the quantity algebra, but in principle more rules can be 183 added depending on chosen quantity algebra. For example, if the quantity 184 algebra is a singleton (so that we have normal System Fω), we can adopt the 185 rule 186 187 -------- 188 ⊢ Q >= R 189 190 (where we emphasize that Q and R are arbitrary types of kind $, meaning they 191 could be neutral). 192 193 194 -------------------------------------------------------------------------------- 195 Inductive types 196 197 At this point, we only have arrow and forall types to work with. That's enough 198 to Church-encode inductive types like nats, lists, and trees, but the derived 199 elimination rules for these types are oblivious of the fact that only one 200 case will apply, so the quantity tracking is needlessly conservative. 201 202 For example, take 203 Nat := ∀M::$*. Q0 ! (M -> Q1 ! (Q2 ! (M -> M) -> M)) 204 Here, the motive M has kind $* instead of the usual *, so we get to pick the 205 continuation quantity when we eliminate a Nat. Technically, we need to decide 206 on quantities Q0, Q1, and Q2, but they're noise for now, so let's remove them: 207 Nat := ∀M::$*. M -> (M -> M) -> M 208 The problem mentioned above is that, given n:Nat, the elimination n [M] z s 209 has to "pay" for "resources" used by both z and s, even though only one will 210 apply. 211 212 To get a tighter, more intuitive accounting of quantities for inductive types, 213 we need to build them in as primitives and add a LUB operation to quantity 214 algebras. 215 216 TODO: Type up the rules for inductive types.