Prototyping type normalizaton (#466)

* Added type normalization

prototyping/Luau/FunctionTypes.agda

@@ -0,0 +1,38 @@
+{-# OPTIONS --rewriting #-}
+
+open import FFI.Data.Either using (Either; Left; Right)
+open import Luau.Type using (Type; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
+open import Luau.TypeNormalization using (normalize)
+
+module Luau.FunctionTypes where
+
+-- The domain of a normalized type
+srcⁿ : Type → Type
+srcⁿ (S ⇒ T) = S
+srcⁿ (S ∩ T) = srcⁿ S ∪ srcⁿ T
+srcⁿ never = unknown
+srcⁿ T = never
+
+-- To get the domain of a type, we normalize it first We need to do
+-- this, since if we try to use it on non-normalized types, we get
+--
+-- src(number ∩ string) = src(number) ∪ src(string) = never ∪ never
+-- src(never) = unknown
+--
+-- so src doesn't respect type equivalence.
+src : Type → Type
+src (S ⇒ T) = S
+src T = srcⁿ(normalize T)
+
+-- The codomain of a type
+tgt : Type → Type
+tgt nil = never
+tgt (S ⇒ T) = T
+tgt never = never
+tgt unknown = unknown
+tgt number = never
+tgt boolean = never
+tgt string = never
+tgt (S ∪ T) = (tgt S) ∪ (tgt T)
+tgt (S ∩ T) = (tgt S) ∩ (tgt T)
+

prototyping/Luau/StrictMode.agda

@@ -5,7 +5,8 @@ module Luau.StrictMode where
 open import Agda.Builtin.Equality using (_≡_)
 open import FFI.Data.Maybe using (just; nothing)
 open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; var; binexp; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; +; -; *; /; <; >; <=; >=; ··)
-open import Luau.Type using (Type; nil; number; string; boolean; _⇒_; _∪_; _∩_; src; tgt)
+open import Luau.FunctionTypes using (src; tgt)
+open import Luau.Type using (Type; nil; number; string; boolean; _⇒_; _∪_; _∩_)
 open import Luau.Subtyping using (_≮:_)
 open import Luau.Heap using (Heap; function_is_end) renaming (_[_] to _[_]ᴴ)
 open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)

prototyping/Luau/Subtyping.agda

@@ -25,7 +25,6 @@ data Language where
   function : ∀ {T U} → Language (T ⇒ U) function
   function-ok : ∀ {T U u} → (Language U u) → Language (T ⇒ U) (function-ok u)
   function-err : ∀ {T U t} → (¬Language T t) → Language (T ⇒ U) (function-err t)
-  scalar-function-err : ∀ {S t} → (Scalar S) → Language S (function-err t)
   left : ∀ {T U t} → Language T t → Language (T ∪ U) t
   right : ∀ {T U u} → Language U u → Language (T ∪ U) u
   _,_ : ∀ {T U t} → Language T t → Language U t → Language (T ∩ U) t
@@ -36,6 +35,7 @@ data ¬Language where
   scalar-scalar : ∀ {S T} → (s : Scalar S) → (Scalar T) → (S ≢ T) → ¬Language T (scalar s)
   scalar-function : ∀ {S} → (Scalar S) → ¬Language S function
   scalar-function-ok : ∀ {S u} → (Scalar S) → ¬Language S (function-ok u)
+  scalar-function-err : ∀ {S t} → (Scalar S) → ¬Language S (function-err t)
   function-scalar : ∀ {S T U} (s : Scalar S) → ¬Language (T ⇒ U) (scalar s)
   function-ok : ∀ {T U u} → (¬Language U u) → ¬Language (T ⇒ U) (function-ok u)
   function-err : ∀ {T U t} → (Language T t) → ¬Language (T ⇒ U) (function-err t)

prototyping/Luau/Type.agda

@@ -24,6 +24,8 @@ data Scalar : Type → Set where
   string : Scalar string
   nil : Scalar nil
 
+skalar = number ∪ (string ∪ (nil ∪ boolean))
+
 lhs : Type → Type
 lhs (T ⇒ _) = T
 lhs (T ∪ _) = T
@@ -146,28 +148,6 @@ just T ≡ᴹᵀ just U with T ≡ᵀ U
 (just T ≡ᴹᵀ just T) | yes refl = yes refl
 (just T ≡ᴹᵀ just U) | no p = no (λ q → p (just-inv q))
 
-src : Type → Type
-src nil = never
-src number = never
-src boolean = never
-src string = never
-src (S ⇒ T) = S
-src (S ∪ T) = (src S) ∩ (src T)
-src (S ∩ T) = (src S) ∪ (src T)
-src never = unknown
-src unknown = never
-
-tgt : Type → Type
-tgt nil = never
-tgt (S ⇒ T) = T
-tgt never = never
-tgt unknown = unknown
-tgt number = never
-tgt boolean = never
-tgt string = never
-tgt (S ∪ T) = (tgt S) ∪ (tgt T)
-tgt (S ∩ T) = (tgt S) ∩ (tgt T)
-
 optional : Type → Type
 optional nil = nil
 optional (T ∪ nil) = (T ∪ nil)

prototyping/Luau/TypeCheck.agda

@@ -7,8 +7,9 @@ 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.FunctionTypes using (src; tgt)
 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.Type using (Type; nil; unknown; number; boolean; string; _⇒_)
 open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)
 open import FFI.Data.Vector using (Vector)
 open import FFI.Data.Maybe using (Maybe; just; nothing)

