We outline a method to extend the TypeScript system to Lua. However, as TypeScript's subtype semantics do not satisfy completeness (only soundness), we emphasize a method for subtyping that is both sound and complete.
...
2. Subtyping using operators
In this section, we develop just enough definitions to aid in the implementation of such a system. We will define precisely what it means to be a subtype and show informally that our definition is sensible (i.e., it is consistent with basic subtype rules).
Denote an element e of type τ as e:τ. Define a subtype operator ≤ where σ≤τ to indicate that σ is a subtype of τ. What does it mean for a type to be the subtype of another type?
Definition 1: The set of all objects x:τ is the domain of τ notated [[τ]]
Remark: We don't observe types under the framework of type theory. Instead, types are predicates where x:τ iff x∈[[τ]].
Definition 2a: The set of operations, denoted Ω, is the set where any element is of typeo∈Ω:∏n[[τi]]→∏m[[σi]].
Definition 2b: Suppose we have o:∏[[ai]]→∏[[bi]]∈Ω and o′:∏[[ai′]]→∏[[bi′]]∈Ω. Then o=o′ iff ov=o′v for all v:∏ai∈∏[[ai]]. We will not develop this further.
Definition 3: Denote the set of operators that accept a parameter typed a as Ωa. Then we define a≤b as Ωa⊆Ωb.
Remark: This is analogous to the subsumption rule in type theory. We'll see later that the sets Ωa are far easier to compute than subtype rules.
Definition 4: Type union is notated a+b or a∣b where x:a+b⟺(x:a)∨(x:b)
Definition 5: Type intersection is notated a⋅b where x:a⋅b⟺(x:a)∧(x:b)
Theorem 1: The following are true about types a,b,c
a≤a
a≤b and b≤c implies a≤c
The theorem shows that ≤ behaves as we would expect. The proof is trivial and excluded.
Lemma 1:[[a∣b]]=[[a]]∪[[b]] and [[a⋅b]]=[[a]]∩[[b]]
Proof
First:
Let any x:a∣b∈[[a∣b]] then if x:a we have x∈[[a]] and if x:b we have x∈[[b]]hence x∈[[a]]∪[[b]]. Now the converse. Let any x:a∈[[a]] then trivially x:a∣b is true so x∈[[a∣b]]. Similarly, x∈[[b]]⟹x∈[[a∣b]] and so we're done. □
Second: Proceed similarly to above.
Theorem 2:Ωa∣b=Ωa∩Ωb and Ωa⋅b=Ωa∪Ωb
Proof
First:
Let any ϕ∈Ωa∣b and WLOG let ϕ:[[a∣b]]×U→V and construct ϕ1:[[a]]×U→V as ϕ1:x×y↦ϕ(x×y) where x∈[[a]] so by Definition 2 we have Ωa⊆Ωa∣b. Similarly, we have Ωb⊆Ωa∣b. Conversely, let any ϕ1∈Ωa and ϕ2∈Ωb and WLOG suppose ϕ1:[[a]]×U1→V1 and ϕ2:[[b]]×U2→V2 then we can construct a partial map ϕ:([[a]]∪[[b]])×(U1∪U2)⇀(V1∪V2) where
and ϕ∈Ωa∣b as [[a]]∪[[b]]=[[a∣b]] by Lemma 1, concluding this proof. □
Second: Proceed similarly to above.
Corollary 1: If a≤c and b≤d then a+b≤c+d
Proof
By Definition 2, Ωa⊆Ωc and Ωb⊆Ωd.
By Theorem 2, Ωa+b=Ωa∩Ωb⊆Ωc∩Ωd=Ωc+d, concluding this proof. □
Theorem 3: If c≤a and b≤d then a→b≤c→d.
Remark: This is an important result and shows that function parameters are contravariant while function return types are covariant.
Proof
Let any ϕ1∈Ωa→b where WLOG ϕ1:[[a→b]]×U1→V=ϕ1:Ωa×U1→V.
Construct function φx1:[[b]]×U2→V so for all x∈[[c]] and some f∈Ωc⊆Ωa we have φx1(f(x),⋯)=ϕ1(f,⋯).
Since Ωb⊆Ωd and ϕx1∈Ωb we can construct partial function φx2:[[d]]×U2⇀V∈Ωd so that for all x∈[[c]] and some f∈Ωc we have φx2(f(x),⋯)=φx1(f(x),⋯).
Finally, we can construct ϕ2:[[c→d]]×U3→V such that ϕ2=φx2=φx1=ϕ1 for all x∈[[c]]. As ϕ2∈Ωc→d, we have Ωa→b⊆Ωc→d concluding this proof. □