From 74c84815a0ca7f1799a800156833cfc44016f12f Mon Sep 17 00:00:00 2001 From: Alan Jeffrey <403333+asajeffrey@users.noreply.github.com> Date: Thu, 28 Apr 2022 15:00:55 -0500 Subject: [PATCH] Prototyping type normalizaton (#466) * Added type normalization --- prototyping/Luau/FunctionTypes.agda | 38 ++ prototyping/Luau/StrictMode.agda | 3 +- prototyping/Luau/Subtyping.agda | 2 +- prototyping/Luau/Type.agda | 24 +- prototyping/Luau/TypeCheck.agda | 3 +- prototyping/Luau/TypeNormalization.agda | 69 ++++ prototyping/Properties.agda | 3 + prototyping/Properties/DecSubtyping.agda | 70 ++++ prototyping/Properties/FunctionTypes.agda | 150 +++++++ prototyping/Properties/StrictMode.agda | 6 +- prototyping/Properties/Subtyping.agda | 331 ++++++++++----- prototyping/Properties/TypeCheck.agda | 3 +- prototyping/Properties/TypeNormalization.agda | 376 ++++++++++++++++++ 13 files changed, 940 insertions(+), 138 deletions(-) create mode 100644 prototyping/Luau/FunctionTypes.agda create mode 100644 prototyping/Luau/TypeNormalization.agda create mode 100644 prototyping/Properties/DecSubtyping.agda create mode 100644 prototyping/Properties/FunctionTypes.agda create mode 100644 prototyping/Properties/TypeNormalization.agda diff --git a/prototyping/Luau/FunctionTypes.agda b/prototyping/Luau/FunctionTypes.agda new file mode 100644 index 0000000..7607052 --- /dev/null +++ b/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) + diff --git a/prototyping/Luau/StrictMode.agda b/prototyping/Luau/StrictMode.agda index 1b02804..d3c0f15 100644 --- a/prototyping/Luau/StrictMode.agda +++ b/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 _[_]ⱽ) diff --git a/prototyping/Luau/Subtyping.agda b/prototyping/Luau/Subtyping.agda index 943f459..624b6be 100644 --- a/prototyping/Luau/Subtyping.agda +++ b/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) diff --git a/prototyping/Luau/Type.agda b/prototyping/Luau/Type.agda index 59d1107..1d0ec9e 100644 --- a/prototyping/Luau/Type.agda +++ b/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) diff --git a/prototyping/Luau/TypeCheck.agda b/prototyping/Luau/TypeCheck.agda index cabd27a..d4fabb9 100644 --- a/prototyping/Luau/TypeCheck.agda +++ b/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) diff --git a/prototyping/Luau/TypeNormalization.agda b/prototyping/Luau/TypeNormalization.agda new file mode 100644 index 0000000..341883e --- /dev/null +++ b/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 diff --git a/prototyping/Properties.agda b/prototyping/Properties.agda index 5594812..b696c0f 100644 --- a/prototyping/Properties.agda +++ b/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 diff --git a/prototyping/Properties/DecSubtyping.agda b/prototyping/Properties/DecSubtyping.agda new file mode 100644 index 0000000..332520a --- /dev/null +++ b/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))) + diff --git a/prototyping/Properties/FunctionTypes.agda b/prototyping/Properties/FunctionTypes.agda new file mode 100644 index 0000000..514477f --- /dev/null +++ b/prototyping/Properties/FunctionTypes.agda @@ -0,0 +1,150 @@ +{-# OPTIONS --rewriting #-} + +module Properties.FunctionTypes where + +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; _⇒_; _∪_; _∩_; skalar) +open import Properties.Contradiction using (CONTRADICTION; ¬; ⊥) +open import Properties.Functions using (_∘_) +open import Properties.Subtyping using (<:-refl; ≮:-refl; <:-trans-≮:; skalar-scalar; <:-impl-⊇; skalar-function-ok; language-comp) +open import Properties.TypeNormalization using (FunType; Normal; never; unknown; _∩_; _∪_; _⇒_; normal; <:-normalize; normalize-<:) + +-- Properties of src +function-err-srcⁿ : ∀ {T t} → (FunType T) → (¬Language (srcⁿ T) t) → Language T (function-err t) +function-err-srcⁿ (S ⇒ T) p = function-err p +function-err-srcⁿ (S ∩ T) (p₁ , p₂) = (function-err-srcⁿ S p₁ , function-err-srcⁿ T p₂) + +¬function-err-srcᶠ : ∀ {T t} → (FunType T) → (Language (srcⁿ T) t) → ¬Language T (function-err t) +¬function-err-srcᶠ (S ⇒ T) p = function-err p +¬function-err-srcᶠ (S ∩ T) (left p) = left (¬function-err-srcᶠ S p) +¬function-err-srcᶠ (S ∩ T) (right p) = right (¬function-err-srcᶠ T p) + +¬function-err-srcⁿ : ∀ {T t} → (Normal T) → (Language (srcⁿ T) t) → ¬Language T (function-err t) +¬function-err-srcⁿ never p = never +¬function-err-srcⁿ unknown (scalar ()) +¬function-err-srcⁿ (S ⇒ T) p = function-err p +¬function-err-srcⁿ (S ∩ T) (left p) = left (¬function-err-srcᶠ S p) +¬function-err-srcⁿ (S ∩ T) (right p) = right (¬function-err-srcᶠ T p) +¬function-err-srcⁿ (S ∪ T) (scalar ()) + +¬function-err-src : ∀ {T t} → (Language (src T) t) → ¬Language T (function-err t) +¬function-err-src {T = S ⇒ T} p = function-err p +¬function-err-src {T = nil} p = scalar-function-err nil +¬function-err-src {T = never} p = never +¬function-err-src {T = unknown} (scalar ()) +¬function-err-src {T = boolean} p = scalar-function-err boolean +¬function-err-src {T = number} p = scalar-function-err number +¬function-err-src {T = string} p = scalar-function-err string +¬function-err-src {T = S ∪ T} p = <:-impl-⊇ (<:-normalize (S ∪ T)) _ (¬function-err-srcⁿ (normal (S ∪ T)) p) +¬function-err-src {T = S ∩ T} p = <:-impl-⊇ (<:-normalize (S ∩ T)) _ (¬function-err-srcⁿ (normal (S ∩ T)) p) + +src-¬function-errᶠ : ∀ {T t} → (FunType T) → Language T (function-err t) → (¬Language (srcⁿ T) t) +src-¬function-errᶠ (S ⇒ T) (function-err p) = p +src-¬function-errᶠ (S ∩ T) (p₁ , p₂) = (src-¬function-errᶠ S p₁ , src-¬function-errᶠ T p₂) + +src-¬function-errⁿ : ∀ {T t} → (Normal T) → Language T (function-err t) → (¬Language (srcⁿ T) t) +src-¬function-errⁿ unknown p = never +src-¬function-errⁿ (S ⇒ T) (function-err p) = p +src-¬function-errⁿ (S ∩ T) (p₁ , p₂) = (src-¬function-errᶠ S p₁ , src-¬function-errᶠ T p₂) +src-¬function-errⁿ (S ∪ T) p = never + +src-¬function-err : ∀ {T t} → Language T (function-err t) → (¬Language (src T) t) +src-¬function-err {T = S ⇒ T} (function-err p) = p +src-¬function-err {T = unknown} p = never +src-¬function-err {T = S ∪ T} p = src-¬function-errⁿ (normal (S ∪ T)) (<:-normalize (S ∪ T) _ p) +src-¬function-err {T = S ∩ T} p = src-¬function-errⁿ (normal (S ∩ T)) (<:-normalize (S ∩ T) _ p) + +fun-¬scalar : ∀ {S T} (s : Scalar S) → FunType T → ¬Language T (scalar s) +fun-¬scalar s (S ⇒ T) = function-scalar s +fun-¬scalar s (S ∩ T) = left (fun-¬scalar s S) + +¬fun-scalar : ∀ {S T t} (s : Scalar S) → FunType T → Language T t → ¬Language S t +¬fun-scalar s (S ⇒ T) function = scalar-function s +¬fun-scalar s (S ⇒ T) (function-ok p) = scalar-function-ok s +¬fun-scalar s (S ⇒ T) (function-err p) = scalar-function-err s +¬fun-scalar s (S ∩ T) (p₁ , p₂) = ¬fun-scalar s T p₂ + +fun-function : ∀ {T} → FunType T → Language T function +fun-function (S ⇒ T) = function +fun-function (S ∩ T) = (fun-function S , fun-function T) + +srcⁿ-¬scalar : ∀ {S T t} (s : Scalar S) → Normal T → Language T (scalar s) → (¬Language (srcⁿ T) t) +srcⁿ-¬scalar s never (scalar ()) +srcⁿ-¬scalar s unknown p = never +srcⁿ-¬scalar s (S ⇒ T) (scalar ()) +srcⁿ-¬scalar s (S ∩ T) (p₁ , p₂) = CONTRADICTION (language-comp (scalar s) (fun-¬scalar s S) p₁) +srcⁿ-¬scalar s (S ∪ T) p = never + +src-¬scalar : ∀ {S T t} (s : Scalar S) → Language T (scalar s) → (¬Language (src T) t) +src-¬scalar {T = nil} s p = never +src-¬scalar {T = T ⇒ U} s (scalar ()) +src-¬scalar {T = never} s (scalar ()) +src-¬scalar {T = unknown} s p = never +src-¬scalar {T = boolean} s p = never +src-¬scalar {T = number} s p = never +src-¬scalar {T = string} s p = never +src-¬scalar {T = T ∪ U} s p = srcⁿ-¬scalar s (normal (T ∪ U)) (<:-normalize (T ∪ U) (scalar s) p) +src-¬scalar {T = T ∩ U} s p = srcⁿ-¬scalar s (normal (T ∩ U)) (<:-normalize (T ∩ U) (scalar s) p) + +srcⁿ-unknown-≮: : ∀ {T U} → (Normal U) → (T ≮: srcⁿ U) → (U ≮: (T ⇒ unknown)) +srcⁿ-unknown-≮: never (witness t p q) = CONTRADICTION (language-comp t q unknown) +srcⁿ-unknown-≮: unknown (witness t p q) = witness (function-err t) unknown (function-err p) +srcⁿ-unknown-≮: (U ⇒ V) (witness t p q) = witness (function-err t) (function-err q) (function-err p) +srcⁿ-unknown-≮: (U ∩ V) (witness t p q) = witness (function-err t) (function-err-srcⁿ (U ∩ V) q) (function-err p) +srcⁿ-unknown-≮: (U ∪ V) (witness t p q) = witness (scalar V) (right (scalar V)) (function-scalar V) + +src-unknown-≮: : ∀ {T U} → (T ≮: src U) → (U ≮: (T ⇒ unknown)) +src-unknown-≮: {U = nil} (witness t p q) = witness (scalar nil) (scalar nil) (function-scalar nil) +src-unknown-≮: {U = T ⇒ U} (witness t p q) = witness (function-err t) (function-err q) (function-err p) +src-unknown-≮: {U = never} (witness t p q) = CONTRADICTION (language-comp t q unknown) +src-unknown-≮: {U = unknown} (witness t p q) = witness (function-err t) unknown (function-err p) +src-unknown-≮: {U = boolean} (witness t p q) = witness (scalar boolean) (scalar boolean) (function-scalar boolean) +src-unknown-≮: {U = number} (witness t p q) = witness (scalar number) (scalar number) (function-scalar number) +src-unknown-≮: {U = string} (witness t p q) = witness (scalar string) (scalar string) (function-scalar string) +src-unknown-≮: {U = T ∪ U} p = <:-trans-≮: (normalize-<: (T ∪ U)) (srcⁿ-unknown-≮: (normal (T ∪ U)) p) +src-unknown-≮: {U = T ∩ U} p = <:-trans-≮: (normalize-<: (T ∩ U)) (srcⁿ-unknown-≮: (normal (T ∩ U)) p) + +unknown-src-≮: : ∀ {S T U} → (U ≮: S) → (T ≮: (U ⇒ unknown)) → (U ≮: src T) +unknown-src-≮: (witness t x x₁) (witness (scalar s) p (function-scalar s)) = witness t x (src-¬scalar s p) +unknown-src-≮: r (witness (function-ok (scalar s)) p (function-ok (scalar-scalar s () q))) +unknown-src-≮: r (witness (function-ok (function-ok _)) p (function-ok (scalar-function-ok ()))) +unknown-src-≮: r (witness (function-err t) p (function-err q)) = witness t q (src-¬function-err p) + +-- Properties of tgt +tgt-function-ok : ∀ {T t} → (Language (tgt T) t) → Language T (function-ok t) +tgt-function-ok {T = nil} (scalar ()) +tgt-function-ok {T = T₁ ⇒ T₂} p = function-ok p +tgt-function-ok {T = never} (scalar ()) +tgt-function-ok {T = unknown} p = unknown +tgt-function-ok {T = boolean} (scalar ()) +tgt-function-ok {T = number} (scalar ()) +tgt-function-ok {T = string} (scalar ()) +tgt-function-ok {T = T₁ ∪ T₂} (left p) = left (tgt-function-ok p) +tgt-function-ok {T = T₁ ∪ T₂} (right p) = right (tgt-function-ok p) +tgt-function-ok {T = T₁ ∩ T₂} (p₁ , p₂) = (tgt-function-ok p₁ , tgt-function-ok p₂) + +function-ok-tgt : ∀ {T t} → Language T (function-ok t) → (Language (tgt T) t) +function-ok-tgt (function-ok p) = p +function-ok-tgt (left p) = left (function-ok-tgt p) +function-ok-tgt (right p) = right (function-ok-tgt p) +function-ok-tgt (p₁ , p₂) = (function-ok-tgt p₁ , function-ok-tgt p₂) +function-ok-tgt unknown = unknown + +tgt-never-≮: : ∀ {T U} → (tgt T ≮: U) → (T ≮: (skalar ∪ (never ⇒ U))) +tgt-never-≮: (witness t p q) = witness (function-ok t) (tgt-function-ok p) (skalar-function-ok , function-ok q) + +never-tgt-≮: : ∀ {T U} → (T ≮: (skalar ∪ (never ⇒ U))) → (tgt T ≮: U) +never-tgt-≮: (witness (scalar s) p (q₁ , q₂)) = CONTRADICTION (≮:-refl (witness (scalar s) (skalar-scalar s) q₁)) +never-tgt-≮: (witness function p (q₁ , scalar-function ())) +never-tgt-≮: (witness (function-ok t) p (q₁ , function-ok q₂)) = witness t (function-ok-tgt p) q₂ +never-tgt-≮: (witness (function-err (scalar s)) p (q₁ , function-err (scalar ()))) + +src-tgtᶠ-<: : ∀ {T U V} → (FunType T) → (U <: src T) → (tgt T <: V) → (T <: (U ⇒ V)) +src-tgtᶠ-<: T p q (scalar s) r = CONTRADICTION (language-comp (scalar s) (fun-¬scalar s T) r) +src-tgtᶠ-<: T p q function r = function +src-tgtᶠ-<: T p q (function-ok s) r = function-ok (q s (function-ok-tgt r)) +src-tgtᶠ-<: T p q (function-err s) r = function-err (<:-impl-⊇ p s (src-¬function-err r)) + + diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda index fd2cf2f..69e9131 100644 --- a/prototyping/Properties/StrictMode.agda +++ b/prototyping/Properties/StrictMode.agda @@ -11,7 +11,8 @@ open import Luau.StrictMode using (Warningᴱ; Warningᴮ; Warningᴼ; Warning open import Luau.Substitution using (_[_/_]ᴮ; _[_/_]ᴱ; _[_/_]ᴮunless_; var_[_/_]ᴱwhenever_) 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.FunctionTypes using (src; tgt) +open import Luau.Type using (Type; nil; number; boolean; string; _⇒_; never; unknown; _∩_; _∪_; _≡ᵀ_; _≡ᴹᵀ_) 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 (_≡ᴬ_) @@ -22,7 +23,8 @@ 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.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.FunctionTypes using (never-tgt-≮:; tgt-never-≮:; src-unknown-≮:; unknown-src-≮:) +open import Properties.Subtyping using (unknown-≮:; ≡-trans-≮:; ≮:-trans-≡; ≮:-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; +; -; *; /; <; >; <=; >=; ··) diff --git a/prototyping/Properties/Subtyping.agda b/prototyping/Properties/Subtyping.agda index b713eaf..34e6691 100644 --- a/prototyping/Properties/Subtyping.agda +++ b/prototyping/Properties/Subtyping.agda @@ -4,9 +4,10 @@ module Properties.Subtyping where open import Agda.Builtin.Equality using (_≡_; refl) open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond) +open import FFI.Data.Maybe using (Maybe; just; nothing) 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; _⇒_; _∪_; _∩_; src; tgt) -open import Properties.Contradiction using (CONTRADICTION; ¬) +open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; skalar) +open import Properties.Contradiction using (CONTRADICTION; ¬; ⊥) open import Properties.Equality using (_≢_) open import Properties.Functions using (_∘_) open import Properties.Product using (_×_; _,_) @@ -19,28 +20,28 @@ dec-language nil (scalar string) = Left (scalar-scalar string nil (λ ())) dec-language nil (scalar nil) = Right (scalar nil) dec-language nil function = Left (scalar-function nil) dec-language nil (function-ok t) = Left (scalar-function-ok nil) -dec-language nil (function-err t) = Right (scalar-function-err nil) +dec-language nil (function-err t) = Left (scalar-function-err nil) dec-language boolean (scalar number) = Left (scalar-scalar number boolean (λ ())) dec-language boolean (scalar boolean) = Right (scalar boolean) dec-language boolean (scalar string) = Left (scalar-scalar string boolean (λ ())) dec-language boolean (scalar nil) = Left (scalar-scalar nil boolean (λ ())) dec-language boolean function = Left (scalar-function boolean) dec-language boolean (function-ok t) = Left (scalar-function-ok boolean) -dec-language boolean (function-err t) = Right (scalar-function-err boolean) +dec-language boolean (function-err t) = Left (scalar-function-err boolean) dec-language number (scalar number) = Right (scalar number) dec-language number (scalar boolean) = Left (scalar-scalar boolean number (λ ())) dec-language number (scalar string) = Left (scalar-scalar string number (λ ())) dec-language number (scalar nil) = Left (scalar-scalar nil number (λ ())) dec-language number function = Left (scalar-function number) dec-language number (function-ok t) = Left (scalar-function-ok number) -dec-language number (function-err t) = Right (scalar-function-err number) +dec-language number (function-err t) = Left (scalar-function-err number) dec-language string (scalar number) = Left (scalar-scalar number string (λ ())) dec-language string (scalar boolean) = Left (scalar-scalar boolean string (λ ())) dec-language string (scalar string) = Right (scalar string) dec-language string (scalar nil) = Left (scalar-scalar nil string (λ ())) dec-language string function = Left (scalar-function string) dec-language string (function-ok t) = Left (scalar-function-ok string) -dec-language string (function-err t) = Right (scalar-function-err string) +dec-language string (function-err t) = Left (scalar-function-err string) dec-language (T₁ ⇒ T₂) (scalar s) = Left (function-scalar s) dec-language (T₁ ⇒ T₂) function = Right function dec-language (T₁ ⇒ T₂) (function-ok t) = mapLR function-ok function-ok (dec-language T₂ t) @@ -73,6 +74,11 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp <:-impl-¬≮: : ∀ {T U} → (T <: U) → ¬(T ≮: U) <:-impl-¬≮: p (witness t q r) = language-comp t r (p t q) +<:-impl-⊇ : ∀ {T U} → (T <: U) → ∀ t → ¬Language U t → ¬Language T t +<:-impl-⊇ {T} p t q with dec-language T t +<:-impl-⊇ {_} p t q | Left r = r +<:-impl-⊇ {_} p t q | Right r = CONTRADICTION (language-comp t q (p t r)) + -- reflexivity ≮:-refl : ∀ {T} → ¬(T ≮: T) ≮:-refl (witness t p q) = language-comp t q p @@ -91,10 +97,162 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp ≮:-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 + +≮:-trans-<: : ∀ {S T U} → (S ≮: U) → (T <: U) → (S ≮: T) +≮:-trans-<: (witness t p q) r = witness t p (<:-impl-⊇ r t q) + +-- Properties of union + +<:-union : ∀ {R S T U} → (R <: T) → (S <: U) → ((R ∪ S) <: (T ∪ U)) +<:-union p q t (left r) = left (p t r) +<:-union p q t (right r) = right (q t r) + +<:-∪-left : ∀ {S T} → S <: (S ∪ T) +<:-∪-left t p = left p + +<:-∪-right : ∀ {S T} → T <: (S ∪ T) +<:-∪-right t p = right p + +<:-∪-lub : ∀ {S T U} → (S <: U) → (T <: U) → ((S ∪ T) <: U) +<:-∪-lub p q t (left r) = p t r +<:-∪-lub p q t (right r) = q t r + +<:-∪-symm : ∀ {T U} → (T ∪ U) <: (U ∪ T) +<:-∪-symm t (left p) = right p +<:-∪-symm t (right p) = left p + +<:-∪-assocl : ∀ {S T U} → (S ∪ (T ∪ U)) <: ((S ∪ T) ∪ U) +<:-∪-assocl t (left p) = left (left p) +<:-∪-assocl t (right (left p)) = left (right p) +<:-∪-assocl t (right (right p)) = right p + +<:-∪-assocr : ∀ {S T U} → ((S ∪ T) ∪ U) <: (S ∪ (T ∪ U)) +<:-∪-assocr t (left (left p)) = left p +<:-∪-assocr t (left (right p)) = right (left p) +<:-∪-assocr t (right p) = right (right p) + +≮:-∪-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)) +<:-intersect p q t (r₁ , r₂) = (p t r₁ , q t r₂) + +<:-∩-left : ∀ {S T} → (S ∩ T) <: S +<:-∩-left t (p , _) = p + +<:-∩-right : ∀ {S T} → (S ∩ T) <: T +<:-∩-right t (_ , p) = p + +<:-∩-glb : ∀ {S T U} → (S <: T) → (S <: U) → (S <: (T ∩ U)) +<:-∩-glb p q t r = (p t r , q t r) + +<:-∩-symm : ∀ {T U} → (T ∩ U) <: (U ∩ T) +<:-∩-symm t (p₁ , p₂) = (p₂ , p₁) + +≮:-∩-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 +<:-∩-distl-∪ : ∀ {S T U} → (S ∩ (T ∪ U)) <: ((S ∩ T) ∪ (S ∩ U)) +<:-∩-distl-∪ t (p₁ , left p₂) = left (p₁ , p₂) +<:-∩-distl-∪ t (p₁ , right p₂) = right (p₁ , p₂) + +∩-distl-∪-<: : ∀ {S T U} → ((S ∩ T) ∪ (S ∩ U)) <: (S ∩ (T ∪ U)) +∩-distl-∪-<: t (left (p₁ , p₂)) = (p₁ , left p₂) +∩-distl-∪-<: t (right (p₁ , p₂)) = (p₁ , right p₂) + +<:-∩-distr-∪ : ∀ {S T U} → ((S ∪ T) ∩ U) <: ((S ∩ U) ∪ (T ∩ U)) +<:-∩-distr-∪ t (left p₁ , p₂) = left (p₁ , p₂) +<:-∩-distr-∪ t (right p₁ , p₂) = right (p₁ , p₂) + +∩-distr-∪-<: : ∀ {S T U} → ((S ∩ U) ∪ (T ∩ U)) <: ((S ∪ T) ∩ U) +∩-distr-∪-<: t (left (p₁ , p₂)) = (left p₁ , p₂) +∩-distr-∪-<: t (right (p₁ , p₂)) = (right p₁ , p₂) + +<:-∪-distl-∩ : ∀ {S T U} → (S ∪ (T ∩ U)) <: ((S ∪ T) ∩ (S ∪ U)) +<:-∪-distl-∩ t (left p) = (left p , left p) +<:-∪-distl-∩ t (right (p₁ , p₂)) = (right p₁ , right p₂) + +∪-distl-∩-<: : ∀ {S T U} → ((S ∪ T) ∩ (S ∪ U)) <: (S ∪ (T ∩ U)) +∪-distl-∩-<: t (left p₁ , p₂) = left p₁ +∪-distl-∩-<: t (right p₁ , left p₂) = left p₂ +∪-distl-∩-<: t (right p₁ , right p₂) = right (p₁ , p₂) + +<:-∪-distr-∩ : ∀ {S T U} → ((S ∩ T) ∪ U) <: ((S ∪ U) ∩ (T ∪ U)) +<:-∪-distr-∩ t (left (p₁ , p₂)) = left p₁ , left p₂ +<:-∪-distr-∩ t (right p) = (right p , right p) + +∪-distr-∩-<: : ∀ {S T U} → ((S ∪ U) ∩ (T ∪ U)) <: ((S ∩ T) ∪ U) +∪-distr-∩-<: t (left p₁ , left p₂) = left (p₁ , p₂) +∪-distr-∩-<: t (left p₁ , right p₂) = right p₂ +∪-distr-∩-<: t (right p₁ , p₂) = right p₁ + +-- Properties of functions +<:-function : ∀ {R S T U} → (R <: S) → (T <: U) → (S ⇒ T) <: (R ⇒ U) +<:-function p q function function = function +<:-function p q (function-ok t) (function-ok r) = function-ok (q t r) +<:-function p q (function-err s) (function-err r) = function-err (<:-impl-⊇ p s r) + +<:-function-∩-∪ : ∀ {R S T U} → ((R ⇒ T) ∩ (S ⇒ U)) <: ((R ∪ S) ⇒ (T ∪ U)) +<:-function-∩-∪ function (function , function) = function +<:-function-∩-∪ (function-ok t) (function-ok p₁ , function-ok p₂) = function-ok (right p₂) +<:-function-∩-∪ (function-err _) (function-err p₁ , function-err q₂) = function-err (p₁ , q₂) + +<:-function-∩ : ∀ {S T U} → ((S ⇒ T) ∩ (S ⇒ U)) <: (S ⇒ (T ∩ U)) +<:-function-∩ function (function , function) = function +<:-function-∩ (function-ok 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 (left function) = function +<:-function-∪ (function-ok t) (left (function-ok p)) = function-ok (left p) +<:-function-∪ (function-err s) (left (function-err p)) = function-err (left p) +<:-function-∪ (scalar s) (left (scalar ())) +<:-function-∪ function (right function) = function +<:-function-∪ (function-ok t) (right (function-ok p)) = function-ok (right p) +<:-function-∪ (function-err s) (right (function-err x)) = function-err (right x) +<:-function-∪ (scalar s) (right (scalar ())) + +<:-function-∪-∩ : ∀ {R S T U} → ((R ∩ S) ⇒ (T ∪ U)) <: ((R ⇒ T) ∪ (S ⇒ U)) +<:-function-∪-∩ function function = left function +<:-function-∪-∩ (function-ok t) (function-ok (left p)) = left (function-ok p) +<:-function-∪-∩ (function-ok 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) + +≮:-function-left : ∀ {R S T U} → (R ≮: S) → (S ⇒ T) ≮: (R ⇒ U) +≮:-function-left (witness t p q) = witness (function-err t) (function-err q) (function-err p) + +≮:-function-right : ∀ {R S T U} → (T ≮: U) → (S ⇒ T) ≮: (R ⇒ U) +≮:-function-right (witness t p q) = witness (function-ok t) (function-ok p) (function-ok q) -- Properties of scalars -skalar = number ∪ (string ∪ (nil ∪ boolean)) +skalar-function-ok : ∀ {t} → (¬Language skalar (function-ok t)) +skalar-function-ok = (scalar-function-ok number , (scalar-function-ok string , (scalar-function-ok nil , scalar-function-ok boolean))) + +scalar-<: : ∀ {S T} → (s : Scalar S) → Language T (scalar s) → (S <: T) +scalar-<: number p (scalar number) (scalar number) = p +scalar-<: boolean p (scalar boolean) (scalar boolean) = p +scalar-<: string p (scalar string) (scalar string) = p +scalar-<: nil p (scalar nil) (scalar nil) = p + +scalar-∩-function-<:-never : ∀ {S T U} → (Scalar S) → ((T ⇒ U) ∩ S) <: never +scalar-∩-function-<:-never number .(scalar number) (() , scalar number) +scalar-∩-function-<:-never boolean .(scalar boolean) (() , scalar boolean) +scalar-∩-function-<:-never string .(scalar string) (() , scalar string) +scalar-∩-function-<:-never nil .(scalar nil) (() , scalar nil) function-≮:-scalar : ∀ {S T U} → (Scalar U) → ((S ⇒ T) ≮: U) function-≮:-scalar s = witness function function (scalar-function s) @@ -111,28 +269,8 @@ scalar-≮:-never s = witness (scalar s) (scalar s) never scalar-≢-impl-≮: : ∀ {T U} → (Scalar T) → (Scalar U) → (T ≢ U) → (T ≮: U) scalar-≢-impl-≮: s₁ s₂ p = witness (scalar s₁) (scalar s₁) (scalar-scalar s₁ s₂ p) --- Properties of tgt -tgt-function-ok : ∀ {T t} → (Language (tgt T) t) → Language T (function-ok t) -tgt-function-ok {T = nil} (scalar ()) -tgt-function-ok {T = T₁ ⇒ T₂} p = function-ok p -tgt-function-ok {T = never} (scalar ()) -tgt-function-ok {T = unknown} p = unknown -tgt-function-ok {T = boolean} (scalar ()) -tgt-function-ok {T = number} (scalar ()) -tgt-function-ok {T = string} (scalar ()) -tgt-function-ok {T = T₁ ∪ T₂} (left p) = left (tgt-function-ok p) -tgt-function-ok {T = T₁ ∪ T₂} (right p) = right (tgt-function-ok p) -tgt-function-ok {T = T₁ ∩ T₂} (p₁ , p₂) = (tgt-function-ok p₁ , tgt-function-ok p₂) - -function-ok-tgt : ∀ {T t} → Language T (function-ok t) → (Language (tgt T) t) -function-ok-tgt (function-ok p) = p -function-ok-tgt (left p) = left (function-ok-tgt p) -function-ok-tgt (right p) = right (function-ok-tgt p) -function-ok-tgt (p₁ , p₂) = (function-ok-tgt p₁ , function-ok-tgt p₂) -function-ok-tgt unknown = unknown - -skalar-function-ok : ∀ {t} → (¬Language skalar (function-ok t)) -skalar-function-ok = (scalar-function-ok number , (scalar-function-ok string , (scalar-function-ok nil , scalar-function-ok boolean))) +scalar-≢-∩-<:-never : ∀ {T U V} → (Scalar T) → (Scalar U) → (T ≢ U) → (T ∩ U) <: V +scalar-≢-∩-<:-never s t p u (scalar s₁ , scalar s₂) = CONTRADICTION (p refl) skalar-scalar : ∀ {T} (s : Scalar T) → (Language skalar (scalar s)) skalar-scalar number = left (scalar number) @@ -140,72 +278,6 @@ skalar-scalar boolean = right (right (right (scalar boolean))) skalar-scalar string = right (left (scalar string)) skalar-scalar nil = right (right (left (scalar nil))) -tgt-never-≮: : ∀ {T U} → (tgt T ≮: U) → (T ≮: (skalar ∪ (never ⇒ U))) -tgt-never-≮: (witness t p q) = witness (function-ok t) (tgt-function-ok p) (skalar-function-ok , function-ok q) - -never-tgt-≮: : ∀ {T U} → (T ≮: (skalar ∪ (never ⇒ U))) → (tgt T ≮: U) -never-tgt-≮: (witness (scalar s) p (q₁ , q₂)) = CONTRADICTION (≮:-refl (witness (scalar s) (skalar-scalar s) q₁)) -never-tgt-≮: (witness function p (q₁ , scalar-function ())) -never-tgt-≮: (witness (function-ok t) p (q₁ , function-ok q₂)) = witness t (function-ok-tgt p) q₂ -never-tgt-≮: (witness (function-err (scalar s)) p (q₁ , function-err (scalar ()))) - --- Properties of src -function-err-src : ∀ {T t} → (¬Language (src T) t) → Language T (function-err t) -function-err-src {T = nil} never = scalar-function-err nil -function-err-src {T = T₁ ⇒ T₂} p = function-err p -function-err-src {T = never} (scalar-scalar number () p) -function-err-src {T = never} (scalar-function-ok ()) -function-err-src {T = unknown} never = unknown -function-err-src {T = boolean} p = scalar-function-err boolean -function-err-src {T = number} p = scalar-function-err number -function-err-src {T = string} p = scalar-function-err string -function-err-src {T = T₁ ∪ T₂} (left p) = left (function-err-src p) -function-err-src {T = T₁ ∪ T₂} (right p) = right (function-err-src p) -function-err-src {T = T₁ ∩ T₂} (p₁ , p₂) = function-err-src p₁ , function-err-src p₂ - -¬function-err-src : ∀ {T t} → (Language (src T) t) → ¬Language T (function-err t) -¬function-err-src {T = nil} (scalar ()) -¬function-err-src {T = T₁ ⇒ T₂} p = function-err p -¬function-err-src {T = never} unknown = never -¬function-err-src {T = unknown} (scalar ()) -¬function-err-src {T = boolean} (scalar ()) -¬function-err-src {T = number} (scalar ()) -¬function-err-src {T = string} (scalar ()) -¬function-err-src {T = T₁ ∪ T₂} (p₁ , p₂) = (¬function-err-src p₁ , ¬function-err-src p₂) -¬function-err-src {T = T₁ ∩ T₂} (left p) = left (¬function-err-src p) -¬function-err-src {T = T₁ ∩ T₂} (right p) = right (¬function-err-src p) - -src-¬function-err : ∀ {T t} → Language T (function-err t) → (¬Language (src T) t) -src-¬function-err {T = nil} p = never -src-¬function-err {T = T₁ ⇒ T₂} (function-err p) = p -src-¬function-err {T = never} (scalar-function-err ()) -src-¬function-err {T = unknown} p = never -src-¬function-err {T = boolean} p = never -src-¬function-err {T = number} p = never -src-¬function-err {T = string} p = never -src-¬function-err {T = T₁ ∪ T₂} (left p) = left (src-¬function-err p) -src-¬function-err {T = T₁ ∪ T₂} (right p) = right (src-¬function-err p) -src-¬function-err {T = T₁ ∩ T₂} (p₁ , p₂) = (src-¬function-err p₁ , src-¬function-err p₂) - -src-¬scalar : ∀ {S T t} (s : Scalar S) → Language T (scalar s) → (¬Language (src T) t) -src-¬scalar number (scalar number) = never -src-¬scalar boolean (scalar boolean) = never -src-¬scalar string (scalar string) = never -src-¬scalar nil (scalar nil) = never -src-¬scalar s (left p) = left (src-¬scalar s p) -src-¬scalar s (right p) = right (src-¬scalar s p) -src-¬scalar s (p₁ , p₂) = (src-¬scalar s p₁ , src-¬scalar s p₂) -src-¬scalar s unknown = never - -src-unknown-≮: : ∀ {T U} → (T ≮: src U) → (U ≮: (T ⇒ unknown)) -src-unknown-≮: (witness t p q) = witness (function-err t) (function-err-src q) (¬function-err-src p) - -unknown-src-≮: : ∀ {S T U} → (U ≮: S) → (T ≮: (U ⇒ unknown)) → (U ≮: src T) -unknown-src-≮: (witness t x x₁) (witness (scalar s) p (function-scalar s)) = witness t x (src-¬scalar s p) -unknown-src-≮: r (witness (function-ok (scalar s)) p (function-ok (scalar-scalar s () q))) -unknown-src-≮: r (witness (function-ok (function-ok _)) p (function-ok (scalar-function-ok ()))) -unknown-src-≮: r (witness (function-err t) p (function-err q)) = witness t q (src-¬function-err p) - -- Properties of unknown and never unknown-≮: : ∀ {T U} → (T ≮: U) → (unknown ≮: U) unknown-≮: (witness t p q) = witness t unknown q @@ -219,6 +291,28 @@ unknown-≮:-never = witness (scalar nil) unknown never function-≮:-never : ∀ {T U} → ((T ⇒ U) ≮: never) function-≮:-never = witness function function never +<:-never : ∀ {T} → (never <: T) +<:-never t (scalar ()) + +≮:-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) + +<:-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 t) p = left (function-ok unknown) +<:-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) -- Unfortunately we don't quite have this property, due to uninhabited types, @@ -234,13 +328,21 @@ _⊗_ : ∀ {A B : Set} → (A → Set) → (B → Set) → ((A × B) → Set) Comp : ∀ {A : Set} → (A → Set) → (A → Set) Comp P a = ¬(P a) +Lift : ∀ {A : Set} → (A → Set) → (Maybe A → Set) +Lift P nothing = ⊥ +Lift P (just a) = P a + set-theoretic-if : ∀ {S₁ T₁ S₂ T₂} → -- This is the "if" part of being a set-theoretic model + -- though it uses the definition from Frisch's thesis + -- rather than from the Gentle Introduction. The difference + -- being the presence of Lift, (written D_Ω in Defn 4.2 of + -- https://www.cduce.org/papers/frisch_phd.pdf). (Language (S₁ ⇒ T₁) ⊆ Language (S₂ ⇒ T₂)) → - (∀ Q → Q ⊆ Comp((Language S₁) ⊗ Comp(Language T₁)) → Q ⊆ Comp((Language S₂) ⊗ Comp(Language T₂))) + (∀ Q → Q ⊆ Comp((Language S₁) ⊗ Comp(Lift(Language T₁))) → Q ⊆ Comp((Language S₂) ⊗ Comp(Lift(Language T₂)))) -set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , u) Qtu (S₂t , ¬T₂u) = q (t , u) Qtu (S₁t , ¬T₁u) where +set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , just u) Qtu (S₂t , ¬T₂u) = q (t , just u) Qtu (S₁t , ¬T₁u) where S₁t : Language S₁ t S₁t with dec-language S₁ t @@ -252,6 +354,14 @@ set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , u) Qtu (S₂t , ¬T₂u) ¬T₁u T₁u with p (function-ok u) (function-ok T₁u) ¬T₁u T₁u | function-ok T₂u = ¬T₂u T₂u +set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , nothing) Qt- (S₂t , _) = q (t , nothing) Qt- (S₁t , λ ()) where + + S₁t : Language S₁ t + S₁t with dec-language S₁ t + S₁t | Left ¬S₁t with p (function-err t) (function-err ¬S₁t) + S₁t | Left ¬S₁t | function-err ¬S₂t = CONTRADICTION (language-comp t ¬S₂t S₂t) + S₁t | Right r = r + not-quite-set-theoretic-only-if : ∀ {S₁ T₁ S₂ T₂} → -- We don't quite have that this is a set-theoretic model @@ -260,32 +370,33 @@ not-quite-set-theoretic-only-if : ∀ {S₁ T₁ S₂ T₂} → ∀ s₂ t₂ → Language S₂ s₂ → ¬Language T₂ t₂ → -- This is the "only if" part of being a set-theoretic model - (∀ Q → Q ⊆ Comp((Language S₁) ⊗ Comp(Language T₁)) → Q ⊆ Comp((Language S₂) ⊗ Comp(Language T₂))) → + (∀ Q → Q ⊆ Comp((Language S₁) ⊗ Comp(Lift(Language T₁))) → Q ⊆ Comp((Language S₂) ⊗ Comp(Lift(Language T₂)))) → (Language (S₁ ⇒ T₁) ⊆ Language (S₂ ⇒ T₂)) not-quite-set-theoretic-only-if {S₁} {T₁} {S₂} {T₂} s₂ t₂ S₂s₂ ¬T₂t₂ p = r where - Q : (Tree × Tree) → Set - Q (t , u) = Either (¬Language S₁ t) (Language T₁ u) + Q : (Tree × Maybe Tree) → Set + Q (t , just u) = Either (¬Language S₁ t) (Language T₁ u) + Q (t , nothing) = ¬Language S₁ t - q : Q ⊆ Comp((Language S₁) ⊗ Comp(Language T₁)) - q (t , u) (Left ¬S₁t) (S₁t , ¬T₁u) = language-comp t ¬S₁t S₁t - q (t , u) (Right T₂u) (S₁t , ¬T₁u) = ¬T₁u T₂u + q : Q ⊆ Comp((Language S₁) ⊗ Comp(Lift(Language T₁))) + q (t , just u) (Left ¬S₁t) (S₁t , ¬T₁u) = language-comp t ¬S₁t S₁t + q (t , just u) (Right T₂u) (S₁t , ¬T₁u) = ¬T₁u T₂u + q (t , nothing) ¬S₁t (S₁t , _) = language-comp t ¬S₁t S₁t r : Language (S₁ ⇒ T₁) ⊆ Language (S₂ ⇒ T₂) r function function = function - r (function-err t) (function-err ¬S₁t) with dec-language S₂ t - r (function-err t) (function-err ¬S₁t) | Left ¬S₂t = function-err ¬S₂t - r (function-err t) (function-err ¬S₁t) | Right S₂t = CONTRADICTION (p Q q (t , t₂) (Left ¬S₁t) (S₂t , language-comp t₂ ¬T₂t₂)) + r (function-err s) (function-err ¬S₁s) with dec-language S₂ s + r (function-err s) (function-err ¬S₁s) | Left ¬S₂s = function-err ¬S₂s + r (function-err s) (function-err ¬S₁s) | Right S₂s = CONTRADICTION (p Q q (s , nothing) ¬S₁s (S₂s , λ ())) r (function-ok t) (function-ok T₁t) with dec-language T₂ t - r (function-ok t) (function-ok T₁t) | Left ¬T₂t = CONTRADICTION (p Q q (s₂ , t) (Right T₁t) (S₂s₂ , language-comp t ¬T₂t)) + r (function-ok t) (function-ok T₁t) | Left ¬T₂t = CONTRADICTION (p Q q (s₂ , just t) (Right T₁t) (S₂s₂ , language-comp t ¬T₂t)) r (function-ok t) (function-ok T₁t) | Right T₂t = function-ok T₂t -- A counterexample when the argument type is empty. -set-theoretic-counterexample-one : (∀ Q → Q ⊆ Comp((Language never) ⊗ Comp(Language number)) → Q ⊆ Comp((Language never) ⊗ Comp(Language string))) +set-theoretic-counterexample-one : (∀ Q → Q ⊆ Comp((Language never) ⊗ Comp(Lift(Language number))) → Q ⊆ Comp((Language never) ⊗ Comp(Lift(Language string)))) set-theoretic-counterexample-one Q q ((scalar s) , u) Qtu (scalar () , p) -set-theoretic-counterexample-one Q q ((function-err t) , u) Qtu (scalar-function-err () , p) set-theoretic-counterexample-two : (never ⇒ number) ≮: (never ⇒ string) set-theoretic-counterexample-two = witness diff --git a/prototyping/Properties/TypeCheck.agda b/prototyping/Properties/TypeCheck.agda index 0726a4b..37fbeda 100644 --- a/prototyping/Properties/TypeCheck.agda +++ b/prototyping/Properties/TypeCheck.agda @@ -8,7 +8,8 @@ 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.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.FunctionTypes using (src; tgt) +open import Luau.Type using (Type; nil; unknown; never; number; boolean; string; _⇒_) open import Luau.RuntimeType using (RuntimeType; nil; number; function; string; valueType) open import Luau.VarCtxt using (VarCtxt; ∅; _↦_; _⊕_↦_; _⋒_; _⊝_) renaming (_[_] to _[_]ⱽ) open import Luau.Addr using (Addr) diff --git a/prototyping/Properties/TypeNormalization.agda b/prototyping/Properties/TypeNormalization.agda new file mode 100644 index 0000000..299f648 --- /dev/null +++ b/prototyping/Properties/TypeNormalization.agda @@ -0,0 +1,376 @@ +{-# OPTIONS --rewriting #-} + +module Properties.TypeNormalization where + +open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_) +open import Luau.Subtyping using (scalar-function-err) +open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_; _∪ᶠ_; _∪ⁿˢ_; _∩ⁿˢ_; normalize) +open import Luau.Subtyping using (_<:_) +open import Properties.Subtyping using (<:-trans; <:-refl; <:-unknown; <:-never; <:-∪-left; <:-∪-right; <:-∪-lub; <:-∩-left; <:-∩-right; <:-∩-glb; <:-∩-symm; <:-function; <:-function-∪-∩; <:-function-∩-∪; <:-function-∪; <:-everything; <:-union; <:-∪-assocl; <:-∪-assocr; <:-∪-symm; <:-intersect; ∪-distl-∩-<:; ∪-distr-∩-<:; <:-∪-distr-∩; <:-∪-distl-∩; ∩-distl-∪-<:; <:-∩-distl-∪; <:-∩-distr-∪; scalar-∩-function-<:-never; scalar-≢-∩-<:-never) + +-- Notmal forms for types +data FunType : Type → Set +data Normal : Type → Set + +data FunType where + _⇒_ : ∀ {S T} → Normal S → Normal T → FunType (S ⇒ T) + _∩_ : ∀ {F G} → FunType F → FunType G → FunType (F ∩ G) + +data Normal where + never : Normal never + unknown : Normal unknown + _⇒_ : ∀ {S T} → Normal S → Normal T → Normal (S ⇒ T) + _∩_ : ∀ {F G} → FunType F → FunType G → Normal (F ∩ G) + _∪_ : ∀ {S T} → Normal S → Scalar T → Normal (S ∪ T) + +data OptScalar : Type → Set where + never : OptScalar never + number : OptScalar number + boolean : OptScalar boolean + string : OptScalar string + nil : OptScalar nil + +-- Normalization produces normal types +normal : ∀ T → Normal (normalize T) +normalᶠ : ∀ {F} → FunType F → Normal F +normal-∪ⁿ : ∀ {S T} → Normal S → Normal T → Normal (S ∪ⁿ T) +normal-∩ⁿ : ∀ {S T} → Normal S → Normal T → Normal (S ∩ⁿ T) +normal-∪ⁿˢ : ∀ {S T} → Normal S → OptScalar T → Normal (S ∪ⁿˢ T) +normal-∩ⁿˢ : ∀ {S T} → Normal S → Scalar T → OptScalar (S ∩ⁿˢ T) +normal-∪ᶠ : ∀ {F G} → FunType F → FunType G → FunType (F ∪ᶠ G) + +normal nil = never ∪ nil +normal (S ⇒ T) = normalᶠ ((normal S) ⇒ (normal T)) +normal never = never +normal unknown = unknown +normal boolean = never ∪ boolean +normal number = never ∪ number +normal string = never ∪ string +normal (S ∪ T) = normal-∪ⁿ (normal S) (normal T) +normal (S ∩ T) = normal-∩ⁿ (normal S) (normal T) + +normalᶠ (S ⇒ T) = S ⇒ T +normalᶠ (F ∩ G) = F ∩ G + +normal-∪ⁿ S (T₁ ∪ T₂) = (normal-∪ⁿ S T₁) ∪ T₂ +normal-∪ⁿ S never = S +normal-∪ⁿ S unknown = unknown +normal-∪ⁿ never (T ⇒ U) = T ⇒ U +normal-∪ⁿ never (G₁ ∩ G₂) = G₁ ∩ G₂ +normal-∪ⁿ unknown (T ⇒ U) = unknown +normal-∪ⁿ unknown (G₁ ∩ G₂) = unknown +normal-∪ⁿ (R ⇒ S) (T ⇒ U) = normalᶠ (normal-∪ᶠ (R ⇒ S) (T ⇒ U)) +normal-∪ⁿ (R ⇒ S) (G₁ ∩ G₂) = normalᶠ (normal-∪ᶠ (R ⇒ S) (G₁ ∩ G₂)) +normal-∪ⁿ (F₁ ∩ F₂) (T ⇒ U) = normalᶠ (normal-∪ᶠ (F₁ ∩ F₂) (T ⇒ U)) +normal-∪ⁿ (F₁ ∩ F₂) (G₁ ∩ G₂) = normalᶠ (normal-∪ᶠ (F₁ ∩ F₂) (G₁ ∩ G₂)) +normal-∪ⁿ (S₁ ∪ S₂) (T₁ ⇒ T₂) = normal-∪ⁿ S₁ (T₁ ⇒ T₂) ∪ S₂ +normal-∪ⁿ (S₁ ∪ S₂) (G₁ ∩ G₂) = normal-∪ⁿ S₁ (G₁ ∩ G₂) ∪ S₂ + +normal-∩ⁿ S never = never +normal-∩ⁿ S unknown = S +normal-∩ⁿ S (T ∪ U) = normal-∪ⁿˢ (normal-∩ⁿ S T) (normal-∩ⁿˢ S U ) +normal-∩ⁿ never (T ⇒ U) = never +normal-∩ⁿ unknown (T ⇒ U) = T ⇒ U +normal-∩ⁿ (R ⇒ S) (T ⇒ U) = (R ⇒ S) ∩ (T ⇒ U) +normal-∩ⁿ (R ∩ S) (T ⇒ U) = (R ∩ S) ∩ (T ⇒ U) +normal-∩ⁿ (R ∪ S) (T ⇒ U) = normal-∩ⁿ R (T ⇒ U) +normal-∩ⁿ never (T ∩ U) = never +normal-∩ⁿ unknown (T ∩ U) = T ∩ U +normal-∩ⁿ (R ⇒ S) (T ∩ U) = (R ⇒ S) ∩ (T ∩ U) +normal-∩ⁿ (R ∩ S) (T ∩ U) = (R ∩ S) ∩ (T ∩ U) +normal-∩ⁿ (R ∪ S) (T ∩ U) = normal-∩ⁿ R (T ∩ U) + +normal-∪ⁿˢ S never = S +normal-∪ⁿˢ never number = never ∪ number +normal-∪ⁿˢ unknown number = unknown +normal-∪ⁿˢ (R ⇒ S) number = (R ⇒ S) ∪ number +normal-∪ⁿˢ (R ∩ S) number = (R ∩ S) ∪ number +normal-∪ⁿˢ (R ∪ number) number = R ∪ number +normal-∪ⁿˢ (R ∪ boolean) number = normal-∪ⁿˢ R number ∪ boolean +normal-∪ⁿˢ (R ∪ string) number = normal-∪ⁿˢ R number ∪ string +normal-∪ⁿˢ (R ∪ nil) number = normal-∪ⁿˢ R number ∪ nil +normal-∪ⁿˢ never boolean = never ∪ boolean +normal-∪ⁿˢ unknown boolean = unknown +normal-∪ⁿˢ (R ⇒ S) boolean = (R ⇒ S) ∪ boolean +normal-∪ⁿˢ (R ∩ S) boolean = (R ∩ S) ∪ boolean +normal-∪ⁿˢ (R ∪ number) boolean = normal-∪ⁿˢ R boolean ∪ number +normal-∪ⁿˢ (R ∪ boolean) boolean = R ∪ boolean +normal-∪ⁿˢ (R ∪ string) boolean = normal-∪ⁿˢ R boolean ∪ string +normal-∪ⁿˢ (R ∪ nil) boolean = normal-∪ⁿˢ R boolean ∪ nil +normal-∪ⁿˢ never string = never ∪ string +normal-∪ⁿˢ unknown string = unknown +normal-∪ⁿˢ (R ⇒ S) string = (R ⇒ S) ∪ string +normal-∪ⁿˢ (R ∩ S) string = (R ∩ S) ∪ string +normal-∪ⁿˢ (R ∪ number) string = normal-∪ⁿˢ R string ∪ number +normal-∪ⁿˢ (R ∪ boolean) string = normal-∪ⁿˢ R string ∪ boolean +normal-∪ⁿˢ (R ∪ string) string = R ∪ string +normal-∪ⁿˢ (R ∪ nil) string = normal-∪ⁿˢ R string ∪ nil +normal-∪ⁿˢ never nil = never ∪ nil +normal-∪ⁿˢ unknown nil = unknown +normal-∪ⁿˢ (R ⇒ S) nil = (R ⇒ S) ∪ nil +normal-∪ⁿˢ (R ∩ S) nil = (R ∩ S) ∪ nil +normal-∪ⁿˢ (R ∪ number) nil = normal-∪ⁿˢ R nil ∪ number +normal-∪ⁿˢ (R ∪ boolean) nil = normal-∪ⁿˢ R nil ∪ boolean +normal-∪ⁿˢ (R ∪ string) nil = normal-∪ⁿˢ R nil ∪ string +normal-∪ⁿˢ (R ∪ nil) nil = R ∪ nil + +normal-∩ⁿˢ never number = never +normal-∩ⁿˢ never boolean = never +normal-∩ⁿˢ never string = never +normal-∩ⁿˢ never nil = never +normal-∩ⁿˢ unknown number = number +normal-∩ⁿˢ unknown boolean = boolean +normal-∩ⁿˢ unknown string = string +normal-∩ⁿˢ unknown nil = nil +normal-∩ⁿˢ (R ⇒ S) number = never +normal-∩ⁿˢ (R ⇒ S) boolean = never +normal-∩ⁿˢ (R ⇒ S) string = never +normal-∩ⁿˢ (R ⇒ S) nil = never +normal-∩ⁿˢ (R ∩ S) number = never +normal-∩ⁿˢ (R ∩ S) boolean = never +normal-∩ⁿˢ (R ∩ S) string = never +normal-∩ⁿˢ (R ∩ S) nil = never +normal-∩ⁿˢ (R ∪ number) number = number +normal-∩ⁿˢ (R ∪ boolean) number = normal-∩ⁿˢ R number +normal-∩ⁿˢ (R ∪ string) number = normal-∩ⁿˢ R number +normal-∩ⁿˢ (R ∪ nil) number = normal-∩ⁿˢ R number +normal-∩ⁿˢ (R ∪ number) boolean = normal-∩ⁿˢ R boolean +normal-∩ⁿˢ (R ∪ boolean) boolean = boolean +normal-∩ⁿˢ (R ∪ string) boolean = normal-∩ⁿˢ R boolean +normal-∩ⁿˢ (R ∪ nil) boolean = normal-∩ⁿˢ R boolean +normal-∩ⁿˢ (R ∪ number) string = normal-∩ⁿˢ R string +normal-∩ⁿˢ (R ∪ boolean) string = normal-∩ⁿˢ R string +normal-∩ⁿˢ (R ∪ string) string = string +normal-∩ⁿˢ (R ∪ nil) string = normal-∩ⁿˢ R string +normal-∩ⁿˢ (R ∪ number) nil = normal-∩ⁿˢ R nil +normal-∩ⁿˢ (R ∪ boolean) nil = normal-∩ⁿˢ R nil +normal-∩ⁿˢ (R ∪ string) nil = normal-∩ⁿˢ R nil +normal-∩ⁿˢ (R ∪ nil) nil = nil + +normal-∪ᶠ (R ⇒ S) (T ⇒ U) = (normal-∩ⁿ R T) ⇒ (normal-∪ⁿ S U) +normal-∪ᶠ (R ⇒ S) (G ∩ H) = normal-∪ᶠ (R ⇒ S) G ∩ normal-∪ᶠ (R ⇒ S) H +normal-∪ᶠ (E ∩ F) G = normal-∪ᶠ E G ∩ normal-∪ᶠ F G + +scalar-∩-fun-<:-never : ∀ {F S} → FunType F → Scalar S → (F ∩ S) <: never +scalar-∩-fun-<:-never (T ⇒ U) S = scalar-∩-function-<:-never S +scalar-∩-fun-<:-never (F ∩ G) S = <:-trans (<:-intersect <:-∩-left <:-refl) (scalar-∩-fun-<:-never F S) + +flipper : ∀ {S T U} → ((S ∪ T) ∪ U) <: ((S ∪ U) ∪ T) +flipper = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) <:-∪-assocl) + +∩-<:-∩ⁿ : ∀ {S T} → Normal S → Normal T → (S ∩ T) <: (S ∩ⁿ T) +∩ⁿ-<:-∩ : ∀ {S T} → Normal S → Normal T → (S ∩ⁿ T) <: (S ∩ T) +∩-<:-∩ⁿˢ : ∀ {S T} → Normal S → Scalar T → (S ∩ T) <: (S ∩ⁿˢ T) +∩ⁿˢ-<:-∩ : ∀ {S T} → Normal S → Scalar T → (S ∩ⁿˢ T) <: (S ∩ T) +∪ᶠ-<:-∪ : ∀ {F G} → FunType F → FunType G → (F ∪ᶠ G) <: (F ∪ G) +∪ⁿ-<:-∪ : ∀ {S T} → Normal S → Normal T → (S ∪ⁿ T) <: (S ∪ T) +∪-<:-∪ⁿ : ∀ {S T} → Normal S → Normal T → (S ∪ T) <: (S ∪ⁿ T) +∪ⁿˢ-<:-∪ : ∀ {S T} → Normal S → OptScalar T → (S ∪ⁿˢ T) <: (S ∪ T) +∪-<:-∪ⁿˢ : ∀ {S T} → Normal S → OptScalar T → (S ∪ T) <: (S ∪ⁿˢ T) + +∩-<:-∩ⁿ S never = <:-∩-right +∩-<:-∩ⁿ S unknown = <:-∩-left +∩-<:-∩ⁿ S (T ∪ U) = <:-trans <:-∩-distl-∪ (<:-trans (<:-union (∩-<:-∩ⁿ S T) (∩-<:-∩ⁿˢ S U)) (∪-<:-∪ⁿˢ (normal-∩ⁿ S T) (normal-∩ⁿˢ S U)) ) +∩-<:-∩ⁿ never (T ⇒ U) = <:-∩-left +∩-<:-∩ⁿ unknown (T ⇒ U) = <:-∩-right +∩-<:-∩ⁿ (R ⇒ S) (T ⇒ U) = <:-refl +∩-<:-∩ⁿ (R ∩ S) (T ⇒ U) = <:-refl +∩-<:-∩ⁿ (R ∪ S) (T ⇒ U) = <:-trans <:-∩-distr-∪ (<:-trans (<:-union (∩-<:-∩ⁿ R (T ⇒ U)) (<:-trans <:-∩-symm (∩-<:-∩ⁿˢ (T ⇒ U) S))) (<:-∪-lub <:-refl <:-never)) +∩-<:-∩ⁿ never (T ∩ U) = <:-∩-left +∩-<:-∩ⁿ unknown (T ∩ U) = <:-∩-right +∩-<:-∩ⁿ (R ⇒ S) (T ∩ U) = <:-refl +∩-<:-∩ⁿ (R ∩ S) (T ∩ U) = <:-refl +∩-<:-∩ⁿ (R ∪ S) (T ∩ U) = <:-trans <:-∩-distr-∪ (<:-trans (<:-union (∩-<:-∩ⁿ R (T ∩ U)) (<:-trans <:-∩-symm (∩-<:-∩ⁿˢ (T ∩ U) S))) (<:-∪-lub <:-refl <:-never)) + +∩ⁿ-<:-∩ S never = <:-never +∩ⁿ-<:-∩ S unknown = <:-∩-glb <:-refl <:-unknown +∩ⁿ-<:-∩ S (T ∪ U) = <:-trans (∪ⁿˢ-<:-∪ (normal-∩ⁿ S T) (normal-∩ⁿˢ S U)) (<:-trans (<:-union (∩ⁿ-<:-∩ S T) (∩ⁿˢ-<:-∩ S U)) ∩-distl-∪-<:) +∩ⁿ-<:-∩ never (T ⇒ U) = <:-never +∩ⁿ-<:-∩ unknown (T ⇒ U) = <:-∩-glb <:-unknown <:-refl +∩ⁿ-<:-∩ (R ⇒ S) (T ⇒ U) = <:-refl +∩ⁿ-<:-∩ (R ∩ S) (T ⇒ U) = <:-refl +∩ⁿ-<:-∩ (R ∪ S) (T ⇒ U) = <:-trans (∩ⁿ-<:-∩ R (T ⇒ U)) (<:-∩-glb (<:-trans <:-∩-left <:-∪-left) <:-∩-right) +∩ⁿ-<:-∩ never (T ∩ U) = <:-never +∩ⁿ-<:-∩ unknown (T ∩ U) = <:-∩-glb <:-unknown <:-refl +∩ⁿ-<:-∩ (R ⇒ S) (T ∩ U) = <:-refl +∩ⁿ-<:-∩ (R ∩ S) (T ∩ U) = <:-refl +∩ⁿ-<:-∩ (R ∪ S) (T ∩ U) = <:-trans (∩ⁿ-<:-∩ R (T ∩ U)) (<:-∩-glb (<:-trans <:-∩-left <:-∪-left) <:-∩-right) + +∩-<:-∩ⁿˢ never number = <:-∩-left +∩-<:-∩ⁿˢ never boolean = <:-∩-left +∩-<:-∩ⁿˢ never string = <:-∩-left +∩-<:-∩ⁿˢ never nil = <:-∩-left +∩-<:-∩ⁿˢ unknown T = <:-∩-right +∩-<:-∩ⁿˢ (R ⇒ S) T = scalar-∩-fun-<:-never (R ⇒ S) T +∩-<:-∩ⁿˢ (F ∩ G) T = scalar-∩-fun-<:-never (F ∩ G) T +∩-<:-∩ⁿˢ (R ∪ number) number = <:-∩-right +∩-<:-∩ⁿˢ (R ∪ boolean) number = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R number) (scalar-≢-∩-<:-never boolean number (λ ()))) +∩-<:-∩ⁿˢ (R ∪ string) number = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R number) (scalar-≢-∩-<:-never string number (λ ()))) +∩-<:-∩ⁿˢ (R ∪ nil) number = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R number) (scalar-≢-∩-<:-never nil number (λ ()))) +∩-<:-∩ⁿˢ (R ∪ number) boolean = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R boolean) (scalar-≢-∩-<:-never number boolean (λ ()))) +∩-<:-∩ⁿˢ (R ∪ boolean) boolean = <:-∩-right +∩-<:-∩ⁿˢ (R ∪ string) boolean = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R boolean) (scalar-≢-∩-<:-never string boolean (λ ()))) +∩-<:-∩ⁿˢ (R ∪ nil) boolean = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R boolean) (scalar-≢-∩-<:-never nil boolean (λ ()))) +∩-<:-∩ⁿˢ (R ∪ number) string = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R string) (scalar-≢-∩-<:-never number string (λ ()))) +∩-<:-∩ⁿˢ (R ∪ boolean) string = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R string) (scalar-≢-∩-<:-never boolean string (λ ()))) +∩-<:-∩ⁿˢ (R ∪ string) string = <:-∩-right +∩-<:-∩ⁿˢ (R ∪ nil) string = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R string) (scalar-≢-∩-<:-never nil string (λ ()))) +∩-<:-∩ⁿˢ (R ∪ number) nil = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R nil) (scalar-≢-∩-<:-never number nil (λ ()))) +∩-<:-∩ⁿˢ (R ∪ boolean) nil = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R nil) (scalar-≢-∩-<:-never boolean nil (λ ()))) +∩-<:-∩ⁿˢ (R ∪ string) nil = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R nil) (scalar-≢-∩-<:-never string nil (λ ()))) +∩-<:-∩ⁿˢ (R ∪ nil) nil = <:-∩-right + +∩ⁿˢ-<:-∩ never T = <:-never +∩ⁿˢ-<:-∩ unknown T = <:-∩-glb <:-unknown <:-refl +∩ⁿˢ-<:-∩ (R ⇒ S) T = <:-never +∩ⁿˢ-<:-∩ (F ∩ G) T = <:-never +∩ⁿˢ-<:-∩ (R ∪ number) number = <:-∩-glb <:-∪-right <:-refl +∩ⁿˢ-<:-∩ (R ∪ boolean) number = <:-trans (∩ⁿˢ-<:-∩ R number) (<:-intersect <:-∪-left <:-refl) +∩ⁿˢ-<:-∩ (R ∪ string) number = <:-trans (∩ⁿˢ-<:-∩ R number) (<:-intersect <:-∪-left <:-refl) +∩ⁿˢ-<:-∩ (R ∪ nil) number = <:-trans (∩ⁿˢ-<:-∩ R number) (<:-intersect <:-∪-left <:-refl) +∩ⁿˢ-<:-∩ (R ∪ number) boolean = <:-trans (∩ⁿˢ-<:-∩ R boolean) (<:-intersect <:-∪-left <:-refl) +∩ⁿˢ-<:-∩ (R ∪ boolean) boolean = <:-∩-glb <:-∪-right <:-refl +∩ⁿˢ-<:-∩ (R ∪ string) boolean = <:-trans (∩ⁿˢ-<:-∩ R boolean) (<:-intersect <:-∪-left <:-refl) +∩ⁿˢ-<:-∩ (R ∪ nil) boolean = <:-trans (∩ⁿˢ-<:-∩ R boolean) (<:-intersect <:-∪-left <:-refl) +∩ⁿˢ-<:-∩ (R ∪ number) string = <:-trans (∩ⁿˢ-<:-∩ R string) (<:-intersect <:-∪-left <:-refl) +∩ⁿˢ-<:-∩ (R ∪ boolean) string = <:-trans (∩ⁿˢ-<:-∩ R string) (<:-intersect <:-∪-left <:-refl) +∩ⁿˢ-<:-∩ (R ∪ string) string = <:-∩-glb <:-∪-right <:-refl +∩ⁿˢ-<:-∩ (R ∪ nil) string = <:-trans (∩ⁿˢ-<:-∩ R string) (<:-intersect <:-∪-left <:-refl) +∩ⁿˢ-<:-∩ (R ∪ number) nil = <:-trans (∩ⁿˢ-<:-∩ R nil) (<:-intersect <:-∪-left <:-refl) +∩ⁿˢ-<:-∩ (R ∪ boolean) nil = <:-trans (∩ⁿˢ-<:-∩ R nil) (<:-intersect <:-∪-left <:-refl) +∩ⁿˢ-<:-∩ (R ∪ string) nil = <:-trans (∩ⁿˢ-<:-∩ R nil) (<:-intersect <:-∪-left <:-refl) +∩ⁿˢ-<:-∩ (R ∪ nil) nil = <:-∩-glb <:-∪-right <:-refl + +∪ᶠ-<:-∪ (R ⇒ S) (T ⇒ U) = <:-trans (<:-function (∩-<:-∩ⁿ R T) (∪ⁿ-<:-∪ S U)) <:-function-∪-∩ +∪ᶠ-<:-∪ (R ⇒ S) (G ∩ H) = <:-trans (<:-intersect (∪ᶠ-<:-∪ (R ⇒ S) G) (∪ᶠ-<:-∪ (R ⇒ S) H)) ∪-distl-∩-<: +∪ᶠ-<:-∪ (E ∩ F) G = <:-trans (<:-intersect (∪ᶠ-<:-∪ E G) (∪ᶠ-<:-∪ F G)) ∪-distr-∩-<: + +∪-<:-∪ᶠ : ∀ {F G} → FunType F → FunType G → (F ∪ G) <: (F ∪ᶠ G) +∪-<:-∪ᶠ (R ⇒ S) (T ⇒ U) = <:-trans <:-function-∪ (<:-function (∩ⁿ-<:-∩ R T) (∪-<:-∪ⁿ S U)) +∪-<:-∪ᶠ (R ⇒ S) (G ∩ H) = <:-trans <:-∪-distl-∩ (<:-intersect (∪-<:-∪ᶠ (R ⇒ S) G) (∪-<:-∪ᶠ (R ⇒ S) H)) +∪-<:-∪ᶠ (E ∩ F) G = <:-trans <:-∪-distr-∩ (<:-intersect (∪-<:-∪ᶠ E G) (∪-<:-∪ᶠ F G)) + +∪ⁿˢ-<:-∪ S never = <:-∪-left +∪ⁿˢ-<:-∪ never number = <:-refl +∪ⁿˢ-<:-∪ never boolean = <:-refl +∪ⁿˢ-<:-∪ never string = <:-refl +∪ⁿˢ-<:-∪ never nil = <:-refl +∪ⁿˢ-<:-∪ unknown number = <:-∪-left +∪ⁿˢ-<:-∪ unknown boolean = <:-∪-left +∪ⁿˢ-<:-∪ unknown string = <:-∪-left +∪ⁿˢ-<:-∪ unknown nil = <:-∪-left +∪ⁿˢ-<:-∪ (R ⇒ S) number = <:-refl +∪ⁿˢ-<:-∪ (R ⇒ S) boolean = <:-refl +∪ⁿˢ-<:-∪ (R ⇒ S) string = <:-refl +∪ⁿˢ-<:-∪ (R ⇒ S) nil = <:-refl +∪ⁿˢ-<:-∪ (R ∩ S) number = <:-refl +∪ⁿˢ-<:-∪ (R ∩ S) boolean = <:-refl +∪ⁿˢ-<:-∪ (R ∩ S) string = <:-refl +∪ⁿˢ-<:-∪ (R ∩ S) nil = <:-refl +∪ⁿˢ-<:-∪ (R ∪ number) number = <:-union <:-∪-left <:-refl +∪ⁿˢ-<:-∪ (R ∪ boolean) number = <:-trans (<:-union (∪ⁿˢ-<:-∪ R number) <:-refl) flipper +∪ⁿˢ-<:-∪ (R ∪ string) number = <:-trans (<:-union (∪ⁿˢ-<:-∪ R number) <:-refl) flipper +∪ⁿˢ-<:-∪ (R ∪ nil) number = <:-trans (<:-union (∪ⁿˢ-<:-∪ R number) <:-refl) flipper +∪ⁿˢ-<:-∪ (R ∪ number) boolean = <:-trans (<:-union (∪ⁿˢ-<:-∪ R boolean) <:-refl) flipper +∪ⁿˢ-<:-∪ (R ∪ boolean) boolean = <:-union <:-∪-left <:-refl +∪ⁿˢ-<:-∪ (R ∪ string) boolean = <:-trans (<:-union (∪ⁿˢ-<:-∪ R boolean) <:-refl) flipper +∪ⁿˢ-<:-∪ (R ∪ nil) boolean = <:-trans (<:-union (∪ⁿˢ-<:-∪ R boolean) <:-refl) flipper +∪ⁿˢ-<:-∪ (R ∪ number) string = <:-trans (<:-union (∪ⁿˢ-<:-∪ R string) <:-refl) flipper +∪ⁿˢ-<:-∪ (R ∪ boolean) string = <:-trans (<:-union (∪ⁿˢ-<:-∪ R string) <:-refl) flipper +∪ⁿˢ-<:-∪ (R ∪ string) string = <:-union <:-∪-left <:-refl +∪ⁿˢ-<:-∪ (R ∪ nil) string = <:-trans (<:-union (∪ⁿˢ-<:-∪ R string) <:-refl) flipper +∪ⁿˢ-<:-∪ (R ∪ number) nil = <:-trans (<:-union (∪ⁿˢ-<:-∪ R nil) <:-refl) flipper +∪ⁿˢ-<:-∪ (R ∪ boolean) nil = <:-trans (<:-union (∪ⁿˢ-<:-∪ R nil) <:-refl) flipper +∪ⁿˢ-<:-∪ (R ∪ string) nil = <:-trans (<:-union (∪ⁿˢ-<:-∪ R nil) <:-refl) flipper +∪ⁿˢ-<:-∪ (R ∪ nil) nil = <:-union <:-∪-left <:-refl + +∪-<:-∪ⁿˢ T never = <:-∪-lub <:-refl <:-never +∪-<:-∪ⁿˢ never number = <:-refl +∪-<:-∪ⁿˢ never boolean = <:-refl +∪-<:-∪ⁿˢ never string = <:-refl +∪-<:-∪ⁿˢ never nil = <:-refl +∪-<:-∪ⁿˢ unknown number = <:-unknown +∪-<:-∪ⁿˢ unknown boolean = <:-unknown +∪-<:-∪ⁿˢ unknown string = <:-unknown +∪-<:-∪ⁿˢ unknown nil = <:-unknown +∪-<:-∪ⁿˢ (R ⇒ S) number = <:-refl +∪-<:-∪ⁿˢ (R ⇒ S) boolean = <:-refl +∪-<:-∪ⁿˢ (R ⇒ S) string = <:-refl +∪-<:-∪ⁿˢ (R ⇒ S) nil = <:-refl +∪-<:-∪ⁿˢ (R ∩ S) number = <:-refl +∪-<:-∪ⁿˢ (R ∩ S) boolean = <:-refl +∪-<:-∪ⁿˢ (R ∩ S) string = <:-refl +∪-<:-∪ⁿˢ (R ∩ S) nil = <:-refl +∪-<:-∪ⁿˢ (R ∪ number) number = <:-∪-lub <:-refl <:-∪-right +∪-<:-∪ⁿˢ (R ∪ boolean) number = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R number) <:-refl) +∪-<:-∪ⁿˢ (R ∪ string) number = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R number) <:-refl) +∪-<:-∪ⁿˢ (R ∪ nil) number = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R number) <:-refl) +∪-<:-∪ⁿˢ (R ∪ number) boolean = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R boolean) <:-refl) +∪-<:-∪ⁿˢ (R ∪ boolean) boolean = <:-∪-lub <:-refl <:-∪-right +∪-<:-∪ⁿˢ (R ∪ string) boolean = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R boolean) <:-refl) +∪-<:-∪ⁿˢ (R ∪ nil) boolean = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R boolean) <:-refl) +∪-<:-∪ⁿˢ (R ∪ number) string = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R string) <:-refl) +∪-<:-∪ⁿˢ (R ∪ boolean) string = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R string) <:-refl) +∪-<:-∪ⁿˢ (R ∪ string) string = <:-∪-lub <:-refl <:-∪-right +∪-<:-∪ⁿˢ (R ∪ nil) string = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R string) <:-refl) +∪-<:-∪ⁿˢ (R ∪ number) nil = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R nil) <:-refl) +∪-<:-∪ⁿˢ (R ∪ boolean) nil = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R nil) <:-refl) +∪-<:-∪ⁿˢ (R ∪ string) nil = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R nil) <:-refl) +∪-<:-∪ⁿˢ (R ∪ nil) nil = <:-∪-lub <:-refl <:-∪-right + +∪ⁿ-<:-∪ S never = <:-∪-left +∪ⁿ-<:-∪ S unknown = <:-∪-right +∪ⁿ-<:-∪ never (T ⇒ U) = <:-∪-right +∪ⁿ-<:-∪ unknown (T ⇒ U) = <:-∪-left +∪ⁿ-<:-∪ (R ⇒ S) (T ⇒ U) = ∪ᶠ-<:-∪ (R ⇒ S) (T ⇒ U) +∪ⁿ-<:-∪ (R ∩ S) (T ⇒ U) = ∪ᶠ-<:-∪ (R ∩ S) (T ⇒ U) +∪ⁿ-<:-∪ (R ∪ S) (T ⇒ U) = <:-trans (<:-union (∪ⁿ-<:-∪ R (T ⇒ U)) <:-refl) (<:-∪-lub (<:-∪-lub (<:-trans <:-∪-left <:-∪-left) <:-∪-right) (<:-trans <:-∪-right <:-∪-left)) +∪ⁿ-<:-∪ never (T ∩ U) = <:-∪-right +∪ⁿ-<:-∪ unknown (T ∩ U) = <:-∪-left +∪ⁿ-<:-∪ (R ⇒ S) (T ∩ U) = ∪ᶠ-<:-∪ (R ⇒ S) (T ∩ U) +∪ⁿ-<:-∪ (R ∩ S) (T ∩ U) = ∪ᶠ-<:-∪ (R ∩ S) (T ∩ U) +∪ⁿ-<:-∪ (R ∪ S) (T ∩ U) = <:-trans (<:-union (∪ⁿ-<:-∪ R (T ∩ U)) <:-refl) (<:-∪-lub (<:-∪-lub (<:-trans <:-∪-left <:-∪-left) <:-∪-right) (<:-trans <:-∪-right <:-∪-left)) +∪ⁿ-<:-∪ S (T ∪ U) = <:-∪-lub (<:-trans (∪ⁿ-<:-∪ S T) (<:-union <:-refl <:-∪-left)) (<:-trans <:-∪-right <:-∪-right) + +∪-<:-∪ⁿ S never = <:-∪-lub <:-refl <:-never +∪-<:-∪ⁿ S unknown = <:-unknown +∪-<:-∪ⁿ never (T ⇒ U) = <:-∪-lub <:-never <:-refl +∪-<:-∪ⁿ unknown (T ⇒ U) = <:-unknown +∪-<:-∪ⁿ (R ⇒ S) (T ⇒ U) = ∪-<:-∪ᶠ (R ⇒ S) (T ⇒ U) +∪-<:-∪ⁿ (R ∩ S) (T ⇒ U) = ∪-<:-∪ᶠ (R ∩ S) (T ⇒ U) +∪-<:-∪ⁿ (R ∪ S) (T ⇒ U) = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) (<:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ R (T ⇒ U)) <:-refl))) +∪-<:-∪ⁿ never (T ∩ U) = <:-∪-lub <:-never <:-refl +∪-<:-∪ⁿ unknown (T ∩ U) = <:-unknown +∪-<:-∪ⁿ (R ⇒ S) (T ∩ U) = ∪-<:-∪ᶠ (R ⇒ S) (T ∩ U) +∪-<:-∪ⁿ (R ∩ S) (T ∩ U) = ∪-<:-∪ᶠ (R ∩ S) (T ∩ U) +∪-<:-∪ⁿ (R ∪ S) (T ∩ U) = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) (<:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ R (T ∩ U)) <:-refl))) +∪-<:-∪ⁿ never (T ∪ U) = <:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ never T) <:-refl) +∪-<:-∪ⁿ unknown (T ∪ U) = <:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ unknown T) <:-refl) +∪-<:-∪ⁿ (R ⇒ S) (T ∪ U) = <:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ (R ⇒ S) T) <:-refl) +∪-<:-∪ⁿ (R ∩ S) (T ∪ U) = <:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ (R ∩ S) T) <:-refl) +∪-<:-∪ⁿ (R ∪ S) (T ∪ U) = <:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ (R ∪ S) T) <:-refl) + +normalize-<: : ∀ T → normalize T <: T +<:-normalize : ∀ T → T <: normalize T + +<:-normalize nil = <:-∪-right +<:-normalize (S ⇒ T) = <:-function (normalize-<: S) (<:-normalize T) +<:-normalize never = <:-refl +<:-normalize unknown = <:-refl +<:-normalize boolean = <:-∪-right +<:-normalize number = <:-∪-right +<:-normalize string = <:-∪-right +<:-normalize (S ∪ T) = <:-trans (<:-union (<:-normalize S) (<:-normalize T)) (∪-<:-∪ⁿ (normal S) (normal T)) +<:-normalize (S ∩ T) = <:-trans (<:-intersect (<:-normalize S) (<:-normalize T)) (∩-<:-∩ⁿ (normal S) (normal T)) + +normalize-<: nil = <:-∪-lub <:-never <:-refl +normalize-<: (S ⇒ T) = <:-function (<:-normalize S) (normalize-<: T) +normalize-<: never = <:-refl +normalize-<: unknown = <:-refl +normalize-<: boolean = <:-∪-lub <:-never <:-refl +normalize-<: number = <:-∪-lub <:-never <:-refl +normalize-<: string = <:-∪-lub <:-never <:-refl +normalize-<: (S ∪ T) = <:-trans (∪ⁿ-<:-∪ (normal S) (normal T)) (<:-union (normalize-<: S) (normalize-<: T)) +normalize-<: (S ∩ T) = <:-trans (∩ⁿ-<:-∩ (normal S) (normal T)) (<:-intersect (normalize-<: S) (normalize-<: T)) + +