commit f682629dcc43bd18f055b659041e5625ddeae326
parent d9f8021abfe73b38a5de9e93cc2bf5152baf5098
Author: Robert Russell <robert@rr3.xyz>
Date: Thu, 29 Aug 2024 04:53:15 -0700
Add README
WIP
Diffstat:
| A | README | | | 206 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
1 file changed, 206 insertions(+), 0 deletions(-)
diff --git a/README b/README
@@ -0,0 +1,206 @@
+System QFω ("quantified system Fω") is a substructural lambda calculus that
+tracks data flow with "quantities" from a "quantity algebra". Unlike previous
+systems that only annotate binders with quantities (e.g., Quantitative Type
+Theory), which require CPSed code to place restrictions on the return values
+of functions, System QFω can naturally track data flow both in and out of a
+function. And unlike systems with graded modal types (e.g., Bounded Linear
+Logic, Granule), which require a linear core language (?) (and hence suffer
+from ergonomic problems), System QFω makes quantities and types "independent",
+so we can, for example, simply choose to only work with an unrestricted
+quantity (like in normal functional programming), yet without having to deal
+with the "boxing" and "unboxing" of graded modal types.
+
+
+--------------------------------------------------------------------------------
+Quantity algebras
+
+See Algebra.hs.
+
+TODO: Give a better explanation.
+
+
+--------------------------------------------------------------------------------
+Grammar (parameterized by a quantity algebra)
+
+This is not exactly the concrete syntax accepted by the implementation. The
+point of this presentation is merely to present the rules.
+
+
+Quantity ∋ q,r
+
+Kinds ∋ k,l ::= $ (quantities)
+ | * (proper types)
+ | $* (pairs of a quantity and a proper type)
+ | k => k (type-level functions)
+
+Types ∋ T,U,Q,R,Z ::= X (type variable)
+ | T :: k (kind annotation)
+ | q (canonical quantity)
+ | T + T (quantity sum)
+ | T ⋅ T (quantity multiply)
+ | T -> T (function type)
+ | ∀X::k. T (forall type)
+ | T ! T (pair)
+ | T.$ (pair left projection)
+ | T.* (pair right projection)
+ | λX. T (type-level function abstraction)
+ | T T (type-level function application)
+
+Terms ∋ t,u ::= x (term variable)
+ | t : T (type annotation)
+ | λx. t (term-level function abstraction)
+ | t t (term-level function application)
+ | ΛX. t (forall abstraction)
+ | t [T] (forall application)
+
+Type contexts ∋ Θ ::= ⋄
+ | Θ, X::k
+
+Term contexts ∋ Γ ::= ⋄
+ | Γ, x:T
+
+Ledgers ∋ Σ ::= ⋄
+ | Σ, x~Q
+
+
+In the kinding and typing rules, we adopt the convention that type contexts Θ
+and term contexts Γ are unordered and omit mention of the standard side
+conditions regarding variable freshness.
+
+
+--------------------------------------------------------------------------------
+Kinding rules
+
+We define the judgement forms "Θ ⊢ T ↓ k" and "Θ ⊢ T ↑ k", respectively meaning
+"type T checks against kind k in type context Θ" and "we infer kind k for type
+T in type context Θ". Both Θ and T are always inputs, but k is an input to the
+former and output of the latter.
+
+
+X::k ∈ Θ
+----------
+Θ ⊢ X ↑ k
+
+Θ ⊢ T ↓ k
+--------------
+Θ ⊢ T :: k ↑ k
+
+----------
+Θ ⊢ q ↑ $
+
+Θ ⊢ q ↓ $ Θ ⊢ r ↓ $
+---------------------
+Θ ⊢ q + r ↑ $
+
+Θ ⊢ q ↓ $ Θ ⊢ r ↓ $
+---------------------
+Θ ⊢ q ⋅ r ↑ $
+
+Θ ⊢ T ↓ $* Θ ⊢ U ↓ $*
+-----------------------
+Θ ⊢ T -> U ↑ *
+
+Θ, X::k ⊢ T ↓ $*
+----------------
+Θ ⊢ ∀X::k. T ↑ *
+
+Θ ⊢ Q ↓ $ Θ ⊢ T ↓ *
+---------------------
+Θ ⊢ Q ! T ↑ $*
+
+Θ ⊢ Z ↓ $*
+-----------
+Θ ⊢ Z.$ ↑ $
+
+Θ ⊢ Z ↓ $*
+-----------
+Θ ⊢ Z.* ↑ *
+
+Θ, X::k ⊢ Τ ↓ l
+------------------
+Θ ⊢ λX. T ↓ k => l
+
+Θ ⊢ T ↑ k => l Θ ⊢ U ↓ k
+--------------------------
+Θ ⊢ T U ↑ l
+
+
+--------------------------------------------------------------------------------
+Typing rules
+
+We define the judgement forms "Θ; Γ ⊢ t ~ Q ↓ T ⊣ Σ" and "Θ; Γ ⊢ t ~ Q ↑ T ⊣ Σ",
+respectively meaning "term t checks against type T with demand Q in type
+context Θ and term context Γ, resulting in demands Σ on (a subset of) the
+variables in Γ" and "we infer type T for term t with demand Q type context Θ
+and term context Γ, resulting in demands Σ on (a subset of) the variables in
+Γ". All of Θ, Γ, t, and Q are always inputs and Σ is always an output, but T
+is an input to the former and and output of the latter.
+
+
+x:T ∈ Γ
+----------------------
+Θ; Γ ⊢ x ~ Q ↑ T ⊣ x~Q
+
+Θ; Γ ⊢ t ~ Q ↓ T ⊣ Σ
+------------------------
+Θ; Γ ⊢ t : T ~ Q ↑ T ⊣ Σ
+
+Θ; Γ, x:U.* ⊢ t ~ T.$ ↓ T.* ⊣ Σ, x~R ⊢ T.$ >= R
+-------------------------------------------------
+Θ; Γ ⊢ λx. t ~ Q ↓ U -> T ⊣ Q ⋅ Σ
+
+Θ; Γ ⊢ t ~ 1 ↑ U -> T ⊣ Σ0 Θ; Γ ⊢ u ~ U.$ ↓ U.* ⊣ Σ1 ⊢ T.$ >= Q
+-------------------------------------------------------------------
+Θ; Γ ⊢ t u ~ Q ↑ T ⊣ Σ0 + Σ1
+
+Θ, X::k; Γ ⊢ t ~ T.$ ↓ T.* ⊣ Σ
+-----------------------------------
+Θ; Γ ⊢ ΛX. t ~ Q ↓ ∀X::k. T ⊣ Q ⋅ Σ
+
+Θ; Γ ⊢ t ~ 1 ↑ ∀X::k. T ⊣ Σ Θ ⊢ U ↓ k ⊢ T.$ >= Q
+----------------------------------------------------
+Θ; Γ ⊢ t [U] ~ Q ↑ T.*[U/X] ⊣ Σ
+
+
+The auxiliary judgement "⊢ Q >= R" means "the quantity Q (viewed as a supply)
+is greater than the quantity R (viewed as a demand)". We should at least have
+the rule
+
+--------
+⊢ q >= r
+
+whenever q >= r in the quantity algebra, but in principle more rules can be
+added depending on chosen quantity algebra. For example, if the quantity
+algebra is a singleton (so that we have normal System Fω), we can adopt the
+rule
+
+--------
+⊢ Q >= R
+
+(where we emphasize that Q and R are arbitrary types of kind $, meaning they
+could be neutral).
+
+
+--------------------------------------------------------------------------------
+Inductive types
+
+At this point, we only have arrow and forall types to work with. That's enough
+to Church-encode inductive types like nats, lists, and trees, but the derived
+elimination rules for these types are oblivious of the fact that only one
+case will apply, so the quantity tracking is needlessly conservative.
+
+For example, take
+ Nat := ∀M::$*. Q0 ! (M -> Q1 ! (Q2 ! (M -> M) -> M))
+Here, the motive M has kind $* instead of the usual *, so we get to pick the
+continuation quantity when we eliminate a Nat. Technically, we need to decide
+on quantities Q0, Q1, and Q2, but they're noise for now, so let's remove them:
+ Nat := ∀M::$*. M -> (M -> M) -> M
+The problem mentioned above is that, given n:Nat, the elimination n [M] z s
+has to "pay" for "resources" used by both z and s, even though only one will
+apply.
+
+To get a tighter, more intuitive accounting of quantities for inductive types,
+we need to build them in as primitives and add a LUB operation to quantity
+algebras.
+
+TODO: Type up the rules for inductive types.
