# System F(lux) v3
The goal is to allow type variables to be refined such that we can write stuff like
```rust
#[flux::sig(fn(x: T, y: T) -> T{v: v == x || v == y})]
fn choose(x: T, y: T) -> T;
```
This design follows from two realizations. The first one is that we can interpret an indexed type `b[r]` in sprite syntax as `b{v | v = r}` and then apply their definition for type variable instantiation (I'm using `⦇⋅⦈` for type instantiation and substitution to avoid confusion with indexed types):
```
α{v₁ | p}⦇α ↦ b{v₂ | q}⦈ ≐ b{ν₁ | p ∧ q⦇ν₁/ν₂⦈}
```
applying this definition directly to a syntax with explicit existentials and constrained types we get:
```
α[r]⦇α ↦ ∃ν. b[ν] ∧ q⦈ ≐ ∃ν. b[ν] ∧ q ∧ ν = r
```
The definition of type variable instantiation I'll propose is basically this, but with some simplifications that follows from the syntax I'm using for types.
The second realization is that we can make any rust type into a base type by making it indexable by unit. This way we can make type variables range only over base types. We could in theory also have variables over any type, but I want to argue that we don't need to if we tweak a bit the definition of base type.
## Syntax
**Base Types.** A base type is something that can be refined, i.e., it can be indexed. The base types `bool` and `int` can be refined by values of sort `sbool` and `sint` respectively. Types which we cannot refine meaningfully are indexed by values of sort `sunit`. For example the type of rust references `&μ t` is indexed by unit (i.e., the following works `(&μ t)[()]`). Similarly, function types are also refined by `sunit`.
More interestingly, type variables `β` can be indexed by values of sort `sortof(β)`. When checking well-formedness `sortof(β)` is an opaque sort, so there's no much you can do with values of this sort except of moving them around, compare them for equality and used them as arguments for abstract refinements.
**Types.** A type is a refinement of a base type. The most fundamental one is an indexed type `b[r]`. Next, we have constrained types `t ∧ r` which signify values of type `t` and also that the predicate `r` holds. We can quantify existentially over a refinement with the type `∃ν:σ. t`. The surface syntax `b{v: r}` is desugared into an existential with a constrained type as `∃ν:σ. b[ν] ∧ p` where `σ` is the sort of the base type `b`. Finally, polymorphic types `∀β. t` abstract over base types. It's debatable whether polymorphic types should be a base type or not, I think we don't need them to, because rust doesn't have higher-ranked type polymorphism so we will never need to replace a type variable with a polymorphic type. However, we could make it a base type with the same refine-it-by-unit trick.
**Expressions.** Types are instantiated with the syntax `e⦇ν:σ. t⦈`. This is a bit weird and I can't explaint it well yet, but I arrived at it after some iteration. Hopefully it's more clear after defining how the type instantiation works.
```
α, β ∈ TypeVar a,b,ρ,ν ∈ RefineVar z ∈ ℤ
Types
s,t :=
| b[r] indexed types
| t ∧ r constrained types
| ∀β. t polymorphic types
| ∃ν:σ. t existential types (over refinements)
Base Types
b :=
| &μ t references
| int integers
| bool booleans
| unit unit type
| ptr(η) strong pointers
| ∀a:σ. ∀π:σ. fn(T; t) -> T;t function type (only one argument and one refinement parameter because unicode)
| β type variables
#[flux::refined_by(x: int, p: int -> bool)]
struct List {...}
fn foo<p: int -> bool>() -> List<\x . true> {}
fn foo() -> ∃p. ∃x: int. List[x, p] -> List[x, p] {
...
}
foo foo() -> ∃p: int -> bool, x: int, y: int. (i32[x] ∧ p(x), i32[y] ∧ p(y))
foo \forall p: int -> bool.foo() -> x: int, y: int. (i32[x] ∧ p(x), i32[y] ∧ p(y))
Modifiers
μ := mut | shr
Sorts
σ := sint | sbool | sunit | sloc | σ -> σ | sortof(β)
Refinements
r :=
| tt | ff booleans
| z integers
| () unit
| r = r equality
| r[+,-,*]r arithmetic
| r[∧,∨]r boolean logic
| λa.r abstractions
| ℓ locations
| a variables
Locations
η := ℓ | ρ
Expressions
e :=
| Λα. e type abstraction
| e⦇ν:σ. t⦈ type variable instantiation
| ⋮
Location Contexts
T := ∅ | T,ρ ↦ t
Variable Contexts
Δ := ∅ | Δ,α | Δ,a:σ
```
## Well-formed judgments
We define the following well-fomred judgments mutually recursively
* `Δ ⊢ t` is read `t` is well-formed under `Δ`
* `Δ ⊢ b: σ` is read `b` has sort `σ` under `Δ`
* `Δ ⊢ r: σ` is read `r` has sort `σ` under `Δ`
* `Δ ⊢ T` is read `T` is well-formed under `Δ`
Most of this is unsurprising. One interesting rule is `[bty-β]` which assigns `β` the sort `sortof(β)`. The other one that is a midly interesting is `[wf-idx]` which checks whether the index `r` has the appropriate sort.
```
Well-formed Types Δ ⊢ t
----------------------------
[wf-idx] [wf-constr] [wf-poly] [wf-exists]
Δ ⊢ b: σ Δ ⊢ r: σ Δ ⊢ t Δ ⊢ r: sbool Δ,α ⊢ t Δ,ν:σ ⊢ t
───────────────────── ───────────────────── ─────────── ───────────
Δ ⊢ b[r] Δ ⊢ t ∧ r Δ ⊢ ∀α. t Δ ⊢ ∃ν:σ. t
Well-formed Base Types Δ ⊢ b: σ
------------------------------------
Δ ⊢ t Δ ⊢ ρ: sloc
────────────── ──────────── ───────────── ──────────────────
Δ ⊢ &μ t: sunit Δ ⊢ int: sint Δ ⊢ bool: sbool Δ ⊢ ptr(ρ): sunit
[bty-β]
Δ ⊢ t₁ Δ ⊢ t₂ Δ ⊢ T₁ Δ ⊢ T₂ β ∈ Δ
─────────────── ─────────────────────────────── ────────────────
Δ ⊢ unit: sunit Δ ⊢ fn(T₁; t₁) -> t₂/T₂: sunit Δ ⊢ β: sortof(β)
Well-sorted Refinements Δ ⊢ r: σ
-------------------------------------
Δ ⊢ 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: σ₁ -> σ₂
Well-formed Location Contexts Δ ⊢ T
-------------------------------------------
Δ ⊢ T
Δ ⊢ η: sloc Δ ⊢ t
─────────────────── ───────
Δ ⊢ T,η↦t Δ ⊢ ∅
```
## Type Variable Instantiation
```
Types
-----
b[r]⦇β ↦ ν:σ. t⦈ ≐ b⦇β ↦ ν:σ. t⦈[r]
(t ∧ r)⦇β ↦ ν:σ. t⦈ ≐ t⦇β ↦ ν:σ. t⦈ ∧ r
(∀β. t)⦇β ↦ ν:σ. s⦈ ≐ ∀β. t
(∀a:σ₁. t)⦇α ↦ ν:σ₂. s⦈ ≐ ∀a:σ₁⦇β ↦ σ₂⦈. t⦇β ↦ ν:σ₂. s⦈
(∃ν₁:σ₁. t)⦇α ↦ ν:σ₂. s⦈ ≐ ∃ν₁:σ₁⦇β ↦ σ₂⦈. t⦇β ↦ ν₂:σ₂. s⦈
Base Types
----------
β⦇β ↦ ν:σ. t⦈[r] ≐ t⦇r/ν⦈
α⦇β ↦ ν:σ. t⦈[r] ≐ α[r] if α ≠ β
(&μ t)⦇β↦ ν:σ. s⦈[r] ≐ (&μ t⦇β ↦ ∃ν:σ. s⦈)[r]
int⦇β↦ ν:σ. s⦈[r] ≐ int[r]
bool⦇β↦ ν:σ. s⦈[r] ≐ bool[r]
unit⦇β↦ ν:σ. s⦈[r] ≐ unit[r]
ptr(η)⦇β↦ ν:σ. s⦈[r] ≐ ptr(η)[r]
(∀a:σ'. fn(T₁; t₁) -> T₂;t₂)⦇β↦ ν:σ. s⦈[r] ≐
∀a:σ'⦇β ↦σ⦈(fn(T₁⦇β ↦ ν:σ. s⦈; t₁⦇β ↦ ν:σ. s⦈)
-> T₂⦇β ↦ ν:σ. s⦈;t₂⦇β ↦ ν:σ. s⦈)[r]
Sorts
-----
sint⦇β ↦ σ⦈ ≐ sint
sbool⦇β ↦ σ⦈ ≐ sbool
sunit⦇β ↦ σ⦈ ≐ sunit
sloc⦇β ↦ σ⦈ ≐ sloc
(σ₁ -> σ₂)⦇β ↦ σ₃⦈ ≐ (σ₁⦇α ↦ σ₃⦈ -> σ₂⦇α ↦ σ₃⦈)
sortof(β)⦇β ↦ σ⦈ ≐ σ
sortof(α)⦇β ↦ σ⦈ ≐ sortof(α) if α ≠ β
Location Contexts
-----------------
(T, ρ ↦ t)⦇β ↦ ν:σ. s⦈ ≐ T⦇β ↦ ν:σ. s⦈, ρ ↦ t⦇β ↦ ν:σ. s⦈
```
Most of the rules here just propagate the instantiation down. The interesting rule is the one for type variables in base types.
```
β⦇β ↦ ν:σ. t⦈[r] ≐ t⦇r/ν⦈
```
We get the refinement `r` the variable `β` is being indexed with from the surrounding context. The rule says that we just replace the variable `β` with the type `t` but "applying" it to the index `r`.
The second interesting part is that we substitute into sorts so we can replace `sortof(β)` with a concrete sort.
For example, if we have the type `∃a:sortof(β). β[a] ∧ p(a)` and we choose the instantiation
```
β ↦ ν:sint. int[ν] ∧ ν > 0
```
we get
```
∃a:σ. (int[a] ∧ a > 0) ∧ p(a)
```
Alternatively, if we pick the instantiation `β ↦ ν:sint. ∃b:sint. int[b]` we get
```
∃a:sint. (∃b:sint. int[b]) ∧ p(a)
```
This one is weird because the instantiation doesn't say anything about `a`. I don't know if this causes problems metatheoretically, but in practice this wont't be a problem because we will always instantiate type variables with something of the form `ν:σ. b[ν] ∧ p` (`p` will be a kvar).
### Expression typing
For completeness, the rules for type abstraction and type instantiation should look something like this.
```
Δ,α ⊢ e: t Δ,ν:σ ⊢ s Δ ⊢ e: Λα. t
───────────────── ─────────────────────────────
Δ ⊢ Λα. e: ∀α. t Δ ⊢ e⦇ν:σ. s⦈: t⦇α ↦ ν:σ. s⦈
⋮
```
## Examples
### Unrefined type parameters
**Example 1**
```rust
fn choose1<T>(x: T, y: T) -> T;
choose1(0, 1)
```
```
Inst := β ↦ ν:sint. int[ν] ∧ $k(ν)
Sig := ∀ β, a:sortof(β), b:sortof(β). fn(β[a], β[b]) -> ∃c. β[c]
PLUG(β[a], Inst) == int[HOLE] /\ $k(HOLE)
∀ β, a:sortof(β), b:sortof(β). fn(β[a], β[b]) -> ∃c. β[c]
choose1⦇β ↦ ν:sint. int[ν] ∧ $k(ν)⦈:
∀ a:sint, b:sint. fn(int[a] ∧ $k(a), int[b] ∧ $k(b)) -> ∃c. int[c] ∧ $k(ν)
```
**Example 2**
```rust
fn swap1<T>(x: &mut T, y: &mut T);
swap1(&mut 0, &mut 1)
```
```
∀β. fn(&mut ∃a:sortof(β). β[a], &mut ∃b:sortof(β). β[b])
swap1⦇β ↦ ν:sint. int[ν] ∧ $k(ν)⦈:
fn(&mut ∃a:sint. int[a] ∧ $k(a), &mut ∃a:sint. int[a] ∧ $k(a))
```
### Refined Type Parameters
**Example 3**
```rust
#[flux::sig(fn(T[@a], T[@b]) -> T{c: c == a || c == b})]
fn choose2<T>(x: T, y: T)
choose2(0, 1)
```
```
∀ β, a:sortof(β), b:sortof(β).
fn(β[a], β[b]) -> ∃c:sortof(β). β[c] ∧ (c = a ∨ c = b)
choose2⦇β ↦ ν:sint. int[ν] ∧ $k(ν)⦈:
∀ a:sint, b:sint. fn(int[a] ∧ $k(b), int[b] ∧ $k(b)) -> ∃c:sint. (int[c] ∧ $k(c)) ∧ (c = a ∨ c = b)
```
**Example 4**
```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;
choose3(0, 1)
```
```
∀ β, p: sortof(β) -> sbool.
fn(∃a:sortof(β). β[a] ∧ p(a), ∃b:sortof(β). β[b] ∧ p(b))
-> ∃c:sortof(β). β[c] ∧ p(c)
choose3⦇β ↦ ν:sint. int[ν] ∧ $k0(ν)⦈
fn(∃a:sint. (int[a] ∧ $k0(a)) ∧ p(a), ∃b:sint. (int[b] ∧ $k0(b)) ∧ p(b))
-> ∃c:sint. (int[c] ∧ $k0(c)) ∧ p(c)
```
**Example 5**
```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);
let mut x = 0;
let mut y = 1;
swap(&mut x, &mut y);
```
```
∀β, ρ₁:sloc, ρ₂:sloc, a:sortof(β), b:sortof(β).
fn(ρ₁↦β[a],ρ₂↦β[b]; ptr(ρ₁), ptr(ρ₂)) -> (ρ₁↦β[b],ρ₂↦β[a]);unit
swap2⦇β ↦ ν:sint. int[ν] ∧ $k(ν)⦈:
∀ρ₁:sloc, ρ₂:sloc, a:sortof(β), b:sortof(β).
fn(ρ₁↦int[a] ∧ $k(a), ρ₂↦int[b] ∧ $k(b); ptr(ρ₁), ptr(ρ₂))
-> (ρ₁↦int[b] ∧ $k(b), ρ₂↦int[a] ∧ $k(b));unit
```
# Random Thoughs
Interestingly, using our definition of type variable instantiation we can derive the definition of type variable instantiation in sprite. In sprite notation the definition is
```
β[ν₁|p]⦇β ↦ b[v₂|q]⦈ ≐ b[ν₁ | p ∧ q[ν₁/ν₂]]
```
Translated into our syntax (omitting sorts for brevity):
```
(∃ν₁. β[ν₁] ∧ p)⦇β ↦ ν₂. b[ν₂] ∧ q⦈ ≐ ∃ν₁. b[ν₁] ∧ (p ∧ q[ν₁/ν₂])
```
Which we can derive:
```
(∃ν₁. β[ν₁] ∧ p)⦇β ↦ ∃ν₂. b[ν₂] ∧ q⦈
≐ ∃ν₁. (β[ν₁])⦇β ↦ ν₂. b[ν₂] ∧ q⦈ ∧ p (by definition)
≐ ∃ν₁. β⦇β ↦ ν₂. b[ν₂] ∧ q⦈[ν₁] ∧ p (by definition)
≐ ∃ν₁. (b[ν₁] ∧ q[ν₁/ν₂]) ∧ p (by definition)
≡ ∃ν₁. b[ν₁] ∧ (p ∧ q[ν₁/ν₂]) (by associativity and commutativity)
```
### Random Instantation
```rust=
fn foo(Option<Nat>) -> Option<Pos> {
fn foo(x:Option<usize>) -> Option<i32> {
let cl = |n| { n + 1 as i32}
// cl : (usize{$ka} -> i32{$kb})
x.map(cl)
}
// map::<A=usize, B=i32, F=Closure...> -> Option<i32{$k2}>
// map::<A=usize{$k1}, B=i32{$k2},...>
//
//
// map: (Opt<A>, F) -> Opt<B>
// F : FnOnce(A) -> B
//
// A =
//
// usize{$k1}) -> i32{$k2}
```
```
forall x . 0 < x |- t1 <= t2
----------
x:{v:int | 0 <= v } -> t1 <: x:{v:int | 0 < v } -> t2
list <\h t -> 0 < h > <: list <\h t -> 0 <= h >
\h t -> 0 < h ===> \h t -> 0 <= h
\forall h,t. 0 < h => 0 <= h
```
Sign in with Wallet
Connect another wallet