# description of sappho formals

## sappho grammar

```
s, t ::= s | t              (disjunction, a.k.a. union)
       | s & t              (conjunction, a.k.a. intersection)
       | s => t             (implication)
       | s -> t             (arrow, a.k.a. function)
       | forall x . t       (forall, polymorphic)
       | box t              (box, c.f. modal logic)
       | a [t..]            (type operator application)
       | x                  (variable)
       | n                  (nominal)
       | true               (true, a.k.a. top)
       | false              (false, a.k.a. bottom)
       | { m : t }          (member, a.k.a. atomic record)


x ∈ var
n ∈ nominal
a ∈ opname
```

## sappho subtyping rules

```cmath
// trace pairs: none
---- [identity]
s, γ ⊢ s, δ

// trace pairs: none
---- [true-right]
γ ⊢ true, δ

// trace pairs: none
---- [false-left]
false, γ ⊢ δ

// trace pairs: none?
s, t, γ ⊢ δ
---- [conj-left]
s & t, γ ⊢ δ

// trace pairs: none?
γ ⊢ s, t, δ
---- [disj-right]
γ ⊢ s | t, δ

// trace pairs: none?
s, γ ⊢ δ
t, γ ⊢ δ
---- [disj-left]
s | t, γ ⊢ δ

// trace pairs: none?
γ ⊢ s, δ
γ ⊢ t, δ
---- [conj-right]
γ ⊢ s & t, δ

// XXX
// remove s => t? always make progress
// trace pairs: none?
s => t, s, t, γ ⊢ δ
---- [impl-left]
s => t, s, γ ⊢ δ

// trace pairs: none?
s, γ ⊢ t, δ
---- [impl-right]
γ ⊢ s => t, δ

// box works as a kind of "forall" for concrete types
// trace pairs: none
box t, t, γ ⊢ δ
---- [box-left]
box t, γ ⊢ δ

// (.)-- filters the contexts.
// trace pairs: premise[0] -- conclusion
γ-- ⊢ t, δ--
---- [box-right]
γ ⊢ box t, δ


// using cyclic proof strategy, rule for dealing with aliases/type operators
// becomes really simple. However, this requires well-formedness rules on types
// to exclude typedefs like
// type A = A
// Or that our cycle detection excludes paths between "identical" states.
// trace pairs: none?
γ ⊢ expand(a[t..]), δ
----
γ ⊢ a[t..], δ

expand(a[t..]), γ ⊢ δ
----
a[t..], γ ⊢ δ


// member types are filtered according to member name
// trace pairs: premise[0] -- conclusion
γ >> m ⊢ δ >> m
---- [member]
γ ⊢ δ


// foralls are unwrapped and variable substituted with fresh name
// i.e. we treat the bound variable nominally
// trace pairs: premise[1] -- conclusion
n fresh
γ [n] ⊢ δ [n]
---- [forall]
γ ⊢ δ

// TODO can we choose a simpler rule instead?
// 1 + n! premises
// trace pairs: i ∈ [1..(n! + 1)], premise[i] -- conclusion
c, γ*  ⊢ a_1, ..., a_n, δ*
∀ I ⊆ {1, ..., n}.
	c, γ* ⊢ { a_i | i ∈ I }, δ*
	OR
	{ b_i | i ∈ ¬I }, γ* ⊢ d, δ*
---- [loads-of-fun]
a_1 -> b_1, ..., a_n -> b_n, γ    ⊢    c -> d, δ
```


### context operators

* box filtering
```
(t, γ)-- =def= t, γ--       if t == box s, for some s
               γ--          otherwise
```

* member unwrapping
```
(t, γ) >> m =def= s, (γ >> m)       if t == { m : s }, for some s
                  t, (γ >> m)       if t == box s, for some s
                  γ >> m            otherwise
```

* forall-unwrapping and substitution
```
(t, γ) [n] =def= s [n/x], (γ [n])   if t == forall x . s, for some x, s
                 t, (γ [n])         if t == box s, for some s
                 γ [n]              otherwise
```

### trace pairs
Trace pairs are related to cyclic proofs. They identify the pairs of 
`premise -- conclusion` that are *productive*, i.e. leads to some progress
making a cycle in the proof tree admissable as a cyclic proof of the nodes in
the cycle.

The trace pairs are described in the comments for each subtyping rule.

### Semantic function subtyping

*Here we try to give an intuitive explainer of how to reason about function
subtyping in the semantic subtyping domain.*

Given function types
```
a_1 -> b_1, ..., a_n -> b_n
```
the conjunction (intersection) of `a_i -> b_i`, i.e.
```
intsec = (a_1 -> b_1) & ... & (a_n -> b_n)
```
represents the set of functions that combines the properties of all
`a_i -> b_i` by themselves. To get an idea of what functions this describes,
let's start with reasoning about values, that is, functions in `intsec`.
First we note that any function in this set accepts any argument that are in
either of the `a_i`s.  That is, it can take any argument in the set represented
by
```
a = a_1 | ... | a_n
```
Furthermore, a function `f` in `intsec` "promises" to map any value in `a_i` to
a value in its corresponding `b_i`.
Specifically, given `I ⊆ {1..n}`, a value `v` in the intersection
```
a_I_intsec = &[i ∈ I] a_i
```
is mapped to a value in
```
b_I_intsec = &[i ∈ I] b_i
```
that is,
```
v ∈ &[i ∈ I] a_i   implies   f(v) ∈ &[i ∈ I] b_i
```

