mirror of
https://github.com/luau-lang/luau.git
synced 2025-05-04 10:33:46 +01:00
WIP
This commit is contained in:
ajeffrey@roblox.com
parent
b3e538a328
commit
c7d6cbfc95
6 changed files with 113 additions and 154 deletions
26
prototyping/Luau/OverloadedFunctions.agda
Normal file
26
prototyping/Luau/OverloadedFunctions.agda
Normal file
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
49
prototyping/Properties/OverloadedFunctions.agda
Normal file
49
prototyping/Properties/OverloadedFunctions.agda
Normal file
|
|
@ -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-∩-<:
|
||||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue