67 lines
2.5 KiB
Agda
67 lines
2.5 KiB
Agda
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₂)
|
||
F₁ ⋓ (F₂ ∩ G₂) = (F₁ ⋓ F₂) ∩ (F₁ ⋓ G₂)
|
||
F ⋓ G = F ∩ G
|
||
|
||
_⋒_ : Type → Type → Type
|
||
(S₁ ⇒ T₁) ⋒ (S₂ ⇒ T₂) = (S₁ ∩ⁿ S₂) ⇒ (T₁ ∩ⁿ T₂)
|
||
(F₁ ∩ G₁) ⋒ F₂ = (F₁ ⋒ F₂) ∩ (G₁ ⋒ F₂)
|
||
F₁ ⋒ (F₂ ∩ G₂) = (F₁ ⋒ F₂) ∩ (F₁ ⋒ G₂)
|
||
F ⋒ G = F ∩ G
|
||
|
||
_∩ᵘ_ : Type → Type → Type
|
||
F ∩ᵘ G = (F ∩ G) ∩ (F ⋓ G)
|
||
|
||
_∩ⁱ_ : Type → Type → Type
|
||
F ∩ⁱ G = (F ∩ G) ∩ (F ⋒ G)
|
||
|
||
∪-saturate : Type → Type
|
||
∪-saturate (F ∩ G) = (∪-saturate F ∩ᵘ ∪-saturate G)
|
||
∪-saturate F = F
|
||
|
||
∩-saturate : Type → Type
|
||
∩-saturate (F ∩ G) = (∩-saturate F ∩ⁱ ∩-saturate G)
|
||
∩-saturate F = F
|
||
|
||
saturate : Type → Type
|
||
saturate F = ∪-saturate (∩-saturate F)
|