added explainer for semantic subtyping of function types

README.md

@@ -28,43 +28,43 @@ a ∈ opname
 
 ```
 ---- [identity]
-ρ; s, γ ⊢ s, δ
+s, γ ⊢ s, δ
 
 ---- [true-right]
-ρ; γ ⊢ true, δ
+γ ⊢ true, δ
 
 ---- [false-left]
-ρ; false, γ ⊢ δ
+false, γ ⊢ δ
 
-ρ; s, t, γ ⊢ δ
+s, t, γ ⊢ δ
 ---- [conj-left]
-ρ; s & t, γ ⊢ δ
+s & t, γ ⊢ δ
 
-ρ; γ ⊢ s, t, δ
+γ ⊢ s, t, δ
 ---- [disj-right]
-ρ; γ ⊢ s | t, δ
+γ ⊢ s | t, δ
 
-ρ; s, γ ⊢ δ
-ρ; t, γ ⊢ δ
+s, γ ⊢ δ
+t, γ ⊢ δ
 ---- [disj-left]
-ρ; s | t, γ ⊢ δ
+s | t, γ ⊢ δ
 
-ρ; γ ⊢ s, δ
-ρ; γ ⊢ t, δ
+γ ⊢ s, δ
+γ ⊢ t, δ
 ---- [conj-right]
-ρ; γ ⊢ s & t, δ
+γ ⊢ s & t, δ
 
 // XXX
 // remove s => t? always make progress
-ρ; s => t, s, t, γ ⊢ δ
+s => t, s, t, γ ⊢ δ
 ---- [impl-left]
-ρ; s => t, s, γ ⊢ δ
+s => t, s, γ ⊢ δ
 
 // discussion about implication below
 // check how "normal sequent calculus handles this"
-ρ; s, γ ⊢ t, δ
+s, γ ⊢ t, δ
 ---- [impl-right]
-ρ; γ ⊢ s => t, δ
+γ ⊢ s => t, δ
 
 
 
@@ -74,9 +74,9 @@ box t, t, γ ⊢ δ
 box t, γ ⊢ δ
 
 // (.)-- filters the contexts.
-ρ; γ-- ⊢ t, δ--
+γ-- ⊢ t, δ--
 ---- [box-right]
-ρ; γ ⊢ box t, δ
+γ ⊢ box t, δ
 
 
 // using cyclic proof strategy, rule for dealing with aliases/type operators
@@ -94,22 +94,25 @@ a[t..], γ ⊢ δ
 
 
 // member types are filtered according to member name
-ρ; γ >> m ⊢ δ >> m
+γ >> m ⊢ δ >> m
 ---- [member]
-ρ; γ ⊢ δ
+γ ⊢ δ
 
 
 // foralls are unwrapped and variable substituted with fresh name
 // i.e. we treat the bound variable nominally
 n fresh
-ρ; γ [n] ⊢ δ [n]
+γ [n] ⊢ δ [n]
 ---- [forall]
-ρ; γ ⊢ δ
+γ ⊢ δ
 
-
-ρ; t[n/x], s[n/y] ⊢ u[n/z]
-----
-ρ; forall x. t, forall y. s ⊢ forall z. u
+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, δ
 ```
 
 
@@ -135,6 +138,116 @@ n fresh
                  γ [n]              otherwise
 ```
 
+### 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
+```
+Now, letting `IC = {I_cand_1..I_cand_k}` be the set of candidates, it is fairly
+simple to see that
+```
+intsec <: c -> d
+```
+iff
+```
+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, δ*
+----
+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