9.1 KiB
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
// 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_is. 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