TB-Docs/report/chapters/03_theory.typ

#import "../requirements.typ": isc-hei-bthesis
#import isc-hei-bthesis: todo
#import "@preview/gentle-clues:1.3.1" as gc
#import "@preview/acrostiche:0.7.0": acr
#import "@preview/curryst:0.6.0": prooftree, rule
#import "03_theory/python_syntax.typ": python-syntax
#import "03_theory/midas_syntax.typ": midas-syntax
#import "03_theory/typing.typ"

= Underlying Theory and Typing Rules <chap:theory>

#gc.info[
  This chapter presents some type theory notions that form the basis of a type checker and establishes some typing rules we would wish to implement for Python. The reader may skip this more theoretical chapter to the implementation in @chap:impl. These notions are only explained to justify some implementation decisions and provide a solid basis on which to build the type checker but are not strictly necessary to understand the concrete development.
]

The first step to build a useful type checker for Python is to identify the concrete requirements. By identifying what kind of expressions and relationships we are dealing with, we can then select the rules we need to define and handle, and implement appropriate solutions. The concepts and ideas covered in this chapter are mainly derived from the wonderful #acr("TaPL") by Benjamin C. Pierce. This books serves as a reference for all type theory notions presented in this report. This report does not intend to become the new #acr("TaPL").

== Principles <sec:theory-principles>

To talk about type theory and typing rules, we must first define some concepts. B. C. Pierce suggests one definition for type systems:

#quote(block: true)[
  A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.@tapl
]

At its core, a type system provides techniques to ensure the absence of unwanted behavior due to incompatibilities between value types. Although often associated with computer science and programming languages, the fundamental concept of a type system is a mathematical construct.
In the following sections, we will define both syntax rules, to lay out legal constructs in the languages, and typing rules, to build relationships and theorems in our type system.

Syntactically, we will use different kinds of elements, as described in @tab:calculus-elmts.

#figure(
  table(
    columns: 3,
    table.header[*Element*][*Meta-variable*][*Description*],
    [Terms], $"t"$, [Building blocks of the language, expressions which can be evaluated],
    [Values], $"v"$, [Subset of terms, possible final results of evaluation],
    [Statements], $"s"$, [Language constructs that do not evaluate to a value and may have side-effects],
    [Types], $"T"$, [Category of values of the same kind],
  ),
  caption: [Calculus elements]
) <tab:calculus-elmts>

A term $"t"$ is said to be of type $"T"$, written $"t": "T"$ if it can be statically proven that it evaluates to a value belonging to type $"T"$.

Additionally, we will need to define rules that link different types together in a compatibility relationship. For example, we can say that a car is a kind of vehicle. In this case, the type `Car` is said to be a "subtype" of `Vehicle`. This relationship is asymmetric and transitive, and is written $"S" <: "T"$ (read "S is a subtype of T").

Finally, because we are dealing with a complex programming language such as Python, we need to introduce the concept of a context. In Python, as in most other languages, users can define variables and functions taking named parameters. This fact means that evaluating an expression, or even typing it, requires knowing some things about the context of what comes before. Taking the example of @fig:example-context, we can see that evaluating or typing the expression `a + a` on line 2 requires knowing the type (or value) of `a`, which was set in a different statement on line 1.

#figure(
  ```python
  a: float = 3
  b = a + a
  ```,
  caption: [Example Python expression requiring context]
) <fig:example-context>

The notations for context are as follows:
#align(center, grid(
  columns: 2,
  gutter: 1em,
  align: (center, left),
  $Gamma$,
  [the context, a list of bindings, mapping terms to types],
  $Gamma, "t": "T"$,
  [the context extended with the binding of $"t"$ to the type $"T"$],
))

Finally, the rules expressed in @sec:theory-syntax are written in the form of theorems using the following mathematical syntaxes:

#align(center, grid(
  columns: 2,
  gutter: 1em,
  align: (center, left),
  prooftree(rule($P_1$, $...$, $P_n$, $C$)),
  [Given premises $P_1, ..., P_n$, conclusion $C$ is true],
  $Gamma tack P$,
  [$Gamma$ "judges" that $P$ is true, i.e. $P$ is true given context $Gamma$],
  $P tack.l Gamma'$,
  [Evaluating $P$ produces the new context $Gamma'$]
))

== Syntax rules <sec:theory-syntax>

In this section, we define syntax rules for both Python and our type definition language Midas. Obviously, Python already has syntax rules defining what is or is not valid code. What is defined in @sec:theory-syntax-python are a subset of constructs which our type checker will be able to process.

=== Python syntax <sec:theory-syntax-python>

@tab:python-syntax-rules lists mosts Python constructs we want to support with our type checker (notable exceptions are listed below). This subset of the Python language is sufficient to express a wide range of programs, including data processing pipelines and moderately complex scripts.

#figure(
  python-syntax,
  caption: [Python syntax rules],
  supplement: [Table],
  kind: table,
) <tab:python-syntax-rules>

