Boiled properties of function overloading down to 4 lemmas

prototyping/Luau/TypeCheck.agda

@@ -3,15 +3,18 @@
 module Luau.TypeCheck where
 
 open import Agda.Builtin.Equality using (_≡_)
+open import FFI.Data.Either using (Either; Left; Right)
 open import FFI.Data.Maybe using (Maybe; just)
 open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; number; bool; string; val; var; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; binexp; local_←_; _∙_; done; return; name; +; -; *; /; <; >; ==; ~=; <=; >=; ··)
 open import Luau.Var using (Var)
 open import Luau.Addr using (Addr)
 open import Luau.Heap using (Heap; Object; function_is_end) renaming (_[_] to _[_]ᴴ)
-open import Luau.Type using (Type; nil; unknown; number; boolean; string; _⇒_; src; tgt)
+open import Luau.Subtyping using (_≮:_; _<:_)
+open import Luau.Type using (Type; nil; never; unknown; number; boolean; string; _⇒_; _∪_; _∩_; src; tgt)
 open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)
 open import FFI.Data.Vector using (Vector)
 open import FFI.Data.Maybe using (Maybe; just; nothing)
+open import Properties.DecSubtyping using (dec-subtyping)
 open import Properties.Product using (_×_; _,_)
 
 orUnknown : Maybe Type → Type
@@ -44,6 +47,49 @@ tgtBinOp <= = boolean
 tgtBinOp >= = boolean
 tgtBinOp ·· = string
 
+-- (F ⋓ G) is a function type whose domain is the union of F's and G's domain
+-- and whose target is the union of F's and G's target.
+_⋓_ : Type → Type → Type
+(S ⇒ T) ⋓ (U ⇒ V) = (S ∪ U) ⇒ (T ∪ V)
+(S ⇒ T) ⋓ (U₁ ∪ U₂) = ((S ⇒ T) ⋓ U₁) ∪ ((S ⇒ T) ⋓ U₂)
+(S ⇒ T) ⋓ (U₁ ∩ U₂) = ((S ⇒ T) ⋓ U₁) ∩ ((S ⇒ T) ⋓ U₂)
+(S ⇒ T) ⋓ unknown = unknown
+(S ⇒ T) ⋓ nil = (S ⇒ T)
+(S ⇒ T) ⋓ never = (S ⇒ T)
+(S ⇒ T) ⋓ boolean = (S ⇒ T)
+(S ⇒ T) ⋓ number = (S ⇒ T)
+(S ⇒ T) ⋓ string = (S ⇒ T)
+(T₁ ∪ T₂) ⋓ U = (T₁ ⋓ U) ∪ (T₂ ⋓ U)
+(T₁ ∩ T₂) ⋓ U = (T₁ ⋓ U) ∩ (T₂ ⋓ U)
+unknown ⋓ U = unknown
+nil ⋓ U = U
+never ⋓ U = U
+boolean ⋓ U = U
+number ⋓ U = U
+string ⋓ U = U
+
+-- resolve F V is the result of applying a function of type F
+-- to an argument of type V. This does function overload resolution,
+-- e.g. `resolve (((number) -> string) & ((string) -> number)) (number)` is `string`.
+
+resolveFun : ∀{S V} → Either (V ≮: S) (V <: S) → Type → Type
+resolveFun (Left p) T = unknown
+resolveFun (Right p) T = T
+
+-- Honest this terminates, since each recursive call has
+-- fewer intersections, and otherwise we proceed by structural induction.
+{-# TERMINATING #-}
+resolve : Type → Type → Type
+resolve nil V = never
+resolve (S ⇒ T) V = resolveFun (dec-subtyping V S) T
+resolve never V = never
+resolve unknown V = unknown
+resolve boolean V = never
+resolve number V = never
+resolve string V = never
+resolve (F ∪ G) V = (resolve F V) ∪ (resolve G V)
+resolve (F ∩ G) V = ((resolve F V) ∩ (resolve G V)) ∩ (resolve (F ⋓ G) V)
+
 data _⊢ᴮ_∈_ : VarCtxt → Block yes → Type → Set
 data _⊢ᴱ_∈_ : VarCtxt → Expr yes → Type → Set
 
@@ -112,8 +158,8 @@ data _⊢ᴱ_∈_ where
 
     Γ ⊢ᴱ M ∈ T →
     Γ ⊢ᴱ N ∈ U →
-    ----------------------
+    ----------------------------
-    Γ ⊢ᴱ (M $ N) ∈ (tgt T)
+    Γ ⊢ᴱ (M $ N) ∈ (resolve T U)
 
   function : ∀ {f x B T U V Γ} →
 

prototyping/Properties/StrictMode.agda

@@ -12,7 +12,7 @@ open import Luau.Substitution using (_[_/_]ᴮ; _[_/_]ᴱ; _[_/_]ᴮunless_; var
 open import Luau.Subtyping using (_≮:_; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_; Tree; Language; ¬Language)
 open import Luau.Syntax using (Expr; yes; var; val; var_∈_; _⟨_⟩∈_; _$_; addr; number; bool; string; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name; ==; ~=)
 open import Luau.Type using (Type; nil; number; boolean; string; _⇒_; never; unknown; _∩_; _∪_; src; tgt; _≡ᵀ_; _≡ᴹᵀ_)
-open import Luau.TypeCheck using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; _⊢ᴴᴮ_▷_∈_; _⊢ᴴᴱ_▷_∈_; nil; var; addr; app; function; block; done; return; local; orUnknown; srcBinOp; tgtBinOp)
+open import Luau.TypeCheck using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; _⊢ᴴᴮ_▷_∈_; _⊢ᴴᴱ_▷_∈_; nil; var; addr; app; function; block; done; return; local; orUnknown; srcBinOp; tgtBinOp; resolve)
 open import Luau.Var using (_≡ⱽ_)
 open import Luau.Addr using (_≡ᴬ_)
 open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_; ⊕-lookup-miss; ⊕-swap; ⊕-over) renaming (_[_] to _[_]ⱽ)
