πŸ“–
Notes
  • Typed Lua
    • Typed Lua (Old)
  • Fast Userspace Kernel (FUsK)
  • Compiler Optimization
  • RISC-V Merged CmpBr
  • School Projects
    • cc3k
    • wlp4cc
  • Microkernel Design
  • cxkernel
Powered by GitBook
On this page
  • 1. Preface
  • 2. Subtyping using operators
  • 3. Subtyping as a SAT problem
  • 4. ​Implementation
  • 5. Further work and limitations

Was this helpful?

Typed Lua

Some random thoughts and ideas about types

NextTyped Lua (Old)

Last updated 2 years ago

Was this helpful?

1. Preface

We outline a method to extend the TypeScript system to Lua. However, as TypeScript's subtype semantics (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 ee​ of type Ο„\tauτ​ as e:Ο„e:\taue:τ​. Define a subtype operator ≀\le≀​ where σ≀τ\sigma\le\tauσ≀τ​ to indicate that Οƒ\sigmaσ​ is a subtype of Ο„\tauτ​. What does it mean for a type to be the subtype of another type?

Definition 1: The set of all objects x:Ο„x:\taux:Ο„ is the domain of Ο„\tauτ​ notated [ ⁣[Ο„] ⁣][\![\tau]\!][[Ο„]]

Remark: We don't observe types under the framework of type theory. Instead, types are predicates where x:Ο„x:\taux:τ​ iff x∈[ ⁣[Ο„] ⁣]x\in[\![\tau]\!]x∈[[Ο„]].

Definition 2a: The set of operations, denoted Ξ©\OmegaΩ​, is the set where any element is of typeo∈Ω:∏n[ ⁣[Ο„i] ⁣]β†’βˆm[ ⁣[Οƒi] ⁣]o\in\Omega:\prod_n[\![\tau_i]\!]\to\prod_m[\![\sigma_i]\!]o∈Ω:∏n​[[Ο„i​]]β†’βˆm​[[Οƒi​]].