Some syntaxes are simplified or omitted from @tab:python-syntax-rules for the sake of conciseness, readability and scope. Indeed, this work's primary focus is not on the theoretical and formal approach to type checking but rather on the concrete application of it to produce a useful tool for developers. For example, function signature in Python are rather complex and flexible, allowing positional-only, keyword-only and mixed parameters, argument sinks, and default values. Expressing this level of flexibility in a formal definition as those presented above is tricky and not necessarily pertinent to this work.

Other syntaxes not referenced in this report are voluntarily left out because they either fall out of the scope of this work or are either not fundamental to the language or not necessary to most developers. Such constructs include classes, match statements, while loops, `for`/`else` blocks and the walrus operator~(`:=`).

=== Midas syntax <sec:theory-syntax-midas>

Our type system includes a dedicated language to define custom types that can be used in Python code. This language is hereafter referred to as the Midas language, or simply Midas. Its goal is to allow users to concisely define types, aliases, subtypes and the like in a simple and intuitive language. All syntax rules are listed in @tab:midas-syntax-rules.

#figure(
  midas-syntax,
  caption: [Midas syntax rules],
  supplement: [Table],
  kind: table,
) <tab:midas-syntax-rules>

Parameter specifications in function types and predicates are simplified here for conciseness. In actuality, the supported syntax is similar to Python's regarding positional-only, keyword-only and mixed arguments, with the following notable differences:
- the name of positional-only parameters is optional, i.e. `fn(float, /) -> bool` is valid

- default values are not supported but optional parameters may be indicated with a question mark (`?`) after the type, e.g. `fn(a: float?) -> bool`

A more detailed definition of the syntax is available in @app:midas-syntax.

Some elements are worth explaining here. Midas offers four base statements through four keywords: `alias`, `type`, `extend` and `predicate`.\
The first is rather straightforward: ```midas alias X = T``` defines an alias named `X` for the type `T`.\
The second is a simple subtype definition. ```midas type X = T``` is similar to an alias, but it creates a subtype relationship instead of an equivalence. `X` is thus a subtype of `T`. This also allows defining generic types using type parameters, bounded or not, which can be referenced in the right-hand side of the definition. For example ```midas type Foo[T <: U] = list[T]``` defines a type generic `Foo` with one parameter `T` subtype of `U`, which is a subtype of `list[T]`.\
The third, `extend`, is linked to a subtype definition. It allows users to define members on a type, such as properties/attributes (`prop`) and methods (`def`). Methods may be overloaded to combine multiple signatures under the same name. The type specific after `extend` must obviously be defined.\
The last kind of statement provides user with a way to define named constraint expressions and reuse them as functions in other constraint expressions. Predicates are defined like functions, with a list of parameters. This list may be split into multiple parameter specifications, for example ```midas predicate foo(a: float)(b: int) = a < b``` to allow partial application.

A particularity of Midas are its constraint types. A constraint type `T where e` is built from a base type `T` and a constraint expression `e`. It allows binding a constraint on the values belonging to this type, which will be materialized by assertions at runtime.

== Typing rules <sec:theory-typing>

Now that we have defined what Python syntax we will support and our own definition language, we need to define how our type checker will be able to bind types to Python expressions. This section is heavily inspired by the _Pure simply typed lambda-calculus~($lambda_->$)_, _Simply typed lambda-calculus with subtyping~($lambda_(<:)$)_, _Polymorphic lambda-calculus (System F)_ and _Bounded quantification (kernel $F_(<:)$)_ presented in Chapters 9, 15, 23 and 26 of #acr("TaPL")@tapl.

=== Literals

First and foremost, we can define elementary typing rules for all literal values. These rules having no premises, they are simple axioms. @tab:typing-literals lists all literal typing rules.

#figure(
  typing.literals,
  caption: [Typing rules: literals],
  kind: table,
  supplement: [Table],
) <tab:typing-literals>

Other constructs, although not constants, directly map to builtin types. These include literal lists, tuples and dictionaries. Each of these has a corresponding `list[T]`, `tuple` and `dict[K, V]` type. We will not define formal rules in this section regarding these elements, but a more in depth explanation will be given in the implementation of the type checker, in @sec:impl-python. #todo[replace ref]

=== Expressions

Apart from literals, developers also need some building blocks to express their programs. These expressions include variables, function calls, operations, etc. and need their own typing rules. The rules listed in @tab:typing-expressions cover most expressions we will handle, as defined in @sec:theory-syntax-python. Some syntaxes are omitted to keep this chapter short and because they don't necessarily bring new theoretical concepts.

#figure(
  typing.expressions,
  caption: [Typing rules: expressions],
  kind: table,
  supplement: [Table],
) <tab:typing-expressions>

#smallcaps[T-Var] simply states that a variable can be typed iff it is in the context.

#smallcaps[T-Call] is a simplified rule of the concrete behavior. Taking into account all call forms with positional and keyword arguments is a rather tedious process which is left as an exercise to the reader.

#smallcaps[T-Tern] is worth a few more words too. Typing rules used by Midas are, by design, stricter than what Python allows. In this case, because we have chosen not to include union types, an expression can only have at most one type, thus the branches must belong to a common type. The specific types of each branch may differ thanks to #smallcaps[T-Sub], defined in @tab:typing-subtyping-base. Additionally, the test expression must be of type $"bool"$, whereas Python can evaluate any object to a boolean.

