# System F(lux) v1 ## Syntax I'll introduce a kind system so I'm putting everything in the same syntactic category which I'm calling type expressions. Well-formedness will separate type expressions into `Types`, `Base Types`, `Refinements` and `Sorts`. The idea is that substitution is defined as usual, but it satisfies a well-formedness substitution lemma. Note that this is different than LH where you can alter the definition of substitution with the _strengthening_ trick which doesn't really apply for indexed types (maybe there's a similar trick?). The key thing I'm trying to avoid is a situation in which I have `α[r₀]` and then substitute `t[r₁]` for `α` resulting in `t[r₁][r₀]`. This should not be well-formed and must be guaranteed by the kind system. ``` X,α,a,ρ ∈ Var z ∈ ℤ Type Expressions t := Types | t[r] indexed type | t ∧ r constraint type | ∀X:κ. t polymorphic type (over types, base types, sorts 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 | ℓ locations Sorts | σ Variables | X variables (refinement a, location ρ or type α) Modifiers μ := mut | shr Locations η := ℓ | ρ Sorts σ := sint | sbool | sunit | sloc | σ -> σ Kinds κ := type | σ -> type | σ | sort Location Contexts T := ∅ | T,ρ ↦ t Variable Context Δ := ∅ | Δ,X:κ ``` ### Notes * The existential syntax `int{v: v > 0}` desugars to `∃v:sint. int[v] ∧ v > 0` * The syntax for existentials `∃v:σ. t` is very general, I'm assuming there's some well-formedness check that ensures `v` appears in places we can automatically infer. * actually everything is very general, but I believe we should be able to instantiate everything automatically by placing the right restrictions. ## Well-formed type expressions ``` Δ ⊢ t: κ Sorts ─────────── Δ ⊢ σ: sort Variables X:κ ∈ Δ ───────── Δ ⊢ X: κ Types ∆ ⊢ t: σ -> type Δ ⊢ r: σ Δ ⊢ t: type Δ ⊢ r: sbool ──────────────────────────── ────────────────────────── Δ ⊢ t[r]: type Δ ⊢ t ∧ r: type Δ,X:κ ⊢ t: κ' Δ,X:κ ⊢ t: κ' ────────────────── ───────────────── Δ ⊢ ∀X:κ. t: type Δ ⊢ ∃X:κ. t: type Base Types Δ ⊢ t: κ ──────────────────────── ───────────────────── ───────────────────────── Δ ⊢ &μ t: sunit -> type Δ ⊢ int: sint -> type Δ ⊢ bool: sbool -> type Δ ⊢ ρ: sloc ───────────────────────── ───────────────────────── Δ ⊢ ptr(ρ): sunit -> type Δ ⊢ Unit: sunit -> type Δ ⊢ tᵢ: type Δ ⊢ tₒ: type Δ ⊢ Tᵢ Δ ⊢ Tₒ ──────────────────────────────────────────── Δ ⊢ fn(Tᵢ; tᵢ) -> tₒ/Tₒ: sunit -> type 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 ─────────── Δ ⊢ ℓ: sloc ``` ### Well-formed location contexts ``` Δ ⊢ T Δ ⊢ η: sloc Δ ⊢ t: type ───────────────────────── ─────── Δ ⊢ T,η↦t Δ ⊢ ∅ ``` ## Examples Some examples illustrating how we desugar the surface syntax and how polymorphic parameters are instantiated. ### Unrefined type parameters **Example 1** ```rust fn choose1<T>(x: T, y: T) -> T; ``` Since `T` is not refined, we pick `type` for its kind. Thus, the type becomes ``` ∀ α:type. fn(α, α) -> α ``` Note that we can still use `choose` with base types since we can always make base types into types with an existential (but not the other way around). For example, consider the call ```rust choose1(0, 1) ``` We can instantiate the parameter as ``` choose<α := ∃ν:sint. int[ν] ∧ $k(ν)>(0, 1) ``` **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 **Example 3** Consider this modified version of `choose` with a refined annotation ```rust #[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 `σ -> type` for some sort `σ`. Thus the signature becomes ``` ∀ σ:sort, α:(σ -> type), a:σ, b:σ. fn(α[a], α[b]) -> ∃ν:σ. α[ν] ∧ (ν = a ∨ ν = b) ``` At the call site we instantiate it like ``` choose2<σ := sint, α := int, a := 0, b := 1>(0, 1) ``` **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; ``` ``` ∀ σ:sort,p:(σ -> sbool),α:(σ -> type). fn(∃ν:σ. α[ν] ∧ p(ν), ∃ν:σ. α[ν] ∧ p(ν)) -> ∃ν:σ. α[ν] ∧ p(ν) ``` ``` choose3<σ := sint, p := λν.$k(ν), α := int>(0, 1) ``` **Example 5** A version of swap that track 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); ``` ``` ∀σ:sort, α:(σ -> type), ρₒ:loc, ρ₁:loc, a:σ, b:σ. 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<σ := sint, α := 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 `type` for `T` but the signature of `choose2` uses kind `σ -> type`. ### What could go wrong without kinds Consider a call to `choose2` ```rust choose2(0, 1) ``` If we don't consider the kinds and use the strategy it is implemented right now that instantiates type parameters blindly by an existential, we would generate `α := ∃ν':sint. int[ν'] ∧ $k(ν')`. Then, when substituting for `α` in the first argument we would get `(∃ν':sint. int[ν'] ∧ $k(ν'))[?a]` which is not well-formed (what does it mean to index an existential?). I guess, we could define that existentials are indexed by `sunit`, in which case the instantiation will work fine but using `choose2` instantiated with an existential will give completely useless information. 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. On the plus side, if every type is uniformedly indexed by a sort then there are no kind mismatch errors. # Random Thoughs * An alternative interpretation could be that there are two kinds of type variables, one for base types and one for types.