From 0ca279f18ce26d3916bae45d8015d3e1bf23538e Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Tue, 17 Jun 2025 23:19:43 +0200 Subject: [PATCH] added explainer for semantic subtyping of function types --- README.md | 167 +++++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 140 insertions(+), 27 deletions(-) diff --git a/README.md b/README.md index 78b0f90..6ecbbf3 100644 --- a/README.md +++ b/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