> For the complete documentation index, see [llms.txt](https://theonekevin.gitbook.io/notes/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://theonekevin.gitbook.io/notes/typed-lua.md).

# 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](https://www.typescriptlang.org/play?ts=4.8.0-beta#code/C4TwDgpgBAKlC8UDeUAeAuKA7ArgWwCMIAnKAXygB9k1MBnYYgSywHNyBuAWAChRIoAVQQ0M2fEVLUGzNp168ANhGBQAhpmGIUYgIwAGeT2WqCmONtpQDRk1ADG5kWu48gA) (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]!]$$​

<details>

<summary>Proof</summary>

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.​

</details>

**Theorem 2:** $$\Omega\_{a;|;b}=\Omega\_a\cap\Omega\_b$$ and ​$$\Omega\_{a\cdot b}=\Omega\_a\cup\Omega\_b$$​

<details>

<summary>Proof</summary>

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.​

</details>

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

<details>

<summary>Proof</summary>

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

</details>

**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.

<details>

<summary>Proof</summary>

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

</details>

We will not develop these theorems further.

### 3. Subtyping as a SAT problem

### 4. ​Implementation

### 5. Further work and limitations