prototyping/Luau/TypeNormalization.agda

@@ -0,0 +1,69 @@
+module Luau.TypeNormalization where
+
+open import Luau.Type using (Type; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
+
+-- The top non-function type
+¬function : Type
+¬function = number ∪ (string ∪ (nil ∪ boolean))
+
+-- Unions and intersections of normalized types
+_∪ᶠ_ : Type → Type → Type
+_∪ⁿˢ_ : Type → Type → Type
+_∩ⁿˢ_ : Type → Type → Type
+_∪ⁿ_ : Type → Type → Type
+_∩ⁿ_ : Type → Type → Type
+
+-- Union of function types
+(F₁ ∩ F₂) ∪ᶠ G = (F₁ ∪ᶠ G) ∩ (F₂ ∪ᶠ G)
+F ∪ᶠ (G₁ ∩ G₂) = (F ∪ᶠ G₁) ∩ (F ∪ᶠ G₂)
+(R ⇒ S) ∪ᶠ (T ⇒ U) = (R ∩ⁿ T) ⇒ (S ∪ⁿ U)
+F ∪ᶠ G = F ∪ G
+
+-- Union of normalized types
+S ∪ⁿ (T₁ ∪ T₂) = (S ∪ⁿ T₁) ∪ T₂
+S ∪ⁿ unknown = unknown
+S ∪ⁿ never = S
+unknown ∪ⁿ T = unknown
+never ∪ⁿ T = T
+(S₁ ∪ S₂) ∪ⁿ G = (S₁ ∪ⁿ G) ∪ S₂
+F ∪ⁿ G = F ∪ᶠ G
+
+-- Intersection of normalized types
+S ∩ⁿ (T₁ ∪ T₂) = (S ∩ⁿ T₁) ∪ⁿˢ (S ∩ⁿˢ T₂)
+S ∩ⁿ unknown = S
+S ∩ⁿ never = never
+(S₁ ∪ S₂) ∩ⁿ G = (S₁ ∩ⁿ G)
+unknown ∩ⁿ G = G
+never ∩ⁿ G = never
+F ∩ⁿ G = F ∩ G
+
+-- Intersection of normalized types with a scalar
+(S₁ ∪ nil) ∩ⁿˢ nil = nil
+(S₁ ∪ boolean) ∩ⁿˢ boolean = boolean
+(S₁ ∪ number) ∩ⁿˢ number = number
+(S₁ ∪ string) ∩ⁿˢ string = string
+(S₁ ∪ S₂) ∩ⁿˢ T = S₁ ∩ⁿˢ T
+unknown ∩ⁿˢ T = T
+F ∩ⁿˢ T = never
+
+-- Union of normalized types with an optional scalar
+S ∪ⁿˢ never = S
+unknown ∪ⁿˢ T = unknown
+(S₁ ∪ nil) ∪ⁿˢ nil = S₁ ∪ nil
+(S₁ ∪ boolean) ∪ⁿˢ boolean = S₁ ∪ boolean
+(S₁ ∪ number) ∪ⁿˢ number = S₁ ∪ number
+(S₁ ∪ string) ∪ⁿˢ string = S₁ ∪ string
+(S₁ ∪ S₂) ∪ⁿˢ T = (S₁ ∪ⁿˢ T) ∪ S₂
+F ∪ⁿˢ T = F ∪ T
+
+-- Normalize!
+normalize : Type → Type
+normalize nil = never ∪ nil
+normalize (S ⇒ T) = (normalize S ⇒ normalize T)
+normalize never = never
+normalize unknown = unknown
+normalize boolean = never ∪ boolean
+normalize number = never ∪ number
+normalize string = never ∪ string
+normalize (S ∪ T) = normalize S ∪ⁿ normalize T
+normalize (S ∩ T) = normalize S ∩ⁿ normalize T

prototyping/Properties.agda

@@ -4,10 +4,13 @@ module Properties where
 
 import Properties.Contradiction
 import Properties.Dec
+import Properties.DecSubtyping
 import Properties.Equality
 import Properties.Functions
+import Properties.FunctionTypes
 import Properties.Remember
 import Properties.Step
 import Properties.StrictMode
 import Properties.Subtyping
 import Properties.TypeCheck
+import Properties.TypeNormalization

prototyping/Properties/DecSubtyping.agda

@@ -0,0 +1,70 @@
+{-# OPTIONS --rewriting #-}
+
+module Properties.DecSubtyping where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond)
+open import Luau.FunctionTypes using (src; srcⁿ; tgt)
+open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_)
+open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
+open import Properties.Contradiction using (CONTRADICTION; ¬)
+open import Properties.Functions using (_∘_)
+open import Properties.Subtyping using (<:-refl; <:-trans; ≮:-trans-<:; <:-trans-≮:; <:-never; <:-unknown; <:-∪-left; <:-∪-right; <:-∪-lub;  ≮:-∪-left; ≮:-∪-right; <:-∩-left; <:-∩-right; <:-∩-glb;  ≮:-∩-left; ≮:-∩-right; dec-language; scalar-<:; <:-everything; <:-function; ≮:-function-left; ≮:-function-right)
+open import Properties.TypeNormalization using (FunType; Normal; never; unknown; _∩_; _∪_; _⇒_; normal; <:-normalize; normalize-<:)
+open import Properties.FunctionTypes using (fun-¬scalar; ¬fun-scalar; fun-function; src-unknown-≮:; tgt-never-≮:; src-tgtᶠ-<:)
+open import Properties.Equality using (_≢_)
+
+-- Honest this terminates, since src and tgt reduce the depth of nested arrows
+{-# TERMINATING #-}
+dec-subtypingˢⁿ : ∀ {T U} → Scalar T → Normal U → Either (T ≮: U) (T <: U)
+dec-subtypingᶠ : ∀ {T U} → FunType T → FunType U → Either (T ≮: U) (T <: U)
+dec-subtypingᶠⁿ : ∀ {T U} → FunType T → Normal U → Either (T ≮: U) (T <: U)
+dec-subtypingⁿ : ∀ {T U} → Normal T → Normal U → Either (T ≮: U) (T <: U)
+dec-subtyping : ∀ T U → Either (T ≮: U) (T <: U)
+
+dec-subtypingˢⁿ T U with dec-language _ (scalar T)
+dec-subtypingˢⁿ T U | Left p = Left (witness (scalar T) (scalar T) p)
+dec-subtypingˢⁿ T U | Right p = Right (scalar-<: T p)
+
+dec-subtypingᶠ {T = T} _ (U ⇒ V) with dec-subtypingⁿ U (normal (src T)) | dec-subtypingⁿ (normal (tgt T)) V
+dec-subtypingᶠ {T = T} _ (U ⇒ V) | Left p | q = Left (≮:-trans-<: (src-unknown-≮: (≮:-trans-<: p (<:-normalize (src T)))) (<:-function <:-refl <:-unknown))
+dec-subtypingᶠ {T = T} _ (U ⇒ V) | Right p | Left q = Left (≮:-trans-<: (tgt-never-≮: (<:-trans-≮: (normalize-<: (tgt T)) q)) (<:-trans (<:-function <:-never <:-refl) <:-∪-right))
+dec-subtypingᶠ T (U ⇒ V) | Right p | Right q = Right (src-tgtᶠ-<: T (<:-trans p (normalize-<: _)) (<:-trans (<:-normalize _) q))
+
+dec-subtypingᶠ T (U ∩ V) with dec-subtypingᶠ T U | dec-subtypingᶠ T V
+dec-subtypingᶠ T (U ∩ V) | Left p | q = Left (≮:-∩-left p)
+dec-subtypingᶠ T (U ∩ V) | Right p | Left q = Left (≮:-∩-right q)
+dec-subtypingᶠ T (U ∩ V) | Right p | Right q = Right (<:-∩-glb p q)
+
+dec-subtypingᶠⁿ T never = Left (witness function (fun-function T) never)
+dec-subtypingᶠⁿ T unknown = Right <:-unknown
+dec-subtypingᶠⁿ T (U ⇒ V) = dec-subtypingᶠ T (U ⇒ V)
+dec-subtypingᶠⁿ T (U ∩ V) = dec-subtypingᶠ T (U ∩ V)
+dec-subtypingᶠⁿ T (U ∪ V) with dec-subtypingᶠⁿ T U
+dec-subtypingᶠⁿ T (U ∪ V) | Left (witness t p q) = Left (witness t p (q , ¬fun-scalar V T p))
+dec-subtypingᶠⁿ T (U ∪ V) | Right p = Right (<:-trans p <:-∪-left)
+
+dec-subtypingⁿ never U = Right <:-never
+dec-subtypingⁿ unknown unknown = Right <:-refl
+dec-subtypingⁿ unknown U with dec-subtypingᶠⁿ (never ⇒ unknown) U
+dec-subtypingⁿ unknown U | Left p = Left (<:-trans-≮: <:-unknown p)
+dec-subtypingⁿ unknown U | Right p₁ with dec-subtypingˢⁿ number U
+dec-subtypingⁿ unknown U | Right p₁ | Left p = Left (<:-trans-≮: <:-unknown p)
+dec-subtypingⁿ unknown U | Right p₁ | Right p₂ with dec-subtypingˢⁿ string U
+dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Left p = Left (<:-trans-≮: <:-unknown p)
+dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ with dec-subtypingˢⁿ nil U
+dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Left p = Left (<:-trans-≮: <:-unknown p)
+dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Right p₄ with dec-subtypingˢⁿ boolean U
+dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Right p₄ | Left p = Left (<:-trans-≮: <:-unknown p)
+dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Right p₄ | Right p₅ = Right (<:-trans <:-everything (<:-∪-lub p₁ (<:-∪-lub p₂ (<:-∪-lub p₃ (<:-∪-lub p₄ p₅)))))
+dec-subtypingⁿ (S ⇒ T) U = dec-subtypingᶠⁿ (S ⇒ T) U
+dec-subtypingⁿ (S ∩ T) U = dec-subtypingᶠⁿ (S ∩ T) U
+dec-subtypingⁿ (S ∪ T) U with dec-subtypingⁿ S U | dec-subtypingˢⁿ T U
+dec-subtypingⁿ (S ∪ T) U | Left p | q = Left (≮:-∪-left p)
+dec-subtypingⁿ (S ∪ T) U | Right p | Left q = Left (≮:-∪-right q)
+dec-subtypingⁿ (S ∪ T) U | Right p | Right q = Right (<:-∪-lub p q)
+
+dec-subtyping T U with dec-subtypingⁿ (normal T) (normal U)
+dec-subtyping T U | Left p = Left (<:-trans-≮: (normalize-<: T) (≮:-trans-<: p (<:-normalize U)))
+dec-subtyping T U | Right p = Right (<:-trans (<:-normalize T) (<:-trans p (normalize-<: U)))
+