*In the following we will "abuse notation" a bit. Try to look at it like
talking to an old friend, and you just instinctively know exactly what they
mean without explaining...*

Now, given a type `c -> d`, how do we know if
```
intsec = &[i ∈ {1..n}] a_i -> b_i <: c -> d
```
?
Or equivalently, friend speaking, if
```
∩[i ∈ {1..n}] a_i -> b_i ⊆ c -> d
```
?

Immediately, it should be obvious that
```
c ⊆ a (= ∪[i ∈ {1..}] a_i)
```
Furthermore, it is necessary that any function in `intsec` will have to map all
values in `c` into `d`, specifically
```
f ∈ intsec, v ∈ c   implies   f(v) ∈ d
```
Note that this does not mean that any function in `a_i -> b_i` must map all
values in `a_i` into `d`, since it's not necessary that `a_i \ c = ø`.
Specifically, it is not necessary that `b_i ⊆ d`. However, taking `I ⊆ {1..n}`,
assuming
```
a_I_intsec = &[i ∈ I] a_i ⊆ c
```
then, necessarily
```
b_I_intsec = &[i ∈ I] b_i ⊆ d
```

Conversely, if
```
b_I_intsect ⊆ d
```
then any function in `intsec` maps `a_I_intsec` into `d`. If `a_I_intsec`
happens to intersect with `c`, it "covers" a part of `c`. I.e. the set `I` can
be understood as promising to map a part of `c` into `d`.

Defining this formally, we say that `I_cand ⊆ {1..n}` is a (`d`-)*candidate* if,
```
∩[i ∈ I_cand] b_i ⊆ d
```
We can thus see a candidate `I_cand` as a combination, or more specifically,
intersection of the function types `{a_i -> b_i | i ∈ I_cand}`, that according
to the reasoning above promises to map a part of the domain into `d`, namely
```
∩[i ∈ I_cand] a_i
```
A candidate thus "covers" part of the domain or formally speaking, `I`
(`d`-)covers a domain `s` if `I` is a (`d`-)candidate and
```
s ⊆ ∩[i ∈ I] a_i
```
If `IS ⊆ P({1..n})` then we say that `IS` (`d`-)covers `s` if all of `s` is
covered by some `I ∈ IS`, that is
```
s ⊆ ∪[I ∈ IS | I is d-candidate] ∩[i ∈ I] a_i
```

Given the function types `{a_i -> b_i | i ∈ {1..n}}` and its set of candidates
`IC = {I_cand_1..I_cand_k}`, it is fairly easy to see that
```
&[i ∈ {1..n}] (a_i -> b_i)  <:  c -> d
```
iff `IC` `d`-covers `c`:
```
c   ⊆   ( ∪[I_cand ∈ IC]  ∩[i ∈ I_cand] a_i )
```
Using some *pro gamer moves*, we can see that this is equivalent to
```
c   ⊆   ( ∩[I_cand ∈ IC]  ∪[i ∉ I_cand] a_i )
```
This gives us the final form for our subtyping rule
```
c, γ*    ⊢    a_i | ... | a_n, δ*
forall I ⊆ {1..n}.
	&[i ∈ I] b_i, γ*    ⊢    d, δ*
	  or
	c, γ*    ⊢    |[i ∉ I] a_i, δ*
---- [loads-o-fun]
a_1 -> b_1, ..., a_n -> b_n, γ ⊢ c -> d, δ
```

### Recursive subtyping

Type aliases creates the possibility of recursive types, and thus we need to
handle recursive subtyping

Handling subtyping co-inductively would enable us to handle the relation
```
type A = { x : { y : A } }
type B = { y : { x : B } }

A <: { x : B }
{ x : B } <: A
```


We have made progress if we "switch context"

If we make progress and end up at the same sequent, co-induction gives us the
conclusion.

Some actions/rules lead to equivalent contexts, i.e. does not switch
context/make progress.

### Other

True ~ { x : True } on the left
False ~ { x : False } on the right

or rather

True ~ { x : True } in positive position
False ~ { x : False } in negative position





### implication
```

γ ⊢ s => t, u => s, δ

if s, then u => s holds
if ¬s, then s => t holds

```


altho
```
γ ⊢ s => t, s, δ
```

Given the msph program
```
nominal n

type Woops[e] = {
	member f : (e <: false => n) | (e <: false)
}

type Noooes = {
	member f : true
}
```
we can prove that, for any type `t`
```
Noooes <: Woops[t]
```

The derivation looks like this:
```
---- [identity]
true, t <: false ⊢ n, (t <: false)
---- [impl-right]
true ⊢ (t <: false => n), (t <: false)
---- [disj-right]
true ⊢ (t <: false => n) | (t <: false)
---- [member]
{ f : true } ⊢ { f : (t <: false => n) | (t <: false) }
---- [expand-right]
{ f : true } ⊢ Woops[t]
---- [expand-left]
Nooes ⊢ Woops[t]
---- [impl-right]
⊢ Nooes => Woops[t]
---- [box-right]
⊢ Nooes <: Woops[t]
```

This looks a bit dangerous at first. However, if we translate the implication to
using disjunction and negation, we get
```
(t <: false => N) | (t <: false) == (¬(t <: false) | n) | (t <: false)
```

Considering the two cases
```
(1) t == false
(2) t != false
```
we see that in (1)
```
(¬(t <: false) | n) | (t <: false) ==
(¬(true) | n) | (true) ==
true
```
and in (2)
```
(¬(t <: false) | n) | (t <: false) ==
(¬(false) | n) | false ==
(true | n) | false ==
true
```