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-29 16:25:11 -05:00
parent 87b55d6e95
commit cecd783b54
4 changed files with 162 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
prototyping/Luau/TypeNormalization.agda
View file

@ -2,29 +2,26 @@ 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
-- Operations on normalized types
_∪ᶠ_ : Type → Type → Type
_∪ⁿˢ_ : 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)
(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
unknown ∪ⁿ T = unknown
(S₁ ∪ S₂) ∪ⁿ G = (S₁ ∪ⁿ G) ∪ S₂
F ∪ⁿ G = F ∪ᶠ G
@ -56,10 +53,14 @@ unknown ∪ⁿˢ T = unknown
(S₁ ∪ S₂) ∪ⁿˢ T = (S₁ ∪ⁿˢ T) ∪ S₂
F ∪ⁿˢ T = F ∪ T
-- Functions on normalized types
never ⇒ⁿ T = never ⇒ unknown
S ⇒ⁿ T = S ⇒ T
-- Normalize!
normalize : Type → Type
normalize nil = never ∪ nil
normalize (S ⇒ T) = (normalize S ⇒ normalize T)
normalize (S ⇒ T) = (normalize S ⇒ⁿ normalize T)
normalize never = never
normalize unknown = unknown
normalize boolean = never ∪ boolean

14
prototyping/Properties/DecSubtyping.agda
View file

@ -26,11 +26,13 @@ dec-subtyping : ∀ T U → Either (T ≮: U) (T <: U)
srcᶠ : ∀ {F} → FunType F → Type
normal-srcᶠ : ∀ {F} → (Fᶠ : FunType F) → Normal (srcᶠ Fᶠ)
srcᶠ-function-err : ∀ {F} → (Fᶠ : FunType F) → ∀ s → ¬Language (srcᶠ Fᶠ) s → Language F (function-err s)
≮:-srcᶠ : ∀ {F S T} → (Fᶠ : FunType F) → (S ≮: srcᶠ Fᶠ) → (F ≮: (S ⇒ T))
resolveᶠⁿ : ∀ {F V} → FunType F → Normal V → Type
normal-resolveᶠⁿ : ∀ {F V} → (Fᶠ : FunType F) → (Vⁿ : Normal V) → Normal (resolveᶠⁿ Fᶠ Vⁿ)
resolveᶠⁿ-funtion-ok : ∀ {F V} → (Fᶠ : FunType F) → (Vⁿ : Normal V) → ∀ s t → Language (srcᶠ Fᶠ) s → ¬Language (resolveᶠⁿ Fᶠ Vⁿ) t → ¬Language F (function-ok s t)
≮:-resolveᶠⁿ : ∀ {F S T} → (Fᶠ : FunType F) → (Sᶠ : Normal S) → (S <: srcᶠ Fᶠ) → (srcᶠ Fᶠ ≮: never) → (resolveᶠⁿ Fᶠ Sᶠ ≮: T) → (F ≮: (S ⇒ T))
<:-resolveᶠⁿ : ∀ {F S T} → (Fᶠ : FunType F) → (Sᶠ : Normal S) → (S <: srcᶠ Fᶠ) → (resolveᶠⁿ Fᶠ Sᶠ <: T) → (F <: (S ⇒ T))
srcᶠ {S ⇒ T} F = S
srcᶠ (F ∩ G) = srcᶠ F ∪ⁿ srcᶠ G
@ -58,14 +60,20 @@ normal-resolveᶠⁿ (F ∩ G) V | Left p | Right q = normal-resolveᶠⁿ G V
normal-resolveᶠⁿ (F ∩ G) V | Right p | Left q = normal-resolveᶠⁿ F V
normal-resolveᶠⁿ (F ∩ G) V | Right p | Right q = normal-∩ⁿ (normal-resolveᶠⁿ F V) (normal-resolveᶠⁿ G V)
resolveᶠⁿ-funtion-ok F V s t p q = {!!}
≮:-resolveᶠⁿ F S p (witness s q₁ q₂) (witness t r₁ r₂) = witness {!function!} {!!} {!!}
<:-resolveᶠⁿ F S p q = {!!}
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 (U ⇒ V) with dec-subtypingⁿ U (normal-srcᶠ T) | dec-subtypingⁿ (normal-resolveᶠⁿ T U) V
dec-subtypingᶠ T (U ⇒ V) | Left p | q = Left (≮:-srcᶠ T p)
dec-subtypingᶠ 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) | Right p | Left q = Left (≮:-resolveᶠⁿ T U p ? q)
dec-subtypingᶠ T (U ⇒ V) | Right p | Right q = Right (<:-resolveᶠⁿ T U p 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)

