diff --git a/prototyping/Properties/DecSubtyping.agda b/prototyping/Properties/DecSubtyping.agda new file mode 100644 index 00000000..2d990bae --- /dev/null +++ b/prototyping/Properties/DecSubtyping.agda @@ -0,0 +1,197 @@ +{-# 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.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 Properties.Functions using (_∘_) + +-- ¬Language T is the complement of Language T +language-comp : ∀ {T} t → ¬Language T t → ¬(Language T t) +language-comp t (p₁ , p₂) (left q) = language-comp t p₁ q +language-comp t (p₁ , p₂) (right q) = language-comp t p₂ q +language-comp t (left p) (q₁ , q₂) = language-comp t p q₁ +language-comp t (right p) (q₁ , q₂) = language-comp t p q₂ +language-comp (scalar s) (scalar-scalar s p₁ p₂) (scalar s) = p₂ refl +language-comp (scalar s) (function-scalar s) (scalar s) = language-comp function (scalar-function s) function +language-comp (scalar s) never (scalar ()) +language-comp function (scalar-function ()) function +language-comp (function-ok t) (scalar-function-ok ()) (function-ok q) +language-comp (function-ok t) (function-ok p) (function-ok q) = language-comp t p q +language-comp (function-err t) (function-err p) (function-err q) = language-comp t q p + +-- 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-≮: : ∀ {T U} → (src T ≮: src U) → (U ≮: T) +src-≮: (witness t p q) = witness (function-err t) (function-err-src q) (¬function-err-src 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-¬function-ok : ∀ {T t} → (¬Language (tgt T) t) → ¬Language T (function-ok t) +tgt-¬function-ok {T = nil} p = scalar-function-ok nil +tgt-¬function-ok {T = T₁ ⇒ T₂} p = function-ok p +tgt-¬function-ok {T = never} p = never +tgt-¬function-ok {T = unknown} (scalar-scalar s () p) +tgt-¬function-ok {T = unknown} (scalar-function ()) +tgt-¬function-ok {T = unknown} (scalar-function-ok ()) +tgt-¬function-ok {T = boolean} p = scalar-function-ok boolean +tgt-¬function-ok {T = number} p = scalar-function-ok number +tgt-¬function-ok {T = string} p = scalar-function-ok string +tgt-¬function-ok {T = T₁ ∪ T₂} (p₁ , p₂) = (tgt-¬function-ok p₁ , tgt-¬function-ok p₂) +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-≮: : ∀ {T U} → (tgt T ≮: tgt U) → (T ≮: U) +tgt-≮: (witness t p q) = witness (function-ok t) (tgt-function-ok p) (tgt-¬function-ok q) + +-- Language membership is decidable +dec-language : ∀ T t → Either (¬Language T t) (Language T t) +dec-language nil (scalar number) = Left (scalar-scalar number nil (λ ())) +dec-language nil (scalar boolean) = Left (scalar-scalar boolean nil (λ ())) +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 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 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 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 (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) +dec-language (T₁ ⇒ T₂) (function-err t) = mapLR function-err function-err (swapLR (dec-language T₁ t)) +dec-language never t = Left never +dec-language unknown t = Right unknown +dec-language (T₁ ∪ T₂) t = cond (λ p → cond (Left ∘ _,_ p) (Right ∘ right) (dec-language T₂ t)) (Right ∘ left) (dec-language T₁ t) +dec-language (T₁ ∩ T₂) t = cond (Left ∘ left) (λ p → cond (Left ∘ right) (Right ∘ _,_ p) (dec-language T₂ t)) (dec-language T₁ t) + +-- if T <: U then ¬Language U ⊆ ¬Language T +<:-impl-⊇ : ∀ {T U} → (T <: U) → ∀ t → ¬Language U t → ¬Language T t +<:-impl-⊇ {T} p t ¬Ut with dec-language T t +<:-impl-⊇ p t ¬Ut | Left ¬Tt = ¬Tt +<:-impl-⊇ p t ¬Ut | Right Tt = CONTRADICTION (language-comp t ¬Ut (p t Tt)) + +-- Subtyping is decidable +-- Honest, this terminates (because src T and tgt T decrease the depth of the type) + +{-# TERMINATING #-} +dec-subtyping : ∀ T U → Either (T ≮: U) (T <: U) +dec-subtyping T U = result where + + P : Tree → Set + P t = Either (¬Language T t) (Language U t) + + Q : Tree → Set + Q t = Either (T ≮: U) (P t) + + decQ : ∀ t → Q t + decQ t with dec-language T t | dec-language U t + decQ t | Left ¬Tt | _ = Right (Left ¬Tt) + decQ t | Right Tt | Left ¬Ut = Left (witness t Tt ¬Ut) + decQ t | Right _ | Right Ut = Right (Right Ut) + + lemma : P(scalar number) → P(scalar boolean) → P(scalar nil) → P(scalar string) → P(function) → (src U <: src T) → (tgt T <: tgt U) → (T <: U) + lemma (Left ¬Tt) boolP nilP stringP funP srcy tgty (scalar number) Tt = CONTRADICTION (language-comp (scalar number) ¬Tt Tt) + lemma (Right Ut) boolP nilP stringP funP srcy tgty (scalar number) Tt = Ut + lemma numP (Left ¬Tt) nilP stringP funP srcy tgty (scalar boolean) Tt = CONTRADICTION (language-comp (scalar boolean) ¬Tt Tt) + lemma numP (Right Ut) nilP stringP funP srcy tgty (scalar boolean) Tt = Ut + lemma numP boolP (Left ¬Tt) stringP funP srcy tgty (scalar nil) Tt = CONTRADICTION (language-comp (scalar nil) ¬Tt Tt) + lemma numP boolP (Right Ut) stringP funP srcy tgty (scalar nil) Tt = Ut + lemma numP boolP nilP (Left ¬Tt) funP srcy tgty (scalar string) Tt = CONTRADICTION (language-comp (scalar string) ¬Tt Tt) + lemma numP boolP nilP (Right Ut) funP srcy tgty (scalar string) Tt = Ut + lemma numP boolP nilP stringP (Left ¬Tt) srcy tgty function Tt = CONTRADICTION (language-comp function ¬Tt Tt) + lemma numP boolP nilP stringP (Right Ut) srcy tgty function Tt = Ut + lemma numP boolP nilP stringP funP srcy tgty (function-ok t) Tt = tgt-function-ok (tgty t (function-ok-tgt Tt)) + lemma numP boolP nilP stringP funP srcy tgty (function-err t) Tt = function-err-src (<:-impl-⊇ srcy t (src-¬function-err Tt)) + + result : Either (T ≮: U) (T <: U) + result with decQ (scalar number) + result | Left r = Left r + result | Right numP with decQ (scalar boolean) + result | Right numP | Left r = Left r + result | Right numP | Right boolP with decQ (scalar nil) + result | Right numP | Right boolP | Left r = Left r + result | Right numP | Right boolP | Right nilP with decQ (scalar string) + result | Right numP | Right boolP | Right nilP | Left r = Left r + result | Right numP | Right boolP | Right nilP | Right strP with decQ (function) + result | Right numP | Right boolP | Right nilP | Right strP | Left r = Left r + result | Right numP | Right boolP | Right nilP | Right strP | Right funP with dec-subtyping (src U) (src T) + result | Right numP | Right boolP | Right nilP | Right strP | Right funP | Left r = Left (src-≮: r) + result | Right numP | Right boolP | Right nilP | Right strP | Right funP | Right srcy with dec-subtyping (tgt T) (tgt U) + result | Right numP | Right boolP | Right nilP | Right strP | Right funP | Right srcy | Left r = Left (tgt-≮: r) + result | Right numP | Right boolP | Right nilP | Right strP | Right funP | Right srcy | Right tgty = Right (lemma numP boolP nilP strP funP srcy tgty) diff --git a/prototyping/Properties/Subtyping.agda b/prototyping/Properties/Subtyping.agda index 6c2559aa..19715380 100644 --- a/prototyping/Properties/Subtyping.agda +++ b/prototyping/Properties/Subtyping.agda @@ -7,63 +7,11 @@ open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond) 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 Properties.DecSubtyping using (language-comp; dec-language; tgt-function-ok; function-ok-tgt; function-err-src; ¬function-err-src; src-¬function-err) open import Properties.Equality using (_≢_) open import Properties.Functions using (_∘_) open import Properties.Product using (_×_; _,_) --- Language membership is decidable -dec-language : ∀ T t → Either (¬Language T t) (Language T t) -dec-language nil (scalar number) = Left (scalar-scalar number nil (λ ())) -dec-language nil (scalar boolean) = Left (scalar-scalar boolean nil (λ ())) -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 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 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 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 (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) -dec-language (T₁ ⇒ T₂) (function-err t) = mapLR function-err function-err (swapLR (dec-language T₁ t)) -dec-language never t = Left never -dec-language unknown t = Right unknown -dec-language (T₁ ∪ T₂) t = cond (λ p → cond (Left ∘ _,_ p) (Right ∘ right) (dec-language T₂ t)) (Right ∘ left) (dec-language T₁ t) -dec-language (T₁ ∩ T₂) t = cond (Left ∘ left) (λ p → cond (Left ∘ right) (Right ∘ _,_ p) (dec-language T₂ t)) (dec-language T₁ t) - --- ¬Language T is the complement of Language T -language-comp : ∀ {T} t → ¬Language T t → ¬(Language T t) -language-comp t (p₁ , p₂) (left q) = language-comp t p₁ q -language-comp t (p₁ , p₂) (right q) = language-comp t p₂ q -language-comp t (left p) (q₁ , q₂) = language-comp t p q₁ -language-comp t (right p) (q₁ , q₂) = language-comp t p q₂ -language-comp (scalar s) (scalar-scalar s p₁ p₂) (scalar s) = p₂ refl -language-comp (scalar s) (function-scalar s) (scalar s) = language-comp function (scalar-function s) function -language-comp (scalar s) never (scalar ()) -language-comp function (scalar-function ()) function -language-comp (function-ok t) (scalar-function-ok ()) (function-ok q) -language-comp (function-ok t) (function-ok p) (function-ok q) = language-comp t p q -language-comp (function-err t) (function-err p) (function-err q) = language-comp t q p - -- ≮: is the complement of <: ¬≮:-impl-<: : ∀ {T U} → ¬(T ≮: U) → (T <: U) ¬≮:-impl-<: {T} {U} p t q with dec-language U t @@ -73,12 +21,6 @@ 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) --- if T <: U then ¬Language U ⊆ ¬Language T -<:-impl-⊇ : ∀ {T U} → (T <: U) → ∀ t → ¬Language U t → ¬Language T t -<:-impl-⊇ {T} p t ¬Ut with dec-language T t -<:-impl-⊇ p t ¬Ut | Left ¬Tt = ¬Tt -<:-impl-⊇ p t ¬Ut | Right Tt = CONTRADICTION (language-comp t ¬Ut (p t Tt)) - -- reflexivity ≮:-refl : ∀ {T} → ¬(T ≮: T) ≮:-refl (witness t p q) = language-comp t q p @@ -117,40 +59,6 @@ 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 - -tgt-¬function-ok : ∀ {T t} → (¬Language (tgt T) t) → ¬Language T (function-ok t) -tgt-¬function-ok {T = nil} p = scalar-function-ok nil -tgt-¬function-ok {T = T₁ ⇒ T₂} p = function-ok p -tgt-¬function-ok {T = never} p = never -tgt-¬function-ok {T = unknown} (scalar-scalar s () p) -tgt-¬function-ok {T = unknown} (scalar-function ()) -tgt-¬function-ok {T = unknown} (scalar-function-ok ()) -tgt-¬function-ok {T = boolean} p = scalar-function-ok boolean -tgt-¬function-ok {T = number} p = scalar-function-ok number -tgt-¬function-ok {T = string} p = scalar-function-ok string -tgt-¬function-ok {T = T₁ ∪ T₂} (p₁ , p₂) = (tgt-¬function-ok p₁ , tgt-¬function-ok p₂) -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) - 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))) @@ -169,47 +77,6 @@ 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 ()))) -tgt-≮: : ∀ {T U} → (tgt T ≮: tgt U) → (T ≮: U) -tgt-≮: (witness t p q) = witness (function-ok t) (tgt-function-ok p) (tgt-¬function-ok q) - --- 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 @@ -229,9 +96,6 @@ unknown-src-≮: r (witness (function-ok (scalar s)) p (function-ok (scalar-scal 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) -src-≮: : ∀ {T U} → (src T ≮: src U) → (U ≮: T) -src-≮: (witness t p q) = witness (function-err t) (function-err-src q) (¬function-err-src p) - -- Properties of unknown and never unknown-≮: : ∀ {T U} → (T ≮: U) → (unknown ≮: U) unknown-≮: (witness t p q) = witness t unknown q @@ -245,56 +109,6 @@ unknown-≮:-never = witness (scalar nil) unknown never function-≮:-never : ∀ {T U} → ((T ⇒ U) ≮: never) function-≮:-never = witness function function never --- Subtyping is decidable --- Honest, this terminates (because src T and tgt T decrease the depth of the type) - -{-# TERMINATING #-} -dec-subtyping : ∀ T U → Either (T ≮: U) (T <: U) -dec-subtyping T U = result where - - P : Tree → Set - P t = Either (¬Language T t) (Language U t) - - Q : Tree → Set - Q t = Either (T ≮: U) (P t) - - decQ : ∀ t → Q t - decQ t with dec-language T t | dec-language U t - decQ t | Left ¬Tt | _ = Right (Left ¬Tt) - decQ t | Right Tt | Left ¬Ut = Left (witness t Tt ¬Ut) - decQ t | Right _ | Right Ut = Right (Right Ut) - - lemma : P(scalar number) → P(scalar boolean) → P(scalar nil) → P(scalar string) → P(function) → (src U <: src T) → (tgt T <: tgt U) → (T <: U) - lemma (Left ¬Tt) boolP nilP stringP funP srcy tgty (scalar number) Tt = CONTRADICTION (language-comp (scalar number) ¬Tt Tt) - lemma (Right Ut) boolP nilP stringP funP srcy tgty (scalar number) Tt = Ut - lemma numP (Left ¬Tt) nilP stringP funP srcy tgty (scalar boolean) Tt = CONTRADICTION (language-comp (scalar boolean) ¬Tt Tt) - lemma numP (Right Ut) nilP stringP funP srcy tgty (scalar boolean) Tt = Ut - lemma numP boolP (Left ¬Tt) stringP funP srcy tgty (scalar nil) Tt = CONTRADICTION (language-comp (scalar nil) ¬Tt Tt) - lemma numP boolP (Right Ut) stringP funP srcy tgty (scalar nil) Tt = Ut - lemma numP boolP nilP (Left ¬Tt) funP srcy tgty (scalar string) Tt = CONTRADICTION (language-comp (scalar string) ¬Tt Tt) - lemma numP boolP nilP (Right Ut) funP srcy tgty (scalar string) Tt = Ut - lemma numP boolP nilP stringP (Left ¬Tt) srcy tgty function Tt = CONTRADICTION (language-comp function ¬Tt Tt) - lemma numP boolP nilP stringP (Right Ut) srcy tgty function Tt = Ut - lemma numP boolP nilP stringP funP srcy tgty (function-ok t) Tt = tgt-function-ok (tgty t (function-ok-tgt Tt)) - lemma numP boolP nilP stringP funP srcy tgty (function-err t) Tt = function-err-src (<:-impl-⊇ srcy t (src-¬function-err Tt)) - - result : Either (T ≮: U) (T <: U) - result with decQ (scalar number) - result | Left r = Left r - result | Right numP with decQ (scalar boolean) - result | Right numP | Left r = Left r - result | Right numP | Right boolP with decQ (scalar nil) - result | Right numP | Right boolP | Left r = Left r - result | Right numP | Right boolP | Right nilP with decQ (scalar string) - result | Right numP | Right boolP | Right nilP | Left r = Left r - result | Right numP | Right boolP | Right nilP | Right strP with decQ (function) - result | Right numP | Right boolP | Right nilP | Right strP | Left r = Left r - result | Right numP | Right boolP | Right nilP | Right strP | Right funP with dec-subtyping (src U) (src T) - result | Right numP | Right boolP | Right nilP | Right strP | Right funP | Left r = Left (src-≮: r) - result | Right numP | Right boolP | Right nilP | Right strP | Right funP | Right srcy with dec-subtyping (tgt T) (tgt U) - result | Right numP | Right boolP | Right nilP | Right strP | Right funP | Right srcy | Left r = Left (tgt-≮: r) - result | Right numP | Right boolP | Right nilP | Right strP | Right funP | Right srcy | Right tgty = Right (lemma numP boolP nilP strP funP srcy tgty) - -- 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,