---
# System prepended metadata

title: System F(lux) v1
tags: [Flux]

---

# 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.
