diff --git a/prototyping/Luau/OverloadedFunctions.agda b/prototyping/Luau/OverloadedFunctions.agda new file mode 100644 index 00000000..69620450 --- /dev/null +++ b/prototyping/Luau/OverloadedFunctions.agda @@ -0,0 +1,26 @@ +{-# OPTIONS --rewriting #-} + +open import FFI.Data.Either using (Either; Left; Right) +open import Luau.Type using (Type; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; src) +open import Properties.Subtyping using (dec-subtyping) + +module Luau.OverloadedFunctions where + +-- resolve F V is the result of applying a function of type F +-- to an argument of type V. This does function overload resolution, +-- e.g. `resolve (((number) -> string) & ((string) -> number)) (number)` is `string`. + +resolve : Type → Type → Type +resolve nil V = never +resolve (S ⇒ T) V = T +resolve never V = never +resolve unknown V = unknown +resolve boolean V = never +resolve number V = never +resolve string V = never +resolve (F ∪ G) V = (resolve F V) ∪ (resolve G V) +resolve (F ∩ G) V with dec-subtyping V (src F) | dec-subtyping V (src G) +resolve (F ∩ G) V | Left p | Left q = resolve F V ∪ resolve G V +resolve (F ∩ G) V | Right p | Left q = resolve F V +resolve (F ∩ G) V | Left p | Right q = resolve G V +resolve (F ∩ G) V | Right p | Right q = resolve F V ∩ resolve G V diff --git a/prototyping/Luau/StrictMode/ToString.agda b/prototyping/Luau/StrictMode/ToString.agda index eee5722e..dd99f4ee 100644 --- a/prototyping/Luau/StrictMode/ToString.agda +++ b/prototyping/Luau/StrictMode/ToString.agda @@ -27,7 +27,7 @@ treeToString (scalar boolean) n v = v ++ " is a boolean" treeToString (scalar string) n v = v ++ " is a string" treeToString (scalar nil) n v = v ++ " is nil" treeToString function n v = v ++ " is a function" -treeToString (function-ok t) n v = treeToString t n (v ++ "()") +treeToString (function-ok s t) n v = treeToString t (suc n) (v ++ "(" ++ w ++ ")") ++ " when\n " ++ treeToString s (suc n) w where w = tmp n treeToString (function-err t) n v = v ++ "(" ++ w ++ ") can error when\n " ++ treeToString t (suc n) w where w = tmp n subtypeWarningToString : ∀ {T U} → (T ≮: U) → String diff --git a/prototyping/Luau/Subtyping.agda b/prototyping/Luau/Subtyping.agda index 943f459b..6e5cf20c 100644 --- a/prototyping/Luau/Subtyping.agda +++ b/prototyping/Luau/Subtyping.agda @@ -13,7 +13,7 @@ data Tree : Set where scalar : ∀ {T} → Scalar T → Tree function : Tree - function-ok : Tree → Tree + function-ok : Tree → Tree → Tree function-err : Tree → Tree data Language : Type → Tree → Set @@ -23,7 +23,8 @@ data Language where scalar : ∀ {T} → (s : Scalar T) → Language T (scalar s) function : ∀ {T U} → Language (T ⇒ U) function - function-ok : ∀ {T U u} → (Language U u) → Language (T ⇒ U) (function-ok u) + function-ok₁ : ∀ {T U t u} → (¬Language T t) → Language (T ⇒ U) (function-ok t u) + function-ok₂ : ∀ {T U t u} → (Language U u) → Language (T ⇒ U) (function-ok t 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 @@ -35,9 +36,9 @@ 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-ok : ∀ {S t u} → (Scalar S) → ¬Language S (function-ok t u) 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-ok : ∀ {T U t u} → (Language T t) → (¬Language U u) → ¬Language (T ⇒ U) (function-ok t u) function-err : ∀ {T U t} → (Language T t) → ¬Language (T ⇒ U) (function-err t) _,_ : ∀ {T U t} → ¬Language T t → ¬Language U t → ¬Language (T ∪ U) t left : ∀ {T U t} → ¬Language T t → ¬Language (T ∩ U) t diff --git a/prototyping/Properties/DecSubtyping.agda b/prototyping/Properties/DecSubtyping.agda index 2d990bae..d8c6ae8e 100644 --- a/prototyping/Properties/DecSubtyping.agda +++ b/prototyping/Properties/DecSubtyping.agda @@ -4,7 +4,7 @@ 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.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-ok₁; 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 (_∘_) @@ -19,8 +19,10 @@ 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-ok s t) (scalar-function-ok ()) (function-ok₁ _) +language-comp (function-ok s t) (scalar-function-ok ()) (function-ok₂ _) +language-comp (function-ok s t) (function-ok p _) (function-ok₁ q) = language-comp s q p +language-comp (function-ok s 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 @@ -64,43 +66,6 @@ src-¬function-err {T = T₁ ∩ T₂} (p₁ , 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 (λ ())) @@ -108,32 +73,32 @@ 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-ok s 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-ok s 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-ok s 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-ok s 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-ok s t) = cond (Right ∘ function-ok₁) (λ p → mapLR (function-ok p) function-ok₂ (dec-language T₂ t)) (dec-language T₁ s) 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 @@ -147,51 +112,6 @@ dec-language (T₁ ∩ T₂) t = cond (Left ∘ left) (λ p → cond (Left ∘ r <:-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) +-- TODO: Prove this! -{-# 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) +postulate dec-subtyping : ∀ T U → Either (T ≮: U) (T <: U) diff --git a/prototyping/Properties/OverloadedFunctions.agda b/prototyping/Properties/OverloadedFunctions.agda new file mode 100644 index 00000000..b8c0efb2 --- /dev/null +++ b/prototyping/Properties/OverloadedFunctions.agda @@ -0,0 +1,49 @@ +{-# OPTIONS --rewriting #-} + +module Properties.OverloadedFunctions where + +open import FFI.Data.Either using (Either; Left; Right) +open import Luau.OverloadedFunctions using (resolve) +open import Luau.Subtyping using (_<:_; _≮:_) +open import Luau.Type using (Type; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; src) +open import Properties.Subtyping using (dec-subtyping) + +-- Function overload resolution respects subtyping + +resolve-<: : ∀ F {S T} → (S <: T) → (resolve F S <: resolve F T) +resolve-<: nil p = <:-refl +resolve-<: (F ⇒ F₁) p = <:-refl +resolve-<: never p = <:-refl +resolve-<: unknown p = <:-refl +resolve-<: boolean p = <:-refl +resolve-<: number p = <:-refl +resolve-<: string p = <:-refl +resolve-<: (F ∪ G) p = ∪-<: (resolve-<: F p) (resolve-<: G p) +resolve-<: (F ∩ G) {S} {T} p with dec-subtyping S (src F) | dec-subtyping S (src G) | dec-subtyping T (src F) | dec-subtyping T (src G) +resolve-<: (F ∩ G) {S} {T} p | Left q₁ | Left q₂ | Left q₃ | Left q₄ = ∪-<: (resolve-<: F p) (resolve-<: G p) +resolve-<: (F ∩ G) {S} {T} p | _ | Left q₂ | _ | Right q₄ = CONTRADICTION (<:-impl-¬≮: (<:-trans p q₄) q₂) +resolve-<: (F ∩ G) {S} {T} p | Left q₁ | _ | Right q₃ | _ = CONTRADICTION (<:-impl-¬≮: (<:-trans p q₃) q₁) +resolve-<: (F ∩ G) {S} {T} p | Left q₁ | Right q₂ | Left q₃ | Left q₄ = <:-trans (resolve-<: G p) <:-∪-right +resolve-<: (F ∩ G) {S} {T} p | Left q₁ | Right q₂ | Left q₃ | Right q₄ = resolve-<: G p +resolve-<: (F ∩ G) {S} {T} p | Right q₁ | Left q₂ | Left q₃ | Left q₄ = <:-trans (resolve-<: F p) <:-∪-left +resolve-<: (F ∩ G) {S} {T} p | Right q₁ | Left q₂ | Right q₃ | Left q₄ = resolve-<: F p +resolve-<: (F ∩ G) {S} {T} p | Right q₁ | Right q₂ | Left q₃ | Left q₄ = <:-trans <:-∩-left (<:-trans (resolve-<: F p) <:-∪-left) +resolve-<: (F ∩ G) {S} {T} p | Right q₁ | Right q₂ | Left q₃ | Right q₄ = <:-trans <:-∩-right (resolve-<: G p) +resolve-<: (F ∩ G) {S} {T} p | Right q₁ | Right q₂ | Right q₃ | Left q₄ = <:-trans <:-∩-left (resolve-<: F p) +resolve-<: (F ∩ G) {S} {T} p | Right q₁ | Right q₂ | Right q₃ | Right q₄ = ∩-<: (resolve-<: F p) (resolve-<: G p) + +-- A function type is a subtype of any of its overloadings +resolve-intro : ∀ F V → (V ≮: never) → (V <: src F) → F <: (V ⇒ resolve F V) +resolve-intro nil V p₁ p₂ = CONTRADICTION (<:-impl-¬≮: p₂ p₁) +resolve-intro (S ⇒ T) V p₁ p₂ = function-<: p₂ <:-refl +resolve-intro never V p₁ p₂ = <:-never +resolve-intro unknown V p₁ p₂ = CONTRADICTION (<:-impl-¬≮: p₂ p₁) +resolve-intro boolean V p₁ p₂ = CONTRADICTION (<:-impl-¬≮: p₂ p₁) +resolve-intro number V p₁ p₂ = CONTRADICTION (<:-impl-¬≮: p₂ p₁) +resolve-intro string V p₁ p₂ = CONTRADICTION (<:-impl-¬≮: p₂ p₁) +resolve-intro (F ∪ G) V p₁ p₂ = <:-∪-lub (<:-trans (resolve-intro F V p₁ (<:-trans p₂ <:-∩-left)) (function-<: <:-refl <:-∪-left)) (<:-trans (resolve-intro G V p₁ (<:-trans p₂ <:-∩-right)) (function-<: <:-refl <:-∪-right)) +resolve-intro (F ∩ G) V p₁ p₂ with dec-subtyping V (src F) | dec-subtyping V (src G) +resolve-intro (F ∩ G) V p₁ p₂ | Left q₁ | Left q₂ = <:-trans (∩-<: (resolve-intro F (V ∩ src F) (<:-never-right p₂ q₂) <:-∩-right) ((resolve-intro G (V ∩ src G) (<:-never-left p₂ q₁) <:-∩-right))) (<:-trans function-∩-∪-<: (function-<: (<:-trans (<:-∩-glb <:-refl p₂) <:-∩-dist-∪) (∪-<: (resolve-<: F <:-∩-left) (resolve-<: G <:-∩-left)))) +resolve-intro (F ∩ G) V p₁ p₂ | Left q₁ | Right q₂ = <:-trans <:-∩-right (resolve-intro G V p₁ q₂) +resolve-intro (F ∩ G) V p₁ p₂ | Right q₁ | Left q₂ = <:-trans <:-∩-left (resolve-intro F V p₁ q₁) +resolve-intro (F ∩ G) V p₁ p₂ | Right q₁ | Right q₂ = <:-trans (∩-<: (resolve-intro F V p₁ q₁) (resolve-intro G V p₁ q₂)) function-∩-<: diff --git a/prototyping/Properties/Subtyping.agda b/prototyping/Properties/Subtyping.agda index 19715380..664314d2 100644 --- a/prototyping/Properties/Subtyping.agda +++ b/prototyping/Properties/Subtyping.agda @@ -4,10 +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 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.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-ok₁; 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.DecSubtyping using (language-comp; dec-language; function-err-src; ¬function-err-src; src-¬function-err) open import Properties.Equality using (_≢_) open import Properties.Functions using (_∘_) open import Properties.Product using (_×_; _,_) @@ -51,7 +51,7 @@ scalar-≮:-function : ∀ {S T U} → (Scalar U) → (U ≮: (S ⇒ T)) scalar-≮:-function s = witness (scalar s) (scalar s) (function-scalar s) unknown-≮:-scalar : ∀ {U} → (Scalar U) → (unknown ≮: U) -unknown-≮:-scalar s = witness (function-ok (scalar s)) unknown (scalar-function-ok s) +unknown-≮:-scalar s = witness (function) unknown (scalar-function s) scalar-≮:-never : ∀ {U} → (Scalar U) → (U ≮: never) scalar-≮:-never s = witness (scalar s) (scalar s) never @@ -59,7 +59,7 @@ 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) -skalar-function-ok : ∀ {t} → (¬Language skalar (function-ok t)) +skalar-function-ok : ∀ {s t} → (¬Language skalar (function-ok s t)) skalar-function-ok = (scalar-function-ok number , (scalar-function-ok string , (scalar-function-ok nil , scalar-function-ok boolean))) skalar-scalar : ∀ {T} (s : Scalar T) → (Language skalar (scalar s)) @@ -68,15 +68,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 ()))) - 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 @@ -91,10 +82,10 @@ 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) +unknown-src-≮: (witness t p _) (witness (scalar s) q (function-scalar s)) = witness t p (src-¬scalar s q) +unknown-src-≮: (witness _ _ _) (witness function _ (scalar-function ())) +unknown-src-≮: (witness _ _ _) (witness (function-ok _ t) _ (function-ok _ r)) = CONTRADICTION (language-comp t r unknown) +unknown-src-≮: (witness _ _ _) (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) @@ -139,21 +130,17 @@ set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , u) Qtu (S₂t , ¬T₂u) S₁t | Right r = r ¬T₁u : ¬(Language 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 + ¬T₁u T₁u with p (function-ok t u) (function-ok₂ T₁u) + ¬T₁u T₁u | function-ok₁ ¬S₂t = CONTRADICTION (language-comp t ¬S₂t S₂t) + ¬T₁u T₁u | function-ok₂ T₂u = ¬T₂u T₂u -not-quite-set-theoretic-only-if : ∀ {S₁ T₁ S₂ T₂} → - - -- We don't quite have that this is a set-theoretic model - -- it's only true when Language T₁ and ¬Language T₂ t₂ are inhabited - -- in particular it's not true when T₁ is never, or T₂ is unknown. - ∀ s₂ t₂ → Language S₂ s₂ → ¬Language T₂ t₂ → +set-theoretic-only-if : ∀ {S₁ T₁ S₂ 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₂))) → (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 +set-theoretic-only-if {S₁} {T₁} {S₂} {T₂} p = r where Q : (Tree × Tree) → Set Q (t , u) = Either (¬Language S₁ t) (Language T₁ u) @@ -166,34 +153,10 @@ not-quite-set-theoretic-only-if {S₁} {T₁} {S₂} {T₂} s₂ t₂ S₂s₂ 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-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) | 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 ((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 - (function-ok (scalar number)) (function-ok (scalar number)) - (function-ok (scalar-scalar number string (λ ()))) - --- At some point we may deal with overloaded function resolution, which should fix this problem... --- The reason why this is connected to overloaded functions is that currently we have that the type of --- f(x) is (tgt T) where f:T. Really we should have the type depend on the type of x, that is use (tgt T U), --- where U is the type of x. In particular (tgt (S => T) (U & V)) should be the same as (tgt ((S&U) => T) V) --- and tgt(never => T) should be unknown. For example --- --- tgt((number => string) & (string => bool))(number) --- is tgt(number => string)(number) & tgt(string => bool)(number) --- is tgt(number => string)(number) & tgt(string => bool)(number&unknown) --- is tgt(number => string)(number) & tgt(string&number => bool)(unknown) --- is tgt(number => string)(number) & tgt(never => bool)(unknown) --- is string & unknown --- is string --- --- there's some discussion of this in the Gentle Introduction paper. + 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-ok s t) (function-ok₁ ¬S₁s) with dec-language S₂ s + r (function-ok s t) (function-ok₁ ¬S₁s) | Left ¬S₂s = function-ok₁ ¬S₂s + r (function-ok s t) (function-ok₁ ¬S₁s) | Right S₂s = ? -- CONTRADICTION (p Q q (s , t₂) (Left ¬S₁s) (S₂s , language-comp t₂ ¬T₂t₂)) + r (function-ok s t) (function-ok₂ T₁t) with dec-language T₂ t + r (function-ok s 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 s t) (function-ok₂ T₁t) | Right T₂t = function-ok₂ T₂t