luau-lang/luau
1
0
Fork 0
mirror of https://github.com/luau-lang/luau.git synced 2025-05-04 10:33:46 +01:00
Code Issues Projects Releases Packages Wiki Activity

WIP

Browse source
This commit is contained in:
ajeffrey@roblox.com 2022-04-22 19:04:21 -05:00
parent a767929546
commit 2e4f24f0f8
5 changed files with 126 additions and 62 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

44
prototyping/Luau/TypeCheck.agda
View file

@ -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

66
prototyping/Properties/OverloadedFunctions.agda
View file

@ -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 = {!!}

10
prototyping/Properties/StrictMode.agda
View file

@ -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))

65
prototyping/Properties/Subtyping.agda
View file

@ -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)

3
prototyping/Properties/TypeCheck.agda
View file

@ -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)