diff --git a/prototyping/Luau/TypeCheck.agda b/prototyping/Luau/TypeCheck.agda index fc567edf..4a20c321 100644 --- a/prototyping/Luau/TypeCheck.agda +++ b/prototyping/Luau/TypeCheck.agda @@ -8,6 +8,7 @@ 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.OverloadedFunctions using (resolve) open import Luau.Heap using (Heap; Object; function_is_end) renaming (_[_] to _[_]ᴴ) open import Luau.Subtyping using (_≮:_; _<:_) open import Luau.Type using (Type; nil; never; unknown; number; boolean; string; _⇒_; _∪_; _∩_; src; tgt) @@ -47,49 +48,6 @@ 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 diff --git a/prototyping/Properties/OverloadedFunctions.agda b/prototyping/Properties/OverloadedFunctions.agda index 2ba21e80..e8ceaeaf 100644 --- a/prototyping/Properties/OverloadedFunctions.agda +++ b/prototyping/Properties/OverloadedFunctions.agda @@ -4,11 +4,11 @@ module Properties.OverloadedFunctions where open import FFI.Data.Either using (Either; Left; Right) open import Luau.OverloadedFunctions using (resolve) -open import Luau.Subtyping using (_<:_; _≮:_) +open import Luau.Subtyping using (_<:_; _≮:_; witness; _,_; left; right) open import Luau.Type using (Type; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; src) open import Properties.Contradiction using (CONTRADICTION) open import Properties.DecSubtyping using (dec-subtyping) -open import Properties.Subtyping using (<:-refl; <:-trans; <:-union; <:-∪-left; <:-∪-right; <:-∪-lub; <:-intersect; <:-∩-left; <:-∩-right; <:-∩-glb; <:-impl-¬≮:; <:-function; <:-never; <:-never-left; <:-never-right; <:-function-∩; <:-function-∩-∪; <:-∩-dist-∪) +open import Properties.Subtyping using (<:-refl; <:-trans; <:-union; <:-∪-left; <:-∪-right; <:-∪-lub; <:-intersect; <:-∩-left; <:-∩-right; <:-∩-glb; <:-impl-¬≮:; <:-function; <:-never; <:-never-left; <:-never-right; <:-function-∩; <:-function-∩-∪; <:-∩-dist-∪; <:-trans-≮:; never-≮:; ≮:-∩-left; ≮:-∩-right; ≮:-∪-left; ≮:-∪-right) -- Function overload resolution respects subtyping @@ -49,3 +49,65 @@ resolve-intro (F ∩ G) V p₁ p₂ | Left q₁ | Left q₂ = <:-trans (<:-inter resolve-intro (F ∩ G) V p₁ p₂ | Left q₁ | Right q₂ = <:-trans <:-∩-right (resolve-intro G V p₁ q₂) resolve-intro (F ∩ G) V p₁ p₂ | Right q₁ | Left q₂ = <:-trans <:-∩-left (resolve-intro F V p₁ q₁) resolve-intro (F ∩ G) V p₁ p₂ | Right q₁ | Right q₂ = <:-trans (<:-intersect (resolve-intro F V p₁ q₁) (resolve-intro G V p₁ q₂)) <:-function-∩ + +resolve⁻¹ : Type → Type → Type +resolve⁻¹ nil U = unknown +resolve⁻¹ (S ⇒ T) U with dec-subtyping T U +resolve⁻¹ (S ⇒ T) U | Left p = never +resolve⁻¹ (S ⇒ T) U | Right p = S +resolve⁻¹ never U = {!!} +resolve⁻¹ unknown U = {!!} +resolve⁻¹ boolean U = {!!} +resolve⁻¹ number U = {!!} +resolve⁻¹ string U = {!!} +resolve⁻¹ (F ∪ G) U = resolve⁻¹ F U ∩ resolve⁻¹ G U +resolve⁻¹ (F ∩ G) U = {!!} + +uuu : ∀ F U → (resolve⁻¹ F U <: src F) +uuu = ? + +www : ∀ F U V → (V ≮: never) → (V <: src F) → (resolve F V ≮: U) → (V ≮: resolve⁻¹ F U) +www nil U V p q w = CONTRADICTION (<:-impl-¬≮: <:-never w) +www (S ⇒ T) U V p q w with dec-subtyping T U +www (S ⇒ T) U V p q w | Left r = p +www (S ⇒ T) U V p q w | Right r = CONTRADICTION (<:-impl-¬≮: r w) +www never U V p q w = {!!} +www unknown U V p q w = {!!} +www boolean U V p q w = {!!} +www number U V p q w = {!!} +www string U V p q w = {!!} +www (F ∪ G) U V p q w = {!!} +www (F ∩ G) U V p q w with dec-subtyping V (src F) | dec-subtyping V (src G) +www (F ∩ G) U V p q w | Left r₁ | Left r₂ = {!!} +www (F ∩ G) U V p q w | Left r₁ | Right x = {!!} +www (F ∩ G) U V p q w | Right x | y = {!!} + +xxx : ∀ F U V → (V ≮: never) → (resolve F V ≮: U) → (V ≮: resolve⁻¹ F U) +xxx nil U V p q = CONTRADICTION (<:-impl-¬≮: <:-never q) +xxx (S ⇒ T) U V p q with dec-subtyping T U +xxx (S ⇒ T) U V p q | Left r = p +xxx (S ⇒ T) U V p q | Right r = CONTRADICTION (<:-impl-¬≮: r q) +xxx never U V p q = {!!} +xxx unknown U V p q = {!!} +xxx boolean U V p q = {!!} +xxx number U V p q = {!!} +xxx string U V p q = {!!} +xxx (F ∪ G) U V p (witness t (left q) r) = ≮:-∩-left (xxx F U V p (witness t q r)) +xxx (F ∪ G) U V p (witness t (right q) r) = ≮:-∩-right (xxx G U V p (witness t q r)) +xxx (F ∩ G) U V p q with dec-subtyping V (src F) | dec-subtyping V (src G) +xxx (F ∩ G) U V p (witness t (left q₁) q₂) | Left r₁ | Left r₂ = {!xxx F U V p (witness t q₁ q₂)!} +xxx (F ∩ G) U V p (witness t (right q₁) q₂) | Left r₁ | Left r₂ = {!!} +xxx (F ∩ G) U V p q | Left r₁ | Right r₂ = {!!} +xxx (F ∩ G) U V p q | Right x | r₃ = {!!} + +yyy : ∀ F U V → (V ≮: resolve⁻¹ F U) → (resolve F V ≮: U) +yyy nil U V w = {!w!} +yyy (S ⇒ T) U V w = {!!} +yyy never U V w = {!!} +yyy unknown U V w = {!!} +yyy boolean U V w = {!!} +yyy number U V w = {!!} +yyy string U V w = {!!} +yyy (F ∪ G) U V (witness t p (left r)) = ≮:-∪-left (yyy F U V (witness t p r)) +yyy (F ∪ G) U V (witness t p (right r)) = ≮:-∪-right (yyy G U V (witness t p r)) +yyy (F ∩ F₁) U V w = {!!} diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda index 30732cac..9f5c449a 100644 --- a/prototyping/Properties/StrictMode.agda +++ b/prototyping/Properties/StrictMode.agda @@ -12,11 +12,12 @@ 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; resolve) +open import Luau.TypeCheck using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; _⊢ᴴᴮ_▷_∈_; _⊢ᴴᴱ_▷_∈_; nil; var; addr; app; function; block; done; return; local; orUnknown; srcBinOp; tgtBinOp) open import Luau.Var using (_≡ⱽ_) open import Luau.Addr using (_≡ᴬ_) open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_; ⊕-lookup-miss; ⊕-swap; ⊕-over) renaming (_[_] to _[_]ⱽ) open import Luau.VarCtxt using (VarCtxt; ∅) +open import Luau.OverloadedFunctions using (resolve) open import Properties.Remember using (remember; _,_) open import Properties.Equality using (_≢_; sym; cong; trans; subst₁) open import Properties.Dec using (Dec; yes; no) @@ -38,11 +39,6 @@ postulate ⇒-≮:-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 @@ -150,7 +146,7 @@ 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 (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))) 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)) diff --git a/prototyping/Properties/Subtyping.agda b/prototyping/Properties/Subtyping.agda index b628adf5..bf16d82e 100644 --- a/prototyping/Properties/Subtyping.agda +++ b/prototyping/Properties/Subtyping.agda @@ -40,7 +40,10 @@ open import Properties.Product using (_×_; _,_) ≮:-trans {T = T} (witness t p q) = mapLR (witness t p) (λ z → witness t z q) (dec-language T t) <:-trans : ∀ {S T U} → (S <: T) → (T <: U) → (S <: U) -<:-trans p q = ¬≮:-impl-<: (cond (<:-impl-¬≮: p) (<:-impl-¬≮: q) ∘ ≮:-trans) +<:-trans p q t r = q t (p t r) + +<:-trans-≮: : ∀ {S T U} → (S <: T) → (S ≮: U) → (T ≮: U) +<:-trans-≮: p (witness t q r) = witness t (p t q) r -- Properties of union @@ -58,6 +61,12 @@ open import Properties.Product using (_×_; _,_) <:-∪-lub p q t (left r) = p t r <:-∪-lub p q t (right r) = q t r +≮:-∪-left : ∀ {S T U} → (S ≮: U) → ((S ∪ T) ≮: U) +≮:-∪-left (witness t p q) = witness t (left p) q + +≮:-∪-right : ∀ {S T U} → (T ≮: U) → ((S ∪ T) ≮: U) +≮:-∪-right (witness t p q) = witness t (right p) q + -- Properties of intersection <:-intersect : ∀ {R S T U} → (R <: T) → (S <: U) → ((R ∩ S) <: (T ∩ U)) @@ -72,10 +81,30 @@ open import Properties.Product using (_×_; _,_) <:-∩-glb : ∀ {S T U} → (S <: T) → (S <: U) → (S <: (T ∩ U)) <:-∩-glb p q t r = (p t r , q t r) +≮:-∩-left : ∀ {S T U} → (S ≮: T) → (S ≮: (T ∩ U)) +≮:-∩-left (witness t p q) = witness t p (left q) + +≮:-∩-right : ∀ {S T U} → (S ≮: U) → (S ≮: (T ∩ U)) +≮:-∩-right (witness t p q) = witness t p (right q) + +-- Distribution properties <:-∩-dist-∪ : ∀ {S T U} → (S ∩ (T ∪ U)) <: ((S ∩ T) ∪ (S ∩ U)) <:-∩-dist-∪ t (p₁ , left p₂) = left (p₁ , p₂) <:-∩-dist-∪ t (p₁ , right p₂) = right (p₁ , p₂) +∩-dist-∪-<: : ∀ {S T U} → ((S ∩ T) ∪ (S ∩ U)) <: (S ∩ (T ∪ U)) +∩-dist-∪-<: t (left (p₁ , p₂)) = (p₁ , left p₂) +∩-dist-∪-<: t (right (p₁ , p₂)) = (p₁ , right p₂) + +<:-∪-dist-∩ : ∀ {S T U} → (S ∪ (T ∩ U)) <: ((S ∪ T) ∩ (S ∪ U)) +<:-∪-dist-∩ t (left p) = (left p , left p) +<:-∪-dist-∩ t (right (p₁ , p₂)) = (right p₁ , right p₂) + +∪-dist-∩-<: : ∀ {S T U} → ((S ∪ T) ∩ (S ∪ U)) <: (S ∪ (T ∩ U)) +∪-dist-∩-<: t (left p₁ , p₂) = left p₁ +∪-dist-∩-<: t (right p₁ , left p₂) = left p₂ +∪-dist-∩-<: t (right p₁ , right p₂) = right (p₁ , p₂) + -- Properties of functions <:-function : ∀ {R S T U} → (R <: S) → (T <: U) → (S ⇒ T) <: (R ⇒ U) <:-function p q function function = function @@ -97,6 +126,15 @@ open import Properties.Product using (_×_; _,_) <:-function-∩ (function-ok s t) (function-ok₂ p₁ , function-ok₂ p₂) = function-ok₂ (p₁ , p₂) <:-function-∩ (function-err s) (function-err p₁ , function-err p₂) = function-err p₂ +<:-function-∪-∩ : ∀ {R S T U} → ((R ∩ S) ⇒ (T ∪ U)) <: ((R ⇒ T) ∪ (S ⇒ U)) +<:-function-∪-∩ function function = left function +<:-function-∪-∩ (function-ok s t) (function-ok₁ (left p)) = left (function-ok₁ p) +<:-function-∪-∩ (function-ok s t) (function-ok₁ (right p)) = right (function-ok₁ p) +<:-function-∪-∩ (function-ok s t) (function-ok₂ (left p)) = left (function-ok₂ p) +<:-function-∪-∩ (function-ok s t) (function-ok₂ (right p)) = right (function-ok₂ p) +<:-function-∪-∩ (function-err s) (function-err (left p)) = left (function-err p) +<:-function-∪-∩ (function-err s) (function-err (right p)) = right (function-err p) + -- Properties of scalars skalar = number ∪ (string ∪ (nil ∪ boolean)) @@ -160,15 +198,24 @@ function-≮:-never = witness function function never <:-never t (scalar ()) <:-never t (scalar-function-err ()) -<:-never-left : ∀ {S T U} → (S <: (T ∪ U)) → (S ≮: T) → (S ∩ U) ≮: never -<:-never-left p (witness t q₁ q₂) with p t q₁ -<:-never-left p (witness t q₁ q₂) | left r = CONTRADICTION (language-comp t q₂ r) -<:-never-left p (witness t q₁ q₂) | right r = witness t (q₁ , r) never +≮:-never-left : ∀ {S T U} → (S <: (T ∪ U)) → (S ≮: T) → (S ∩ U) ≮: never +≮:-never-left p (witness t q₁ q₂) with p t q₁ +≮:-never-left p (witness t q₁ q₂) | left r = CONTRADICTION (language-comp t q₂ r) +≮:-never-left p (witness t q₁ q₂) | right r = witness t (q₁ , r) never -<:-never-right : ∀ {S T U} → (S <: (T ∪ U)) → (S ≮: U) → (S ∩ T) ≮: never -<:-never-right p (witness t q₁ q₂) with p t q₁ -<:-never-right p (witness t q₁ q₂) | left r = witness t (q₁ , r) never -<:-never-right p (witness t q₁ q₂) | right r = CONTRADICTION (language-comp t q₂ r) +≮:-never-right : ∀ {S T U} → (S <: (T ∪ U)) → (S ≮: U) → (S ∩ T) ≮: never +≮:-never-right p (witness t q₁ q₂) with p t q₁ +≮:-never-right p (witness t q₁ q₂) | left r = witness t (q₁ , r) never +≮:-never-right p (witness t q₁ q₂) | right r = CONTRADICTION (language-comp t q₂ r) + +<:-unknown : ∀ {T} → (T <: unknown) +<:-unknown t p = unknown + +<:-everything : unknown <: ((never ⇒ unknown) ∪ skalar) +<:-everything (scalar s) p = right (skalar-scalar s) +<:-everything function p = left function +<:-everything (function-ok s t) p = left (function-ok₁ never) +<:-everything (function-err s) p = left (function-err never) -- A Gentle Introduction To Semantic Subtyping (https://www.cduce.org/papers/gentle.pdf) -- defines a "set-theoretic" model (sec 2.5) diff --git a/prototyping/Properties/TypeCheck.agda b/prototyping/Properties/TypeCheck.agda index ae70b7cb..f2bc2497 100644 --- a/prototyping/Properties/TypeCheck.agda +++ b/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; resolve) +open import Luau.TypeCheck using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; ⊢ᴼ_; ⊢ᴴ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; nil; var; addr; number; bool; string; app; function; block; binexp; done; return; local; nothing; orUnknown; tgtBinOp) 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) @@ -14,6 +14,7 @@ open import Luau.VarCtxt using (VarCtxt; ∅; _↦_; _⊕_↦_; _⋒_; _⊝_) re open import Luau.Addr using (Addr) open import Luau.Var using (Var; _≡ⱽ_) open import Luau.Heap using (Heap; Object; function_is_end) renaming (_[_] to _[_]ᴴ) +open import Luau.OverloadedFunctions using (resolve) open import Properties.Contradiction using (CONTRADICTION) open import Properties.Dec using (yes; no) open import Properties.Equality using (_≢_; sym; trans; cong)