@@ -22,12 +22,29 @@ open import Properties.Equality using (_≢_; sym; cong; trans; subst₁)
 open import Properties.Dec using (Dec; yes; no)
 open import Properties.Contradiction using (CONTRADICTION; ¬)
 open import Properties.Functions using (_∘_)
+open import Properties.DecSubtyping using (dec-subtyping)
 open import Properties.Subtyping using (unknown-≮:; ≡-trans-≮:; ≮:-trans-≡; never-tgt-≮:; tgt-never-≮:; src-unknown-≮:; unknown-src-≮:; ≮:-trans; ≮:-refl; scalar-≢-impl-≮:; function-≮:-scalar; scalar-≮:-function; function-≮:-never; unknown-≮:-scalar; scalar-≮:-never; unknown-≮:-never)
 open import Properties.TypeCheck using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴ)
 open import Luau.OpSem using (_⟦_⟧_⟶_; _⊢_⟶*_⊣_; _⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app₁; app₂; function; beta; return; block; done; local; subst; binOp₀; binOp₁; binOp₂; refl; step; +; -; *; /; <; >; ==; ~=; <=; >=; ··)
 open import Luau.RuntimeError using (BinOpError; RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; bin₁; bin₂; block; local; return; +; -; *; /; <; >; <=; >=; ··)
 open import Luau.RuntimeType using (RuntimeType; valueType; number; string; boolean; nil; function)
 
+-- PROVE THESE
+
+postulate
+  resolve⁻¹ : Type → Type → Type
+  resolve-≮:-⇒ : ∀ {F V U} → (resolve F V ≮: U) → (F ≮: (V ⇒ U))
+  ⇒-≮:-resolve : ∀ {F V U} → (F ≮: (V ⇒ U)) → (resolve F V ≮: U)
+  ⇒-≮:-resolve⁻¹ : ∀ {F V U} → (F ≮: (V ⇒ U)) → (V ≮: resolve⁻¹ F U)
+  resolve⁻¹-≮:-⇒ : ∀ {F V U} → (V ≮: resolve⁻¹ F U) → (F ≮: (V ⇒ U))
+
+resolve-⇒-≮: : ∀ {S T U V} → (T ≮: U) → resolve (S ⇒ T) V ≮: U
+resolve-⇒-≮: {S = S} {V = V} p with dec-subtyping V S
+resolve-⇒-≮: p | Left q = unknown-≮: p
+resolve-⇒-≮: p | Right q = p
+
+--
+
 data _⊑_ (H : Heap yes) : Heap yes → Set where
   refl : (H ⊑ H)
   snoc : ∀ {H′ a O} → (H′ ≡ᴴ H ⊕ a ↦ O) → (H ⊑ H′)