#smallcaps[T-Op] is used for all binary operations. In Python, these are implemented in _dunder-methods_, such as `__add__` for the `+` operator. A similar rule could be defined for unary operations but is omitted here for brevity.

=== Statements

Finally, expressions can be used in statements, which are special constructs that can have side-effects. We listed in @sec:theory-syntax-python the particular statements that Midas should support, and @tab:typing-statements provides rules to type check their components and effects.

#figure(
  typing.statements,
  caption: [Typing rules: statements],
  kind: table,
  supplement: [Table],
) <tab:typing-statements>

#smallcaps[T-Annot] is a rule which handles Python type annotations. It states that the type checker must take note of type hints in the context.

#smallcaps[T-Seq] allows sequences of statements.

#smallcaps[T-IfElse], like #smallcaps[T-Tern] is a stricter version of how Python processes `if` statements. Indeed, Midas will not allow leaking context from inside the bodies of any branch. If a variable is declared inside an `if` statement, Midas will not allow references outside of it.

#gc.info[
  You may be familiar with the walrus operator `:=` which is often used in `if` statements to simultaneously declare a variable and use it as an expression. It it thus a mix between a simple expression, which may be used everywhere, and a statement, with the side-effect of declaring a variable.
]

#smallcaps[T-Def] is a gross simplification of how functions can be defined. It does not cover multiple parameters, positional-only and keyword-only parameters, complex bodies with multiple and implicit returns, etc. Again, for the sake of simplicity and readability, we will not define a complete rule to handle all forms and features, but the implementation will go into more details in @sec:impl-python. #todo[replace ref]

=== Subtyping

Similarly to some calculi described in #acr("TaPL")@tapl and to allow flexibility, we must equip our type system with a subtyping relationship. This relationship allows using some types in place of others where it is sound to do so. The subtyping rules presented in @tab:typing-subtyping-base cover the base cases of subtyping.

#figure(
  typing.subtyping,
  caption: [Typing rules: subtyping base],
  kind: table,
  supplement: [Table],
) <tab:typing-subtyping-base>

The subtyping relationship is by definition both reflective (#smallcaps[S-Refl]) and transitive (#smallcaps[S-Trans]).

#smallcaps[T-Sub] is a consequence of the #acr("LSP"). A term $"t"$ of type $"S"$ can be used anywhere a term of type $"T"$ is expected if $"S"$ is a subtype of $"T"$.

In addition to these base rules, we need to define how functions, constraint types and generic types are handled.
For constraint types, we will take the simple approach of considering only the base type for the subtype relationship. A more complete and interesting implementation could implement subtyping of constraint expression, where a condition such as `_ < 10` is a subtype of `_ < 100`, but the added complexity was deemed out of scope for this particular project. We do nonetheless define #smallcaps[S-Constr] in @tab:typing-subtyping-constraint to handle the base case.

#figure(
  typing.subtyping-constraint,
  caption: [Typing rules: subtyping constraint type],
  kind: table,
  supplement: [Table],
) <tab:typing-subtyping-constraint>

Generics are handled using similar rules to the _Bounded quantification (kernel $F_(<:)$)_ calculus presented in #acr("TaPL") Chapter 26@tapl. Additionally, Midas supports implicit variance, which is inferred from the locations in which type parameters are used, and is used when checking subtypes of applied generic types. A detailed explanation of variance inference is provided in the corresponding implementation section, @sec:impl-python #todo[replace ref].

Finally, functions in Python are complex types. The general subtyping rule is given in @tab:typing-subtyping-function, but the complete set of rules for checking parameter specifications is too complex to include here. It is however detailed in @app:function-subtyping.

#figure(
  typing.subtyping-function,
  caption: [Typing rules: subtyping functions],
  kind: table,
  supplement: [Table],
) <tab:typing-subtyping-function>

=== Special types

Two special types can be added to our type system for practical purposes. The first is a regular top type, as represented by `Any` in Python. Every type is a subtype of `Any`, as stated by #smallcaps[S-Any] in @tab:typing-subtyping-top.

In addition to `Any`, we will add a second top type to represent unknowns. When a user omits an annotation, the type checker can use this type as a placeholder to track that a particular expression was indeed processed but its type could not be determined. This has many practical benefits, among which avoiding early exits and propagating unknowns. Additionally, this allows the type checker to differentiate a variable which has specifically been typed as `Any`, and can contain _any_ kind of value, from a variable whose type the checker does not know.

#figure(
  typing.subtyping-top,
  caption: [Typing rules: subtyping top types],
  kind: table,
  supplement: [Table],
) <tab:typing-subtyping-top>

The special type `None`, also later referred to as `UnitType`, is used in Midas as a unit type, mapping Python functions' behavior regarding implicit returns.

/*
- Identify requirements
- Introduction to TAPL
- Grammar and typing rules for Midas, paralleled with TAPL
- Omitted rules, simplifications, mechanisms not implemented
*/