Γ ` t: Q → T ∆ ` u: Q

We exhibit a generic modal type system for simply-typed lambda-calculus that subsumes linear and relevance typing, strictness analysis, variance (positivity) checking, and other modal typing disciplines. By identifying a common structure in these seemingly unrelated non-standard type systems, we hope to gain better understanding and a means to combine several analyses into one. This is work in progress. Our modal type assignment system is parametrized by a (partially) ordered monoid (P, ·, 1, ≤) with a partial, monotone binary operation + and a default element p0 ∈ P. Types T,U include at least a greatest type> and function types Q → T, and form a partial ordering under subtyping T ≤ T ′ with partial meet T ∧T ′. Modal types Q:: = pT support composition pQ and partial meet Q ∧Q ′ defined by p(qT) = (pq)T and pT ∧ qT = (p + q)T. Subtyping pT ≤ p′T ′ holds if p ≤ p ′ and T ≤ T ′. For typing contexts Γ,∆, which are total functions from term variables to modal types, modality composition pΓ, subsumption Γ ≤ ∆, and meet Γ ∧ ∆ are defined pointwise. Finite contexts x1:Q1,..., xn:Qn are represented as Γ(xi) = Qi and Γ(y) = p0> for y 6 = xi. Judgements Γ ` t: T and Γ ` t: Q are given by the following (linear) typing rules: p ≤ 1 x: pT ` x: T hy