@@ -71,7 +88,7 @@ heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = b} q) p | no r = ≡-trans-≮:
 heap-weakeningᴱ Γ H (val (number x)) h p = p
 heap-weakeningᴱ Γ H (val (bool x)) h p = p
 heap-weakeningᴱ Γ H (val (string x)) h p = p
-heap-weakeningᴱ Γ H (M $ N) h p = never-tgt-≮: (heap-weakeningᴱ Γ H M h (tgt-never-≮: p))
+heap-weakeningᴱ Γ H (M $ N) h p = ⇒-≮:-resolve (resolve⁻¹-≮:-⇒ (heap-weakeningᴱ Γ H N h (⇒-≮:-resolve⁻¹ (heap-weakeningᴱ Γ H M h (resolve-≮:-⇒ p)))))
 heap-weakeningᴱ Γ H (function f ⟨ var x ∈ T ⟩∈ U is B end) h p = p
 heap-weakeningᴱ Γ H (block var b ∈ T is B end) h p = p
 heap-weakeningᴱ Γ H (binexp M op N) h p = p
@@ -92,7 +109,11 @@ substitutivityᴮ-unless-no : ∀ {Γ Γ′ T V} H B v x y (r : x ≢ y) → (Γ
 substitutivityᴱ H (var y) v x p = substitutivityᴱ-whenever H v x y (x ≡ⱽ y) p
 substitutivityᴱ H (val w) v x p = Left p
 substitutivityᴱ H (binexp M op N) v x p = Left p
-substitutivityᴱ H (M $ N) v x p = mapL never-tgt-≮: (substitutivityᴱ H M v x (tgt-never-≮: p))
+substitutivityᴱ H (M $ N) v x p with substitutivityᴱ H M v x (resolve-≮:-⇒ p) 
+substitutivityᴱ H (M $ N) v x p | Left q with substitutivityᴱ H N v x (⇒-≮:-resolve⁻¹ q)
+substitutivityᴱ H (M $ N) v x p | Left q | Left r = Left (⇒-≮:-resolve (resolve⁻¹-≮:-⇒ r))
+substitutivityᴱ H (M $ N) v x p | Left q | Right r = Right r
+substitutivityᴱ H (M $ N) v x p | Right q = Right q
 substitutivityᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p = Left p
 substitutivityᴱ H (block var b ∈ T is B end) v x p = Left p
 substitutivityᴱ-whenever H v x x (yes refl) q = swapLR (≮:-trans q)
@@ -123,9 +144,13 @@ binOpPreservation H (·· v w) = refl
 reflect-subtypingᴱ : ∀ H M {H′ M′ T} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → (typeOfᴱ H′ ∅ M′ ≮: T) → Either (typeOfᴱ H ∅ M ≮: T) (Warningᴱ H (typeCheckᴱ H ∅ M))
 reflect-subtypingᴮ : ∀ H B {H′ B′ T} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → (typeOfᴮ H′ ∅ B′ ≮: T) → Either (typeOfᴮ H ∅ B ≮: T) (Warningᴮ H (typeCheckᴮ H ∅ B))
 
-reflect-subtypingᴱ H (M $ N) (app₁ s) p = mapLR never-tgt-≮: app₁ (reflect-subtypingᴱ H M s (tgt-never-≮: p))
+reflect-subtypingᴱ H (M $ N) (app₁ s) p with reflect-subtypingᴱ H M s (resolve-≮:-⇒ p)
-reflect-subtypingᴱ H (M $ N) (app₂ v s) p = Left (never-tgt-≮: (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) (tgt-never-≮: p)))
+reflect-subtypingᴱ H (M $ N) (app₁ s) p | Left q = Left (⇒-≮:-resolve (resolve⁻¹-≮:-⇒ (heap-weakeningᴱ ∅ H N (rednᴱ⊑ s) (⇒-≮:-resolve⁻¹ q))))
-reflect-subtypingᴱ H (M $ N) (beta (function f ⟨ var y ∈ T ⟩∈ U is B end) v refl q) p = Left (≡-trans-≮: (cong tgt (cong orUnknown (cong typeOfᴹᴼ q))) p)
+reflect-subtypingᴱ H (M $ N) (app₁ s) p | Right W = Right (app₁ W)
+reflect-subtypingᴱ H (M $ N) (app₂ v s) p with reflect-subtypingᴱ H N s (⇒-≮:-resolve⁻¹ (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) (resolve-≮:-⇒ p)))
+reflect-subtypingᴱ H (M $ N) (app₂ v s) p | Left q = Left (⇒-≮:-resolve (resolve⁻¹-≮:-⇒ q))
+reflect-subtypingᴱ H (M $ N) (app₂ v s) p | Right W = Right (app₂ W)
+reflect-subtypingᴱ H (M $ N) {T = T} (beta (function f ⟨ var y ∈ S ⟩∈ U is B end) v refl q) p = Left (≡-trans-≮: (cong (λ F → resolve F (typeOfᴱ H ∅ N)) (cong orUnknown (cong typeOfᴹᴼ q))) (resolve-⇒-≮: p))
 reflect-subtypingᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) p = Left p
 reflect-subtypingᴱ H (block var b ∈ T is B end) (block s) p = Left p
 reflect-subtypingᴱ H (block var b ∈ T is return (val v) ∙ B end) (return v) p = mapR BlockMismatch (swapLR (≮:-trans p))

