WIP

prototyping/Luau/TypeSaturation.agda

@@ -3,6 +3,39 @@ module Luau.TypeSaturation where
 open import Luau.Type using (Type; _⇒_; _∩_; _∪_)
 open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_)
 
+-- So, there's a problem with overloaded functions
+-- (of the form (S_1 ⇒ T_1) ∩⋯∩ (S_n ⇒ T_n))
+-- which is that it's not good enough to compare them
+-- for subtyping by comparing all of their overloads.
+
+-- For example (nil → nil) is a subtype of (number? → number?) ∩ (string? → string?)
+-- but not a subtype of any of its overloads.
+
+-- To fix this, we adapt the semantic subtyping algorithm for
+-- function types, given in
+-- https://www.irif.fr/~gc/papers/covcon-again.pdf and
+-- https://pnwamk.github.io/sst-tutorial/
+
+-- A function type is *intersection-saturated* if for any overloads
+-- (S₁ ⇒ T₁) and (S₂ ⇒ T₂), there exists an overload which is a subtype
+-- of ((S₁ ∩ S₂) ⇒ (T₁ ∩ T₂)).
+
+-- A function type is *union-saturated* if for any overloads
+-- (S₁ ⇒ T₁) and (S₂ ⇒ T₂), there exists an overload which is a subtype
+-- of ((S₁ ∪ S₂) ⇒ (T₁ ∪ T₂)).
+
+-- A function type is *saturated* if it is both intersection- and
+-- union-saturated.
+
+-- For example (number? → number?) ∩ (string? → string?)
+-- is not saturated, but (number? → number?) ∩ (string? → string?) ∩ (nil → nil) ∩ ((number ∪ string)? → (number ∪ string)?)
+-- is.
+
+-- Saturated function types have the nice property that they can ber
+-- compared by just comparing their overloads: F <: G whenever for any
+-- overload of G, there is an overload os F which is a subtype of it.
+
+-- Forunately every function type can be saturated!
 _⋓_ : Type → Type → Type
 (S₁ ⇒ T₁) ⋓ (S₂ ⇒ T₂) = (S₁ ∪ⁿ S₂) ⇒ (T₁ ∪ⁿ T₂)
 (F₁ ∩ G₁) ⋓ F₂ = (F₁ ⋓ F₂) ∩ (G₁ ⋓ F₂)