Definition 2b: Suppose we have o:∏[ ⁣[ai] ⁣]β†’βˆ[ ⁣[bi] ⁣]∈Ωo:\prod [\![a_i]\!]\to\prod [\![b_i]\!]\in\Omegao:∏[[ai​]]β†’βˆ[[bi​]]βˆˆΞ©β€‹ and oβ€²:∏[ ⁣[aiβ€²] ⁣]β†’βˆ[ ⁣[biβ€²] ⁣]∈Ωo':\prod [\![a_i']\!]\to\prod [\![b_i']\!]\in\Omegaoβ€²:∏[[ai′​]]β†’βˆ[[bi′​]]∈Ω. Then o=oβ€²o=o'o=oβ€² iff oβ€…β€Šv=oβ€²β€…β€Švo\;v=o'\;vov=oβ€²v​ for all v:∏ai∈∏[ ⁣[ai] ⁣]v:\prod a_i\in\prod[\![a_i]\!]v:∏aiβ€‹βˆˆβˆ[[ai​]]​. We will not develop this further.

Definition 3: Denote the set of operators that accept a parameter typed aaa​ as Ξ©a\Omega_aΞ©a​​. Then we define a≀ba\le ba≀b​ as Ξ©aβŠ†Ξ©b\Omega_a\subseteq\Omega_bΞ©aβ€‹βŠ†Ξ©b​.​

Remark: This is analogous to the subsumption rule in type theory. We'll see later that the sets Ξ©a\Omega_aΞ©a​​ are far easier to compute than subtype rules.

Definition 4: Type union is notated a+ba+ba+b​ or aβ€…β€Šβˆ£β€…β€Šba\;|\;ba∣b where x:a+bβ€…β€ŠβŸΊβ€…β€Š(x:a)∨(x:b)x:a+b \iff (x:a)\lor (x:b)x:a+b⟺(x:a)∨(x:b)

Definition 5: Type intersection is notated aβ‹…ba\cdot baβ‹…b​ where x:aβ‹…bβ€…β€ŠβŸΊβ€…β€Š(x:a)∧(x:b)x:a\cdot b\iff (x:a)\land(x:b)x:aβ‹…b⟺(x:a)∧(x:b)​

Theorem 1: The following are true about types a,b,ca,b,ca,b,c​

  1. a≀aa\le aa≀a​

  2. a≀ba\le ba≀b​ and b≀cb\le cb≀c​ implies a≀ca\le ca≀c​

The theorem shows that ≀\le≀​ behaves as we would expect. The proof is trivial and excluded.

Lemma 1: [ ⁣[aβ€…β€Šβˆ£β€…β€Šb] ⁣]=[ ⁣[a] ⁣]βˆͺ[ ⁣[b] ⁣][\![a\;|\;b]\!] = [\![a]\!]\cup [\![b]\!][[a∣b]]=[[a]]βˆͺ[[b]] and [ ⁣[aβ‹…b] ⁣]=[ ⁣[a] ⁣]∩[ ⁣[b] ⁣][\![a\cdot b]\!] = [\![a]\!]\cap [\![b]\!][[aβ‹…b]]=[[a]]∩[[b]]​

Proof

First:

Let any x:aβ€…β€Šβˆ£β€…β€Šb∈[ ⁣[aβ€…β€Šβˆ£β€…β€Šb] ⁣]x:a\;|\;b \in[\![a\;|\;b]\!]x:a∣b∈[[a∣b]] then if x:ax:ax:a​ we have x∈[ ⁣[a] ⁣]x\in[\![a]\!]x∈[[a]]​ and if x:bx:bx:b​ we have x∈[ ⁣[b] ⁣]x\in[\![b]\!]x∈[[b]]hence x∈[ ⁣[a] ⁣]βˆͺ[ ⁣[b] ⁣]x\in[\![a]\!]\cup[\![b]\!]x∈[[a]]βˆͺ[[b]]. Now the converse. Let any x:a∈[ ⁣[a] ⁣]x:a\in [\![a]\!]x:a∈[[a]] then trivially x:aβ€…β€Šβˆ£β€…β€Šbx:a\;|\;bx:a∣b is true so x∈[ ⁣[aβ€…β€Šβˆ£β€…β€Šb] ⁣]x\in[\![a\;|\;b]\!]x∈[[a∣b]]. Similarly, x∈[ ⁣[b] ⁣]β€…β€ŠβŸΉβ€…β€Šx∈[ ⁣[aβ€…β€Šβˆ£β€…β€Šb] ⁣]x\in[\![b]\!]\implies x\in[\![a\;|\;b]\!]x∈[[b]]⟹x∈[[a∣b]]​ and so we're done. β–‘\Boxβ–‘

Second: Proceed similarly to above.​

Theorem 2: Ξ©aβ€…β€Šβˆ£β€…β€Šb=Ξ©a∩Ωb\Omega_{a\;|\;b}=\Omega_a\cap\Omega_bΞ©a∣b​=Ξ©aβ€‹βˆ©Ξ©b​ and ​Ωaβ‹…b=Ξ©aβˆͺΞ©b\Omega_{a\cdot b}=\Omega_a\cup\Omega_bΞ©aβ‹…b​=Ξ©a​βˆͺΞ©b​​

Proof

First:

Let any Ο•βˆˆΞ©aβ€…β€Šβˆ£β€…β€Šb\phi\in\Omega_{a\;|\;b}Ο•βˆˆΞ©a∣b​​ and WLOG let Ο•:[ ⁣[aβ€…β€Šβˆ£β€…β€Šb] ⁣]Γ—Uβ†’V\phi:[\![a\;|\;b]\!]\times U\to VΟ•:[[a∣b]]Γ—Uβ†’V and construct Ο•1:[ ⁣[a] ⁣]Γ—Uβ†’V\phi_1:[\![a]\!]\times U\to VΟ•1​:[[a]]Γ—Uβ†’V​ as Ο•1:xΓ—y↦ϕ(xΓ—y)\phi_1: x\times y\mapsto \phi(x\times y)Ο•1​:xΓ—y↦ϕ(xΓ—y)​ where x∈[ ⁣[a] ⁣]x\in[\![a]\!]x∈[[a]] so by Definition 2 we have Ξ©aβŠ†Ξ©aβ€…β€Šβˆ£β€…β€Šb\Omega_a\subseteq\Omega_{a\;|\;b}Ξ©aβ€‹βŠ†Ξ©a∣b​​. Similarly, we have Ξ©bβŠ†Ξ©aβ€…β€Šβˆ£β€…β€Šb\Omega_b\subseteq\Omega_{a\;|\;b}Ξ©bβ€‹βŠ†Ξ©a∣b​​. Conversely, let any Ο•1∈Ωa\phi_1\in\Omega_aΟ•1β€‹βˆˆΞ©a​ and Ο•2∈Ωb\phi_2\in\Omega_bΟ•2β€‹βˆˆΞ©b​ and WLOG suppose Ο•1:[ ⁣[a] ⁣]Γ—U1β†’V1\phi_1:[\![a]\!]\times U_1\to V_1Ο•1​:[[a]]Γ—U1​→V1​ and Ο•2:[ ⁣[b] ⁣]Γ—U2β†’V2\phi_2:[\![b]\!]\times U_2\to V_2Ο•2​:[[b]]Γ—U2​→V2​ then we can construct a partial map Ο•:([ ⁣[a] ⁣]βˆͺ[ ⁣[b] ⁣])Γ—(U1βˆͺU2)⇀(V1βˆͺV2)\phi:([\![a]\!]\cup [\![b]\!])\times (U_1\cup U_2)\rightharpoonup (V_1\cup V_2)Ο•:([[a]]βˆͺ[[b]])Γ—(U1​βˆͺU2​)⇀(V1​βˆͺV2​) where

Ο•:xΓ—y↦{Ο•1(xΓ—y)ifΒ x∈[ ⁣[a] ⁣],Β y∈U1Ο•2(xΓ—y)ifΒ x∈[ ⁣[b] ⁣],Β y∈U2\phi: x\times y\mapsto\begin{cases}\phi_1(x\times y) &\text{if $x\in[\![a]\!]$, $y\in U_1$}\\\phi_2(x\times y)&\text{if $x\in[\![b]\!]$, $y\in U_2$}\end{cases}Ο•:xΓ—y↦{Ο•1​(xΓ—y)Ο•2​(xΓ—y)​ifΒ x∈[[a]],Β y∈U1​ifΒ x∈[[b]],Β y∈U2​​​

and Ο•βˆˆΞ©aβ€…β€Šβˆ£β€…β€Šb\phi\in \Omega_{a\;|\;b}Ο•βˆˆΞ©a∣b​​ as [ ⁣[a] ⁣]βˆͺ[ ⁣[b] ⁣]=[ ⁣[aβ€…β€Šβˆ£β€…β€Šb] ⁣][\![a]\!]\cup [\![b]\!] = [\![a\;|\;b]\!][[a]]βˆͺ[[b]]=[[a∣b]]​ by Lemma 1, concluding this proof. β–‘\Boxβ–‘

Second: Proceed similarly to above.​

Corollary 1: If a≀ca\le ca≀c​ and b≀db\le db≀d​ then a+b≀c+da+b\le c+da+b≀c+d

Proof

By Definition 2, Ξ©aβŠ†Ξ©c\Omega_a\subseteq\Omega_cΞ©aβ€‹βŠ†Ξ©c​​ and Ξ©bβŠ†Ξ©d\Omega_b\subseteq\Omega_dΞ©bβ€‹βŠ†Ξ©d​​.

By Theorem 2, Ξ©a+b=Ξ©a∩ΩbβŠ†Ξ©c∩Ωd=Ξ©c+d\Omega_{a+b} = \Omega_a\cap\Omega_b\subseteq\Omega_c\cap\Omega_d=\Omega_{c+d}Ξ©a+b​=Ξ©aβ€‹βˆ©Ξ©bβ€‹βŠ†Ξ©cβ€‹βˆ©Ξ©d​=Ξ©c+d​​, concluding this proof. β–‘\Box░​

Theorem 3: If c≀ac\le ac≀a​ and b≀db\le db≀d​ then aβ†’b≀cβ†’da\to b\le c\to daβ†’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\phi_1\in\Omega_{a\to b}Ο•1β€‹βˆˆΞ©aβ†’b​ where WLOG Ο•1:[ ⁣[aβ†’b] ⁣]Γ—U1β†’V=Ο•1:Ξ©aΓ—U1β†’V\phi_1:[\![a\to b]\!]\times U_1\to V = \phi_1:\Omega_a\times U_1\to VΟ•1​:[[aβ†’b]]Γ—U1​→V=Ο•1​:Ξ©a​×U1​→V.

Construct​ function Ο†x1:[ ⁣[b] ⁣]Γ—U2β†’V\varphi_x^1: [\![b]\!]\times U_2\to VΟ†x1​:[[b]]Γ—U2​→V so for all x∈[ ⁣[c] ⁣]x\in[\![c]\!]x∈[[c]] and some f∈ΩcβŠ†Ξ©af\in\Omega_c\subseteq\Omega_af∈Ωcβ€‹βŠ†Ξ©a​ we have Ο†x1(f(x),⋯ )=Ο•1(f,⋯ )\varphi^1_x(f(x),\cdots)=\phi_1(f, \cdots)Ο†x1​(f(x),β‹―)=Ο•1​(f,β‹―).

Since Ξ©bβŠ†Ξ©d\Omega_b\subseteq\Omega_dΞ©bβ€‹βŠ†Ξ©d​ and Ο•x1∈Ωb\phi^1_x\in\Omega_bΟ•x1β€‹βˆˆΞ©b​ we can construct partial function Ο†x2:[ ⁣[d] ⁣]Γ—U2⇀V∈Ωd\varphi_x^2:[\![d]\!]\times U_2\rightharpoonup V \in\Omega_dΟ†x2​:[[d]]Γ—U2​⇀V∈Ωd​ so that for all x∈[ ⁣[c] ⁣]x\in[\![c]\!]x∈[[c]]​ and some f∈Ωcf\in\Omega_cf∈Ωc​ we have Ο†x2(f(x),⋯ )=Ο†x1(f(x),⋯ )\varphi_x^2(f(x),\cdots)=\varphi_x^1(f(x),\cdots)Ο†x2​(f(x),β‹―)=Ο†x1​(f(x),β‹―)​.

Finally, we can construct Ο•2:[ ⁣[cβ†’d] ⁣]Γ—U3β†’V\phi_2:[\![c\to d]\!]\times U_3\to VΟ•2​:[[cβ†’d]]Γ—U3​→V​ such that Ο•2=Ο†x2=Ο†x1=Ο•1\phi_2=\varphi_x^2=\varphi_x^1=\phi_1Ο•2​=Ο†x2​=Ο†x1​=Ο•1​ for all x∈[ ⁣[c] ⁣]x\in[\![c]\!]x∈[[c]]. As Ο•2∈Ωcβ†’d\phi_2\in\Omega_{c\to d}Ο•2β€‹βˆˆΞ©cβ†’d​​, we have Ξ©aβ†’bβŠ†Ξ©cβ†’d\Omega_{a\to b}\subseteq\Omega_{c\to d}Ξ©aβ†’bβ€‹βŠ†Ξ©cβ†’d​​ concluding this proof. β–‘\Box░​

We will not develop these theorems further.

3. Subtyping as a SAT problem

4. ​Implementation

5. Further work and limitations

do not satisfy completeness