prototyping/Properties/TypeCheck.agda

@@ -6,7 +6,7 @@ open import Agda.Builtin.Equality using (_≡_; refl)
 open import Agda.Builtin.Bool using (Bool; true; false)
 open import FFI.Data.Maybe using (Maybe; just; nothing)
 open import FFI.Data.Either using (Either)
-open import Luau.TypeCheck using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; ⊢ᴼ_; ⊢ᴴ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; nil; var; addr; number; bool; string; app; function; block; binexp; done; return; local; nothing; orUnknown; tgtBinOp)
+open import Luau.TypeCheck using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; ⊢ᴼ_; ⊢ᴴ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; nil; var; addr; number; bool; string; app; function; block; binexp; done; return; local; nothing; orUnknown; tgtBinOp; resolve)
 open import Luau.Syntax using (Block; Expr; Value; BinaryOperator; yes; nil; addr; number; bool; string; val; var; binexp; _$_; function_is_end; block_is_end; _∙_; return; done; local_←_; _⟨_⟩; _⟨_⟩∈_; var_∈_; name; fun; arg; +; -; *; /; <; >; ==; ~=; <=; >=)
 open import Luau.Type using (Type; nil; unknown; never; number; boolean; string; _⇒_; src; tgt)
 open import Luau.RuntimeType using (RuntimeType; nil; number; function; string; valueType)
@@ -39,7 +39,7 @@ typeOfᴮ : Heap yes → VarCtxt → (Block yes) → Type
 
 typeOfᴱ H Γ (var x) = orUnknown(Γ [ x ]ⱽ)
 typeOfᴱ H Γ (val v) = orUnknown(typeOfⱽ H v)
-typeOfᴱ H Γ (M $ N) = tgt(typeOfᴱ H Γ M)
+typeOfᴱ H Γ (M $ N) = resolve (typeOfᴱ H Γ M) (typeOfᴱ H Γ N)
 typeOfᴱ H Γ (function f ⟨ var x ∈ S ⟩∈ T is B end) = S ⇒ T
 typeOfᴱ H Γ (block var b ∈ T is B end) = T
 typeOfᴱ H Γ (binexp M op N) = tgtBinOp op