# System F(lux) v2 I want type parameters to be refinable to support stuff like: ```rust #[flux::sig(fn(x: T, y: T) -> T{v: v == x || v == y})] fn choose(x: T, y: T) -> T; ``` My idea is to have a kind system that differentiates between type variables over _base types_ (`bty`) and (refinement) _types_ (`typ`). We will pick automatically wich kind based on the usage: if a variable is refined in any way we pick `bty` otherwise we pick `typ`. ## Syntax Type expressions `t` consist of types, base types and refinements. I'm putting everything in the same syntactic category. The kind system will differentiate between them. Something interesting to note about the syntax is the sort `sortof(t)` which signifies the sort associated to a base type. It's meant to be well-formed only when `t` is a base type. So we have for example `sortof(int) ≡ sint`, but `sortof(int[0])` is not well-formed. I'm using a very general syntax that allows arbitrary for alls `∀X:κ. t` and existentials `∃X:κ. t`. I'm assuming the implementation will have appropriate restrictions to make it decidable. I'm also using the syntax `t ∧ r` for a _constrained type_ which signifies a value of type `t` and also that the predicate `r` holds. Existentials and constrained type are used to desugar the surface syntax `B{v: p}` as `∃v:σ. B[ν] ∧ p` where `σ` is the sort associated with `B` (i.e. `sortof(B) ≡ σ`). ``` X,α,a,ρ,ν ∈ Var z ∈ ℤ Type Expressions t := Types | t[r] indexed type | t ∧ r constraint type | ∀X:κ. t polymorphic type (over types, base types or refinements) | ∃X:κ. t existential type Base Types | &μ t references | int integers | bool booleans | Unit unit type | ptr(η) strong pointers | fn(T; t) -> T;t function type (only one argument because unicode) Refinements | tt | ff boleans | z integers | () unit | r = r equality | r[+,-,*]r arithmetic | r[∧,∨]r boolean logic | λa.r abstractions | ℓ locations Variables | X refinement (a or ν), location (ρ), type (α) or base type (β) Modifiers μ := mut | shr Locations η := ℓ | ρ Sorts σ := sint | sbool | sunit | sloc | σ -> σ | sortof(t) Kinds κ := type | bty | σ Location Contexts T := ∅ | T,ρ ↦ t Variable Contexts Δ := ∅ | Δ,X:κ ``` ## Well-formed judgments We define the following judgments mutually recursively: * `⊢ Δ` is read `Δ` is well-formed * `Δ ⊢ κ` is read `κ` is well-formed under context `Δ` * `Δ ⊢ t: κ` is read `t` has kind `κ` under context `Δ` * `Δ ⊢ T` is read location context `T` is well-formed under context `Δ` The first two judgments are just to rule out the case were `t` is not a base type in `sortof(t)` and are not very interesting. The judgment `Δ ⊢ t: κ` mostly separate types, base types and refinements. Probably the most interesting rule is for `t[r]` which says it has kind `typ` if `t` is a base type (has kind `bty`) and `r` is well-sorted under the sort of `t` (`Δ ⊢ r: sortof(t)`). ``` Variable Contexts ----------------- Δ ⊢ κ ⊢ Δ ───────────── ────── ⊢ Δ, X:κ ⊢ ∅ Kinds ----- κ ∈ [sint, sbool, sunit, sloc, type, bty] ───────────────────────────────────────── Δ ⊢ κ Δ ⊢ t: bty Δ ⊢ σ₁ Δ ⊢ σ₂ ──────────────── ────────────────── Δ ⊢ sortof(t) Δ ⊢ σ₁ -> σ₂ Variables --------- X:κ ∈ Δ ⊢ Δ ──────────────── Δ ⊢ X: κ Types ----- Δ ⊢ t: bty Δ ⊢ r: sortof(t) Δ ⊢ t: typ Δ ⊢ r: sbool ────────────────────────────── ────────────────────────── Δ ⊢ t[r]: typ Δ ⊢ t ∧ r: typ Δ,X:κ ⊢ t: κ' Δ,X:κ ⊢ t: κ' ────────────────── ───────────────── Δ ⊢ ∀X:κ. t: typ Δ ⊢ ∃X:κ. t: typ Base Types ---------- Δ ⊢ t: κ Δ ⊢ ρ: sloc ────────────── ──────────── ───────────── ─────────────── Δ ⊢ &μ t: bty Δ ⊢ int: bty Δ ⊢ bool: bty Δ ⊢ ptr(ρ): bty Δ ⊢ t₁: typ Δ ⊢ t₂: typ Δ ⊢ T₁ Δ ⊢ T₂ ─────────────── ──────────────────────────────────────────── Δ ⊢ Unit: bty Δ ⊢ fn(T₁; t₁) -> t₂/T₂: bty Refinements ----------- Δ ⊢ r₁: σ Δ ⊢ r₂: σ ───────────── ───────────── ─────────── ────────────────────── Δ ⊢ tt: sbool Δ ⊢ ff: sbool Δ ⊢ z: sint Δ ⊢ r₁ = r₂: sbool ⊕ ∈ {+, -, *} ⊕ ∈ {∧, ∨} Δ ⊢ r₁: sint Δ ⊢ r₂: sint Δ ⊢ r₁: sbool Δ ⊢ r₂: sbool ────────────── ─────────────────────────── ────────────────────────────── Δ ⊢ (): sunit Δ ⊢ r₁ ⊕ r₂: sint Δ ⊢ r₁ ⊕ r₂: sbool Δ,a:σ₁ ⊢ r: σ₂ ─────────── ───────────────────── Δ ⊢ ℓ: sloc Δ ⊢ λa. r: σ₁ -> σ₂ Location Contexts ----------------- Δ ⊢ T Δ ⊢ η: sloc Δ ⊢ t: typ ──────────────────────── ─────── Δ ⊢ T,η↦t Δ ⊢ ∅ ``` ### Sort Equivalence We also equip sorts with an equivalence that satisfies the following equations and then define everything up to this equivalence. The idea is that `sortof(t)` can be replaced by a concrete sort and everything remains well-formed. ``` sortof(&μ t) ≡ sunit sortof(int) ≡ sint sortof(bool) ≡ sbool sortof(Unit) ≡ sunit sortof(ptr(η)) ≡ sunit sortof(fn(T; t) -> T/t) ≡ sunit ``` Note that base types that we cannot meaningfully refine have sort `sunit`. ## Examples Some examples illustrating how we desugar the surface syntax and how type parameters are instantiated. ### Unrefined type parameters If we detect that a type type parameter is unrefined we pick a variable of kind `typ`. This is basically what is currently implemented. **Example 1** Consider the function `choose1` with the following signature. ```rust= fn choose1<T>(x: T, y: T) -> T; ``` Since `T` is not refined we desugar the signature to: ``` ∀ α:type. fn(α, α) -> α ``` At the call site we do the "normal" instantiation and pick an existential with a fresh kvar. Thus, for the call ```rust choose1(0, 1) ``` we get the following instantiation ``` choose1<α := ∃ν:sint. int[ν] ∧ $k(ν)>(0, 1) ``` This will generate the following subtyping constraints ``` int[0] <: ∃ν:sint. int[ν] ∧ $k(ν) int[1] <: ∃ν:sint. int[ν] ∧ $k(ν) ``` **Example 2** Similar example but with mutable reference. ```rust fn swap1<T>(x: &mut T, y: &mut T); ``` ``` ∀α:type. fn(&mut α, &mut α) ``` ```rust swap1(&mut 0, &mut 1) ``` ``` swap1<α := ∃ν:sint. int[ν] ∧ $k(ν)>(&mut 0, &mut 1) ``` ### Refined Type Parameters If a type parameter is refined we pick a parameter of kind `bty` when desugaring. **Example 3** Consider the version of `choose` with a refined annotation ```rust= #[flux::sig(fn(a:T, b:T) -> T)] #[flux::sig(fn(a:T, b:T) -> T{v: v == a || v == b})] #[flux::sig(fn(T[@a], T[@b]) -> T{v: v == a || v == b})] fn choose2<T>(x: T, y: T) ``` Since `T` is being refined, we pick kind `bty`. Thus, the signature becomes ``` ∀ β:bty, a:sortof(β), b:sortof(β). fn(β[a], β[b]) -> ∃ν:sort(β). β[ν] ∧ (ν = a ∨ ν = b) ``` At the call site we instantiate it like so ``` choose2<β := int, a := 0, b := 1>(0, 1) ``` Note that the instantiation `a := 0` (resp. `b := 1`) is well-formed because `sortof(int) ≡ sint` **Example 4** A similar example but using abstract refinements instead of indices ```rust #[flux::sig(fn<p: T -> bool>(T{v: p(v)}, T{v: p(v)}) -> T{v: p(v)})] fn choose3<T>(x: T, y: T) -> T; ``` ``` ∀ β: bty, p: sortof(β) -> sbool. fn(∃ν:sortof(β). β[ν] ∧ p(ν), ∃ν:sortof(β). β[ν] ∧ p(ν)) -> ∃ν:sortof(β). β[ν] ∧ p(ν) ``` ``` choose3<β := int, p := λν.$k(ν)>(0, 1) ``` **Example 5** A version of swap that tracks explicit indices ```rust #[flux::sig(fn(x: &strg T[@a], y: &strg T[@b]) -> ensures x: T[b], y: T[a])] fn swap2<T>(x: &mut T, y: &mut T); ``` ``` ∀β:bty, ρ₁:sloc, ρ₂:sloc, a:sortof(β), b:sortof(β). fn(ρ₁↦β[a],ρ₂↦β[b]; ptr(ρ₁), ptr(ρ₂)) -> (ρ₁↦β[b],ρ₂↦β[a]);Unit ``` Consider the following call site ```rust let mut x = 0; let mut y = 1; swap(&mut x, &mut y); ``` If we give `x` and `y` locations `ℓ₁` and `ℓ₂` then we have. ``` swap2<β := int, ρ₁ := ℓ₁, ρ₂ := ℓ₂, a := 0, b := 1>(&mut x, &mut y) ``` ### Mismatched Kinds Errors We could get errors with invalid kinds in some situations. Suppose you want to use the second specification for `choose` like so: ```rust= fn ipa<T>(x: T, y: T) { let z = choose2(x, y); } ``` This would give a kind mismatch error since we would pick kind `typ` for `T` but the signature of `choose2` uses kind `bty`. ## What am I trying to solve? Recall the signature of `choose2` ```rust #[flux::sig(fn(T[@a], T[@b]) -> T{v: v == a || v == b})] fn choose2<T>(x: T, y: T) ``` And now suppose we dont' have kinds. The desugared signature would look something like ``` ∀ α,a,b. fn(α[a], α[b]) -> ∃ν. α[ν] ∧ (ν = a ∨ ν = b) ``` Now consider the following call ```rust choose2(0, 1) ``` If we instantiate the type parameter `α` using the current strategy where we blindly pick an existential, we would generate `α := ∃ν'. int[ν'] ∧ $k(ν')`. Then, when substituting for `α` in the first argument we would get `(∃ν'. int[ν'] ∧ $k(ν'))[?a]` where `?a` is an evar for the parameter `a`. Now, what does it mean to index an existential? With the kind system, this type is not well-formed so we don't need to answer it. The alternative would be to answer the question. I can think of a couple of options. The idea is to remove the distinction between `typ` and `bty`, and then assign sorts to all types (including existentials). 1. The first option is to say that existential are indexed by `sunit`. In this case the instantiation above work just fine but we would solve `?a` (and `?b`) to `()` and get the uninteresting postcondition `ν = () || ν = ()`. In that sense, the problem becomes choosing a better instantiation. That would require knowing how `α` is used in the signature which is kind of what the kind system is doing. 2. Another alternatively would be to enrich the kind system such that the sort of the existentially quantified variable is "lifted" to be the sort of the existential itself, i.e., we could define the equivalence `sortof(∃ν:σ. t) ≡ σ`. In this sytem the type `(∃ν:σ. t)[r]` is well-formed when `r` has sort `σ`. But now the question becomes how to define `(∃v:σ. t)[r]` *semantically*. I believe sprite answers this by defining the equivalence[^1] ``` (∃ν:σ. t)[r] ≡ ∃ν:σ. t ∧ ν = r ``` I find this a bit unsatisfying because the `ν = r` "eats up" any properties encoded in `t` (and could easily generate uninhabited types). However, this may not be a problem in practice and since every type uniformely has a sort we don't need to deal with mismatched kinds errors. Also I'm not sure how well this interpretation extends to define the semantics of other combinations like `(t ∧ p)[r]` or `(t[r₁])[r₂]`, but maybe for those cases we could just define that the sort is `sunit` (i.e., `r` and `r₂` need to have sort `sunit` for the them to be well-formed). Since we only pick existentials for instantiating type parameters then they won't show up in pratice. Finally, just defining the equivalence doesn't actually answer the question of what it means to index an existential, I still have troubles giving a semantic interpretation for it. # Random Thoughs * An alternative interpretation of my proposal could be that there are syntactically two type variables, one for base types and one for types. The implementation may do it like this (i.e., we could have `rty::Ty::Param` and `rty::BaseTy::Param`). I'm proposing the kind system more as reference framework to think about the problem more than something that we should implement. * Crazy idea for the future: we could eventually add "where" clauses that restricts the sort of a type variable. Somethine like: ``` fn<β: bty, sortof(β) ≡ sint, a: sint>(β[a]) -> β[a + 1] ``` I believe this can be particularly useful when refining a trait.