6
prototyping/Properties/Subtyping.agda
View file

@ -248,6 +248,12 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
<:-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-never : ∀ {T U} → (never ⇒ T) <: (never ⇒ U)
<:-function-never function function = function
<:-function-never (function-ok s t) (function-ok₁ p) = function-ok₁ p
<:-function-never (function-ok s t) (function-ok₂ p) = function-ok₁ never
<:-function-never (function-err s) (function-err p) = 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)

150
prototyping/Properties/TypeNormalization.agda
View file

@ -4,24 +4,34 @@ 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.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)
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; <:-function-never)
-- Notmal forms for types
-- Normal forms for types
data FunType : Type → Set
data Inhabited : Type → Set
data Normal : Type → Set
data FunType where
_⇒_ : ∀ {S T} → Normal S → Normal T → FunType (S ⇒ T)
function : FunType (never ⇒ unknown)
_⇒_ : ∀ {S T} → Inhabited S → Normal T → FunType (S ⇒ T)
_∩_ : ∀ {F G} → FunType F → FunType G → FunType (F ∩ G)
data Inhabited where
function : Inhabited (never ⇒ unknown)
_⇒_ : ∀ {S T} → Inhabited S → Normal T → Inhabited (S ⇒ T)
_∩_ : ∀ {F G} → FunType F → FunType G → Inhabited (F ∩ G)
_∪_ : ∀ {S T} → Normal S → Scalar T → Inhabited (S ∪ T)
unknown : Inhabited unknown
data Normal where
never : Normal never
unknown : Normal unknown
_⇒_ : ∀ {S T} → Normal S → Normal T → Normal (S ⇒ T)
function : Normal (never ⇒ unknown)
_⇒_ : ∀ {S T} → Inhabited S → Normal T → Normal (S ⇒ T)
_∩_ : ∀ {F G} → FunType F → FunType G → Normal (F ∩ G)
_∪_ : ∀ {S T} → Normal S → Scalar T → Normal (S ∪ T)
never : Normal never
unknown : Normal unknown
data OptScalar : Type → Set where
never : OptScalar never
@ -33,14 +43,16 @@ data OptScalar : Type → Set where
-- Normalization produces normal types
normal : ∀ T → Normal (normalize T)
normalᶠ : ∀ {F} → FunType F → Normal F
normalⁱ : ∀ {T} → Inhabited T → Normal T
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-⇒ⁿ : ∀ {S T} → Normal S → Normal T → FunType (S ⇒ⁿ T)
normal nil = never ∪ nil
normal (S ⇒ T) = normalᶠ ((normal S) ⇒ (normal T))
normal (S ⇒ T) = normalᶠ (normal-⇒ⁿ (normal S) (normal T))
normal never = never
normal unknown = unknown
normal boolean = never ∪ boolean
@ -49,9 +61,16 @@ normal string = never ∪ string
normal (S ∪ T) = normal-∪ⁿ (normal S) (normal T)
normal (S ∩ T) = normal-∩ⁿ (normal S) (normal T)
normalᶠ function = function
normalᶠ (S ⇒ T) = S ⇒ T
normalᶠ (F ∩ G) = F ∩ G
normalⁱ function = function
normalⁱ (S ⇒ T) = S ⇒ T
normalⁱ (S ∩ T) = S ∩ T
normalⁱ (S ∪ T) = S ∪ T
normalⁱ unknown = unknown
normal-∪ⁿ S (T₁ ∪ T₂) = (normal-∪ⁿ S T₁) ∪ T₂
normal-∪ⁿ S never = S
normal-∪ⁿ S unknown = unknown
@ -65,6 +84,14 @@ normal-∪ⁿ (F₁ ∩ F₂) (T ⇒ U) = normalᶠ (normal-∪ᶠ (F₁ ∩ F
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-∪ⁿ function function = function
normal-∪ⁿ (R ⇒ S) function = function
normal-∪ⁿ (R ∩ S) function = (normal-∪ᶠ R function) ∩ (normal-∪ᶠ S function)
normal-∪ⁿ (R ∪ S) function = normal-∪ⁿ R function ∪ S
normal-∪ⁿ never function = function
normal-∪ⁿ unknown function = unknown
normal-∪ⁿ function (T ⇒ U) = normalᶠ (normal-⇒ⁿ (normal-∩ⁿ never (normalⁱ T)) (normal-∪ⁿ unknown U))
normal-∪ⁿ function (T ∩ U) = normal-∪ᶠ function T ∩ normal-∪ᶠ function U
normal-∩ⁿ S never = never
normal-∩ⁿ S unknown = S
@ -79,6 +106,14 @@ 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-∩ⁿ function function = function ∩ function
normal-∩ⁿ (R ⇒ S) function = (R ⇒ S) ∩ function
normal-∩ⁿ (R ∩ S) function = (R ∩ S) ∩ function
normal-∩ⁿ (R ∪ S) function = normal-∩ⁿ R function
normal-∩ⁿ never function = never
normal-∩ⁿ unknown function = function
normal-∩ⁿ function (T ⇒ U) = function ∩ (T ⇒ U)
normal-∩ⁿ function (T ∩ U) = function ∩ (T ∩ U)
normal-∪ⁿˢ S never = S
normal-∪ⁿˢ never number = never ∪ number
@ -113,6 +148,10 @@ 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-∪ⁿˢ function number = function ∪ number
normal-∪ⁿˢ function boolean = function ∪ boolean
normal-∪ⁿˢ function string = function ∪ string
normal-∪ⁿˢ function nil = function ∪ nil
normal-∩ⁿˢ never number = never
normal-∩ⁿˢ never boolean = never
@ -146,12 +185,28 @@ 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-∩ⁿˢ function number = never
normal-∩ⁿˢ function boolean = never
normal-∩ⁿˢ function string = never
normal-∩ⁿˢ function nil = never
normal-∪ᶠ (R ⇒ S) (T ⇒ U) = (normal-∩ⁿ R T) ⇒ (normal-∪ⁿ S U)
normal-∪ᶠ (R ⇒ S) (T ⇒ U) = normal-⇒ⁿ (normal-∩ⁿ (normalⁱ R) (normalⁱ 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
normal-∪ᶠ function function = function
normal-∪ᶠ function (T ⇒ U) = normal-⇒ⁿ (normal-∩ⁿ never (normalⁱ T)) (normal-∪ⁿ unknown U)
normal-∪ᶠ function (G ∩ H) = normal-∪ᶠ function G ∩ normal-∪ᶠ function H
normal-∪ᶠ (R ⇒ S) function = function
normal-⇒ⁿ function T = function ⇒ T
normal-⇒ⁿ (R ⇒ S) T = (R ⇒ S) ⇒ T
normal-⇒ⁿ (R ∩ S) T = (R ∩ S) ⇒ T
normal-⇒ⁿ (R ∪ S) T = (R ∪ S) ⇒ T
normal-⇒ⁿ never T = function
normal-⇒ⁿ unknown T = unknown ⇒ T
scalar-∩-fun-<:-never : ∀ {F S} → FunType F → Scalar S → (F ∩ S) <: never
scalar-∩-fun-<:-never function S = scalar-∩-function-<:-never S
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)
@ -167,6 +222,8 @@ flipper = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) <:-∪
∪-<:-∪ⁿ : ∀ {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 T} → Normal S → Normal T → (S ⇒ T) <: (S ⇒ⁿ T)
⇒ⁿ-<:-⇒ : ∀ {S T} → Normal S → Normal T → (S ⇒ⁿ T) <: (S ⇒ T)
∩-<:-∩ⁿ S never = <:-∩-right
∩-<:-∩ⁿ S unknown = <:-∩-left
@ -181,6 +238,14 @@ flipper = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) <:-∪
∩-<:-∩ⁿ (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))
∩-<:-∩ⁿ function function = <:-refl
∩-<:-∩ⁿ function (T ⇒ U) = <:-refl
∩-<:-∩ⁿ function (T ∩ U) = <:-refl
∩-<:-∩ⁿ (R ⇒ S) function = <:-refl
∩-<:-∩ⁿ (R ∩ S) function = <:-refl
∩-<:-∩ⁿ (R ∪ S) function = <:-trans <:-∩-distr-∪ (<:-trans (<:-union (∩-<:-∩ⁿ R function) (<:-trans <:-∩-symm (∩-<:-∩ⁿˢ function S))) (<:-∪-lub <:-refl <:-never))
∩-<:-∩ⁿ never function = <:-∩-left
∩-<:-∩ⁿ unknown function = <:-∩-right
∩ⁿ-<:-∩ S never = <:-never
∩ⁿ-<:-∩ S unknown = <:-∩-glb <:-refl <:-unknown
@ -195,6 +260,14 @@ flipper = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) <:-∪
∩ⁿ-<:-∩ (R ⇒ S) (T ∩ U) = <:-refl
∩ⁿ-<:-∩ (R ∩ S) (T ∩ U) = <:-refl
∩ⁿ-<:-∩ (R ∪ S) (T ∩ U) = <:-trans (∩ⁿ-<:-∩ R (T ∩ U)) (<:-∩-glb (<:-trans <:-∩-left <:-∪-left) <:-∩-right)
∩ⁿ-<:-∩ function function = <:-refl
∩ⁿ-<:-∩ function (S ⇒ T) = <:-refl
∩ⁿ-<:-∩ function (S ∩ T) = <:-refl
∩ⁿ-<:-∩ (R ⇒ S) function = <:-refl
∩ⁿ-<:-∩ (R ∩ S) function = <:-refl
∩ⁿ-<:-∩ (R ∪ S) function = <:-trans (∩ⁿ-<:-∩ R function) (<:-∩-glb (<:-trans <:-∩-left <:-∪-left) <:-∩-right)
∩ⁿ-<:-∩ never function = <:-never
∩ⁿ-<:-∩ unknown function = <:-∩-glb <:-unknown <:-refl
∩-<:-∩ⁿˢ never number = <:-∩-left
∩-<:-∩ⁿˢ never boolean = <:-∩-left
@ -219,6 +292,7 @@ flipper = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) <:-∪
∩-<:-∩ⁿˢ (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
∩-<:-∩ⁿˢ function T = scalar-∩-fun-<:-never function T
∩ⁿˢ-<:-∩ never T = <:-never
∩ⁿˢ-<:-∩ unknown T = <:-∩-glb <:-unknown <:-refl
@ -240,15 +314,24 @@ flipper = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) <:-∪
∩ⁿˢ-<:-∩ (R ∪ boolean) nil = <:-trans (∩ⁿˢ-<:-∩ R nil) (<:-intersect <:-∪-left <:-refl)
∩ⁿˢ-<:-∩ (R ∪ string) nil = <:-trans (∩ⁿˢ-<:-∩ R nil) (<:-intersect <:-∪-left <:-refl)
∩ⁿˢ-<:-∩ (R ∪ nil) nil = <:-∩-glb <:-∪-right <:-refl
∩ⁿˢ-<:-∩ function T = <:-never
∪ᶠ-<:-∪ (R ⇒ S) (T ⇒ U) = <:-trans (<:-function (∩-<:-∩ⁿ R T) (∪ⁿ-<:-∪ S U)) <:-function-∪-∩
∪ᶠ-<:-∪ (R ⇒ S) (T ⇒ U) = <:-trans (⇒ⁿ-<:-⇒ (normal-∩ⁿ (normalⁱ R) (normalⁱ T)) (normal-∪ⁿ S U)) (<:-trans (<:-function (∩-<:-∩ⁿ (normalⁱ R) (normalⁱ 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-∩-<:
∪ᶠ-<:-∪ function function = <:-∪-left
∪ᶠ-<:-∪ function (T ⇒ U) = <:-trans (⇒ⁿ-<:-⇒ (normal-∩ⁿ never (normalⁱ T)) (normal-∪ⁿ unknown U)) (<:-trans (<:-function (∩-<:-∩ⁿ never (normalⁱ T)) (∪ⁿ-<:-∪ unknown U)) <:-function-∪-∩)
∪ᶠ-<:-∪ function (G ∩ H) = <:-trans (<:-intersect (∪ᶠ-<:-∪ function G) (∪ᶠ-<:-∪ function H)) ∪-distl-∩-<:
∪ᶠ-<:-∪ (R ⇒ S) function = <:-∪-right
∪-<:-∪ᶠ : ∀ {F G} → FunType F → FunType G → (F ∪ G) <: (F ∪ᶠ G)
∪-<:-∪ᶠ (R ⇒ S) (T ⇒ U) = <:-trans <:-function-∪ (<:-function (∩ⁿ-<:-∩ R T) (∪-<:-∪ⁿ S U))
∪-<:-∪ᶠ (R ⇒ S) (T ⇒ U) = <:-trans (<:-trans <:-function-∪ (<:-function (∩ⁿ-<:-∩ (normalⁱ R) (normalⁱ T)) (∪-<:-∪ⁿ S U))) (⇒-<:-⇒ⁿ (normal-∩ⁿ (normalⁱ R) (normalⁱ T)) (normal-∪ⁿ 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))
∪-<:-∪ᶠ function function = <:-∪-lub <:-refl <:-refl
∪-<:-∪ᶠ function (T ⇒ U) = <:-trans (<:-trans <:-function-∪ (<:-function (∩ⁿ-<:-∩ never (normalⁱ T)) (∪-<:-∪ⁿ unknown U))) (⇒-<:-⇒ⁿ (normal-∩ⁿ never (normalⁱ T)) (normal-∪ⁿ unknown U))
∪-<:-∪ᶠ function (G ∩ H) = <:-trans <:-∪-distl-∩ (<:-intersect (∪-<:-∪ᶠ function G) (∪-<:-∪ᶠ function H))
∪-<:-∪ᶠ (R ⇒ S) function = <:-∪-lub (<:-function <:-never <:-unknown) <:-refl
∪ⁿˢ-<:-∪ S never = <:-∪-left
∪ⁿˢ-<:-∪ never number = <:-refl
@ -283,6 +366,10 @@ flipper = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) <:-∪
∪ⁿˢ-<:-∪ (R ∪ boolean) nil = <:-trans (<:-union (∪ⁿˢ-<:-∪ R nil) <:-refl) flipper
∪ⁿˢ-<:-∪ (R ∪ string) nil = <:-trans (<:-union (∪ⁿˢ-<:-∪ R nil) <:-refl) flipper
∪ⁿˢ-<:-∪ (R ∪ nil) nil = <:-union <:-∪-left <:-refl
∪ⁿˢ-<:-∪ function number = <:-refl
∪ⁿˢ-<:-∪ function boolean = <:-refl
∪ⁿˢ-<:-∪ function string = <:-refl
∪ⁿˢ-<:-∪ function nil = <:-refl
∪-<:-∪ⁿˢ T never = <:-∪-lub <:-refl <:-never
∪-<:-∪ⁿˢ never number = <:-refl
@ -317,6 +404,10 @@ flipper = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) <:-∪
∪-<:-∪ⁿˢ (R ∪ boolean) nil = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R nil) <:-refl)
∪-<:-∪ⁿˢ (R ∪ string) nil = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R nil) <:-refl)
∪-<:-∪ⁿˢ (R ∪ nil) nil = <:-∪-lub <:-refl <:-∪-right
∪-<:-∪ⁿˢ function number = <:-refl
∪-<:-∪ⁿˢ function boolean = <:-refl
∪-<:-∪ⁿˢ function string = <:-refl
∪-<:-∪ⁿˢ function nil = <:-refl
∪ⁿ-<:-∪ S never = <:-∪-left
∪ⁿ-<:-∪ S unknown = <:-∪-right
@ -331,6 +422,14 @@ flipper = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) <:-∪
∪ⁿ-<:-∪ (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)
∪ⁿ-<:-∪ function function = <:-∪-left
∪ⁿ-<:-∪ function (T ⇒ U) = ∪ᶠ-<:-∪ function (T ⇒ U)
∪ⁿ-<:-∪ function (T ∩ U) = ∪ᶠ-<:-∪ function (T ∩ U)
∪ⁿ-<:-∪ (R ⇒ S) function = ∪ᶠ-<:-∪ (R ⇒ S) function
∪ⁿ-<:-∪ (R ∩ S) function = ∪ᶠ-<:-∪ (R ∩ S) function
∪ⁿ-<:-∪ (R ∪ S) function = <:-trans (<:-union (∪ⁿ-<:-∪ R function) <:-refl) (<:-∪-lub (<:-∪-lub (<:-trans <:-∪-left <:-∪-left) <:-∪-right) (<:-trans <:-∪-right <:-∪-left))
∪ⁿ-<:-∪ never function = <:-∪-right
∪ⁿ-<:-∪ unknown function = <:-∪-left
∪-<:-∪ⁿ S never = <:-∪-lub <:-refl <:-never
∪-<:-∪ⁿ S unknown = <:-unknown
@ -338,7 +437,7 @@ flipper = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) <:-∪
∪-<:-∪ⁿ 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)))
∪-<:-∪ⁿ (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)
@ -349,12 +448,35 @@ flipper = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) <:-∪
∪-<:-∪ⁿ (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)
∪-<:-∪ⁿ function function = ∪-<:-∪ᶠ function function
∪-<:-∪ⁿ function (T ⇒ U) = ∪-<:-∪ᶠ function (T ⇒ U)
∪-<:-∪ⁿ function (T ∩ U) = ∪-<:-∪ᶠ function (T ∩ U)
∪-<:-∪ⁿ function (T ∪ U) = <:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ function T) <:-refl)
∪-<:-∪ⁿ (R ⇒ S) function = ∪-<:-∪ᶠ (R ⇒ S) function
∪-<:-∪ⁿ (R ∩ S) function = ∪-<:-∪ᶠ (R ∩ S) function
∪-<:-∪ⁿ (R ∪ S) function = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) (<:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ R function) <:-refl)))
∪-<:-∪ⁿ never function = <:-∪-lub <:-never <:-refl
∪-<:-∪ⁿ unknown function = <:-unknown
⇒-<:-⇒ⁿ function T = <:-refl
⇒-<:-⇒ⁿ (R ⇒ S) T = <:-refl
⇒-<:-⇒ⁿ (R ∩ S) T = <:-refl
⇒-<:-⇒ⁿ (R ∪ S) T = <:-refl
⇒-<:-⇒ⁿ never T = <:-function-never
⇒-<:-⇒ⁿ unknown T = <:-refl
⇒ⁿ-<:-⇒ function T = <:-refl
⇒ⁿ-<:-⇒ (R ⇒ S) T = <:-refl
⇒ⁿ-<:-⇒ (R ∩ S) T = <:-refl
⇒ⁿ-<:-⇒ (R ∪ S) T = <:-refl
⇒ⁿ-<:-⇒ never T = <:-function-never
⇒ⁿ-<:-⇒ unknown T = <:-refl
normalize-<: : ∀ T → normalize T <: T
<:-normalize : ∀ T → T <: normalize T
<:-normalize nil = <:-∪-right
<:-normalize (S ⇒ T) = <:-function (normalize-<: S) (<:-normalize T)
<:-normalize (S ⇒ T) = <:-trans (<:-function (normalize-<: S) (<:-normalize T)) (⇒-<:-⇒ⁿ (normal S) (normal T))
<:-normalize never = <:-refl
<:-normalize unknown = <:-refl
<:-normalize boolean = <:-∪-right
@ -364,7 +486,7 @@ normalize-<: : ∀ T → normalize T <: 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-<: (S ⇒ T) = <:-trans (⇒ⁿ-<:-⇒ (normal S) (normal T)) (<:-function (<:-normalize S) (normalize-<: T))
normalize-<: never = <:-refl
normalize-<: unknown = <:-refl
normalize-<: boolean = <:-∪-lub <:-never <:-refl