From 81d90b032fb6ca53972fd2729746b01252579508 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Tue, 26 Apr 2022 18:51:10 -0500 Subject: [PATCH] Added decidability of subtyping --- prototyping/Properties.agda | 1 + prototyping/Properties/DecSubtyping.agda | 70 +++++++++++++++++++++++ prototyping/Properties/FunctionTypes.agda | 18 ++++++ prototyping/Properties/Subtyping.agda | 15 +++++ 4 files changed, 104 insertions(+) create mode 100644 prototyping/Properties/DecSubtyping.agda diff --git a/prototyping/Properties.agda b/prototyping/Properties.agda index 6305ea53..b696c0fa 100644 --- a/prototyping/Properties.agda +++ b/prototyping/Properties.agda @@ -4,6 +4,7 @@ module Properties where import Properties.Contradiction import Properties.Dec +import Properties.DecSubtyping import Properties.Equality import Properties.Functions import Properties.FunctionTypes diff --git a/prototyping/Properties/DecSubtyping.agda b/prototyping/Properties/DecSubtyping.agda new file mode 100644 index 00000000..332520a9 --- /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 index a02f380f..514477f1 100644 --- a/prototyping/Properties/FunctionTypes.agda +++ b/prototyping/Properties/FunctionTypes.agda @@ -60,6 +60,16 @@ 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 @@ -130,3 +140,11 @@ never-tgt-≮: (witness (scalar s) p (q₁ , q₂)) = CONTRADICTION (≮:-refl ( 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/Subtyping.agda b/prototyping/Properties/Subtyping.agda index f9972ee8..34e6691f 100644 --- a/prototyping/Properties/Subtyping.agda +++ b/prototyping/Properties/Subtyping.agda @@ -102,6 +102,9 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp <:-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)) @@ -229,10 +232,22 @@ 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-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-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)