Typed Lua

Some random thoughts and ideas about types

1. Preface

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 $\tau$​ as $e:\tau$​. 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:\tau$ 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:\tau$​ iff $x\in[\![\tau]\!]$.

Definition 2a: The set of operations, denoted $\Omega$​, is the set where any element is of type$o\in\Omega:\prod_n[\![\tau_i]\!]\to\prod_m[\![\sigma_i]\!]$.

Definition 2b: Suppose we have $o:\prod [\![a_i]\!]\to\prod [\![b_i]\!]\in\Omega$​ and $o':\prod [\![a_i']\!]\to\prod [\![b_i']\!]\in\Omega$. Then $o=o'$ iff $o\;v=o'\;v$​ for all $v:\prod a_i\in\prod[\![a_i]\!]$​. We will not develop this further.

Definition 3: Denote the set of operators that accept a parameter typed $a$​ as $\Omega_a$​. Then we define $a\le b$​ as $\Omega_a\subseteq\Omega_b$.​

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

Definition 4: Type union is notated $a+b$​ or $a\;|\;b$ where $x:a+b \iff (x:a)\lor (x:b)$

Definition 5: Type intersection is notated $a\cdot b$​ where $x:a\cdot b\iff (x:a)\land(x:b)$​

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

1. $a\le a$​
2. $a\le b$​ and $b\le c$​ implies $a\le c$​

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

Lemma 1: $[\![a\;|\;b]\!] = [\![a]\!]\cup [\![b]\!]$ and $[\![a\cdot b]\!] = [\![a]\!]\cap [\![b]\!]$​

Proof

First:

Let any $x:a\;|\;b \in[\![a\;|\;b]\!]$ then if $x:a$​ we have $x\in[\![a]\!]$​ and if $x:b$​ we have $x\in[\![b]\!]$hence $x\in[\![a]\!]\cup[\![b]\!]$. Now the converse. Let any $x:a\in [\![a]\!]$ then trivially $x:a\;|\;b$ is true so $x\in[\![a\;|\;b]\!]$. Similarly, $x\in[\![b]\!]\implies x\in[\![a\;|\;b]\!]$​ and so we're done. $\Box$

Second: Proceed similarly to above.​

Theorem 2: $\Omega_{a\;|\;b}=\Omega_a\cap\Omega_b$ and ​$\Omega_{a\cdot b}=\Omega_a\cup\Omega_b$​

Proof

First:

Let any $\phi\in\Omega_{a\;|\;b}$​ and WLOG let $\phi:[\![a\;|\;b]\!]\times U\to V$ and construct $\phi_1:[\![a]\!]\times U\to V$​ as $\phi_1: x\times y\mapsto \phi(x\times y)$​ where $x\in[\![a]\!]$ so by Definition 2 we have $\Omega_a\subseteq\Omega_{a\;|\;b}$​. Similarly, we have $\Omega_b\subseteq\Omega_{a\;|\;b}$​. Conversely, let any $\phi_1\in\Omega_a$ and $\phi_2\in\Omega_b$ and WLOG suppose $\phi_1:[\![a]\!]\times U_1\to V_1$ and $\phi_2:[\![b]\!]\times U_2\to V_2$ then we can construct a partial map $\phi:([\![a]\!]\cup [\![b]\!])\times (U_1\cup U_2)\rightharpoonup (V_1\cup V_2)$ where

$\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}$​

and $\phi\in \Omega_{a\;|\;b}$​ as $[\![a]\!]\cup [\![b]\!] = [\![a\;|\;b]\!]$​ by Lemma 1, concluding this proof. $\Box$

Second: Proceed similarly to above.​

Corollary 1: If $a\le c$​ and $b\le d$​ then $a+b\le c+d$

Proof

By Definition 2, $\Omega_a\subseteq\Omega_c$​ and $\Omega_b\subseteq\Omega_d$​.

By Theorem 2, $\Omega_{a+b} = \Omega_a\cap\Omega_b\subseteq\Omega_c\cap\Omega_d=\Omega_{c+d}$​, concluding this proof. $\Box$​

Theorem 3: If $c\le a$​ and $b\le d$​ then $a\to b\le c\to d$​.

​Remark: This is an important result and shows that function parameters are contravariant while function return types are covariant.

Proof

Let any $\phi_1\in\Omega_{a\to b}$ where WLOG $\phi_1:[\![a\to b]\!]\times U_1\to V = \phi_1:\Omega_a\times U_1\to V$.

Construct​ function $\varphi_x^1: [\![b]\!]\times U_2\to V$ so for all $x\in[\![c]\!]$ and some $f\in\Omega_c\subseteq\Omega_a$ we have $\varphi^1_x(f(x),\cdots)=\phi_1(f, \cdots)$.

Since $\Omega_b\subseteq\Omega_d$ and $\phi^1_x\in\Omega_b$ we can construct partial function $\varphi_x^2:[\![d]\!]\times U_2\rightharpoonup V \in\Omega_d$ so that for all $x\in[\![c]\!]$​ and some $f\in\Omega_c$ we have $\varphi_x^2(f(x),\cdots)=\varphi_x^1(f(x),\cdots)$​.

Finally, we can construct $\phi_2:[\![c\to d]\!]\times U_3\to V$​ such that $\phi_2=\varphi_x^2=\varphi_x^1=\phi_1$ for all $x\in[\![c]\!]$. As $\phi_2\in\Omega_{c\to d}$​, we have $\Omega_{a\to b}\subseteq\Omega_{c\to 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