398 lines
9.1 KiB
Markdown
398 lines
9.1 KiB
Markdown
# 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. modular 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]
|
||
γ ⊢ δ
|
||
|
||
// 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
|
||
```
|
||
|