feat(report): write state of the art

report/acronyms.typ

@@ -7,6 +7,7 @@
   "LUB": ([Least Upper Bound],),
   "CLI": ([Command-Line Interface],),
   "CSV": ([Comma-Separated Values],),
+  "GLSL": ([OpenGL Shading Language],),
 )
 
 #init-acronyms(acronyms)

report/bibliography.bib

@@ -11,7 +11,7 @@
 
 @article{gator,
   author = {Geisler, Dietrich and Yoon, Irene and Kabra, Aditi and He, Horace and Sanders, Yinnon and Sampson, Adrian},
-  title = {Geometry types for graphics programming},
+  title = {Geometry Types for Graphics Programming},
   year = {2020},
   issue_date = {November 2020},
   publisher = {Association for Computing Machinery},
@@ -44,13 +44,13 @@
   pagetotal = {640},
   url       = {https://craftinginterpreters.com/},
   added-at  = {2025-04-07T18:48:41.000+0200},
-    biburl    = {https://www.bibsonomy.org/bibtex/277c8c518a2426a59a8e4c3a720e60d23/gron},
+  biburl    = {https://www.bibsonomy.org/bibtex/277c8c518a2426a59a8e4c3a720e60d23/gron},
   interhash = {98f889463df208a828c08042cd116e94},
   intrahash = {77c8c518a2426a59a8e4c3a720e60d23},
-    keywords  = {AST Book Bytecode Interpreters Visitor},
+  keywords  = {AST Book Bytecode Interpreters Visitor},
   month     = {July},
-    timestamp = {2025-04-07T18:49:46.000+0200},
-  }
+  timestamp = {2025-04-07T18:49:46.000+0200},
+}
 
 @Book{Householder1951,
   author    = {Householder, Alston S.},
@@ -99,6 +99,28 @@
   url         = {https://llis.nasa.gov/lesson/641},
 }
 
+@TechReport{PEP484,
+  author   = {Guido van Rossum and Jukka Lehtosalo and Łukasz Langa},
+  title    = {Type Hints},
+  year     = {2014},
+  date     = {2014-09-29},
+  type     = {PEP},
+  language = {en},
+  number   = {484},
+  url      = {https://peps.python.org/pep-0484/},
+}
+
+@TechReport{PEP544,
+  author   = {Ivan Levkivskyi and Jukka Lehtosalo and Łukasz Langa},
+  title    = {Protocols: Structural subtyping (static duck typing)},
+  year     = {2017},
+  date     = {2017-03-05},
+  type     = {PEP},
+  language = {en},
+  number   = {544},
+  url      = {https://peps.python.org/pep-0544/},
+}
+
 @Online{Pebble,
   author   = {Louis Heredero},
   title    = {Pebble},
@@ -115,4 +137,14 @@
   url    = {https://en.wikipedia.org/w/index.php?title=Definite_assignment_analysis&oldid=1326872870},
 }
 
+@InProceedings{ niels_bantilan-proc-scipy-2020,
+  author    = { {N}iels {B}antilan },
+  title     = { pandera: {S}tatistical {D}ata {V}alidation of {P}andas {D}ataframes },
+  booktitle = { {P}roceedings of the 19th {P}ython in {S}cience {C}onference },
+  pages     = { 116 - 124 },
+  year      = { 2020 },
+  editor    = { {M}eghann {A}garwal and {C}hris {C}alloway and {D}illon {N}iederhut and {D}avid {S}hupe },
+  doi       = { 10.25080/Majora-342d178e-010 }
+}
+
 @Comment{jabref-meta: databaseType:biblatex;}

report/chapters/01_introduction.typ

@@ -15,7 +15,7 @@ By their fundamental essence, computers and other similar machines are determini
 When programming, developers use formal languages to instruct their devices to do particular tasks. Theses languages are designed to be unambiguous and generally explicit about what they describe. To the machine interpreting that written text, only one meaning is possible. "But", you may say, "sometimes there are bugs when I run my program". Of course, bugs are an inherent part of programming, but not because the machine might not understand you, because you explained it wrongly.
 Errors and bugs are always caused by the human factor of computer science.#footnote[Notable exceptions are of course hardware failures which are a totally separate kind of issue]
 
-Over the years, we have created a terrifyingly large number of programming languages#footnote[At least 8945 in 2005 according to the Historical Encyclopaedia of Programming Languages@HOPL] and developed countless tools to help developers avoid errors. Some are more famous than others, some are short-lived, and some remained obscure research projects which never made it out to the public. 
+Over the years, we have created a terrifyingly large number of programming languages#footnote[At least 8945 in 2005 according to the Historical Encyclopaedia of Programming Languages@HOPL] and developed countless tools to help developers avoid errors. Some are more famous than others, some are short-lived, and some remained obscure research projects which never made it out to the public.
 While programming languages such as C and Java have long been some of the most popular among developers, another language seemed to have taken the lead in recent years. According to Stack Overflow's 2025 Developer Survey, Python is the most popular programming language among respondents, from beginners to professional developers.@SO2025Survey
 
 Python is a very flexible scripting language, used in many fields, from small games, one-off data processing scripts and personal tooling to desktop applications and data processing pipelines. It is simple enough for beginners to easily learn it and play with it but highly expressive and with a rich ecosystem to build complex projects and production software.
@@ -39,6 +39,6 @@ The general goal of this bachelor project is to create a type system on top of P
 
 The system should not impede on Python's dynamic typing philosophy. It should ensure soundness where types are annotated or inferred, while leaving the user free to omit some and perform unsafe operations.
 
-It system must be flexible to allow checking various kinds of constraints (e.g. value domain, geometric shape, distribution, etc.) and allow extension to add support for more Python features and packages.
+It must be flexible to allow checking various kinds of constraints (e.g. value domain, geometric shape, distribution, etc.) and allow extension to add support for more Python features and packages.
 
 Finally, the system must be simple to use for average Python developers, and be able to seamlessly integrate into existing Python code.

report/chapters/02_state_of_the_art.typ

@@ -1,8 +1,24 @@
 #import "../requirements.typ": isc-hei-bthesis
 #import isc-hei-bthesis: todo
+#import "../utils.typ": fn-link
+#import "@preview/acrostiche:0.7.0": acr
 
 = State of the Art <chap:state-of-the-art>
 
+First of all, before reinventing the wheel and creating a completely redundant tool, we must look at what already exists in Python's rich environment and beyond.
+
+The Python Language includes a dedicated syntax for what are called "type hints", as defined in PEP 484 since Python 3.5@PEP484.
+Type hints are annotations that users can add to variables and functions to specify information about the type of some values.
+
+Python also natively provides a `typing` module with several tools developers can use to better describe their code. This includes but is not limited to `Generic` and `TypeVar` for generic types, the `cast()` function, the `TypeAlias` class to explicitly mark some assignments as type aliases, and `Protocol`, a multipurpose machinery allowing the definition of interface-like classes (defined since Python 3.8 in PEP 544@PEP544). The latter can notably be used to remove some ambiguity around duck-typing and make it more explicit, by indicating that some value implements some method or has some specific attribute.\
+However, this system is difficult to scale to dataframe and more complex type operations. Additionally, Python remains a fundamentally dynamically typed language which only really cares about the values' base types and whether they possess specific attributes or methods.
+
+Of course, type checkers have long been integrated into IDEs, like MyPy and Pyright. These often provide comprehensive type checking, supporting all aforementioned features of the `typing` module and more, and often offer multiple levels of strictness. They do lack some features that could give users more freedom in defining type aliases such as a generic type that is a subtype of its own parameter (e.g. a `Price[EUR]` is an amount of `EUR`, which is itself a `float`). They do not support constraint type either and only provide static analysis, without the ability to generate runtime assertions. Type checking complex structures like `numpy` arrays or `pandas` dataframes is also complicated, if not impossible.
+
+In Python's ecosystem, there are two interesting projects which do however try to help with typing dataframes. The first, focused on statically typing schemas, is called #fn-link(<strictly-typed-pandas>, "https://strictly-typed-pandas.readthedocs.io")[_Strictly Typed Pandas_]. It allows declaring schemas as simple class definitions and even provides runtime verification using a simple `@typechecked` decorator. In spite of that, it does seem to lack proper type checking of operations on dataframes and columns.
+The other project worth mentioning is called #fn-link(<pandera>, "https://pandera.readthedocs.io")[_Pandera_]@niels_bantilan-proc-scipy-2020. This Python package provides a wide range of features to perform runtime verification of dataframe schemas and data validation, such as statistical analysis. While it does seem to be a rather useful and complete tool, it does not cover our static type checking goal and has quite a verbose syntax.
+
+Finally, this project takes some loose inspiration from another research project named #fn-link(<gator-web>, "https://capra.cs.cornell.edu/research/gator/")[_Gator_]@gator. The Gator system is a type system and language created to "prevent geometry bugs by reflecting the coordinate system for each geometric object", in #acr("GLSL").
 
 /*
 - Python type hints (https://peps.python.org/pep-0484/):
@@ -14,6 +30,7 @@
   - MyPy / Pyright
 
 - Existing libraries
+  - Strictly Typed Pandas: schema manipulation
   - Pandera: runtime only, syntax heavy, but quite complete
 
 - Similar ideas

report/chapters/04_implementation/04_midas_language.typ

@@ -38,7 +38,7 @@ Concretely, the lexer scans the source code character by character and produces
   caption: [`Token` and `Position` classes]
 ) <fig:token-class>
 
-`MidasLexer` has a simple constructor taking in a source code string and optional file path, and a concise `process` method returning a list of tokens, as shown in @fig:lexer-signatures. 
+`MidasLexer` has a simple constructor taking in a source code string and optional file path, and a concise `process` method returning a list of tokens, as shown in @fig:lexer-signatures.
 
 #figure(
   ```python
@@ -347,7 +347,7 @@ When processing a predicate definition, we first need to gather all parameters a
 
 === Example
 
-Continuing with our example from @fig:example-midas-ast, the type statement would register a new type named `Kelvin` with internal representation given in 
+Continuing with our example from @fig:example-midas-ast, the type statement would register a new type named `Kelvin` with an internal representation given in @fig:example-midas-type.
 
 #figure(
   ```python

report/chapters/04_implementation/05_python_checking.typ

@@ -563,7 +563,7 @@ In practice, we keep track of a scope dictionary containing all defined variable
 
 == Frames and Columns <sec:python-df-cols>
 
-There is still one big part of the type checker that we have not covered: dataframes and columns. Properly type checking dataframe operations is a never-ending rabbit hole. Libraries like `pandas` or `polars` provide a enormous amount of features, as methods and syntax sugars. They also have highly polymorphic functions, accepting operations with all kinds of values, such as multiplying a dataframe by a scalar, a list, a column or even another dataframe. The results of these operations may vary quite a lot depending on the operands, or sometimes on the parameters passed to some functions. As discussed in @chap:state-of-the-art, some libraries do try and make developers' lives a little better by providing some static type-checking like #fn-link(<strictly-typed-pandas>, "https://strictly-typed-pandas.readthedocs.io")[_Strictly Typed Pandas_], or runtime schema verification like #fn-link(<pandera>, "https://pandera.readthedocs.io")[_Pandera_].
+There is still one big part of the type checker that we have not covered: dataframes and columns. Properly type checking dataframe operations is a never-ending rabbit hole. Libraries like `pandas` or `polars` provide a enormous amount of features, as methods and syntax sugars. They also have highly polymorphic functions, accepting operations with all kinds of values, such as multiplying a dataframe by a scalar, a list, a column or even another dataframe. The results of these operations may vary quite a lot depending on the operands, or sometimes on the parameters passed to some functions. As discussed in @chap:state-of-the-art, some libraries do try and make developers' lives a little better by providing some static type-checking like #fn-link(<strictly-typed-pandas>, "https://strictly-typed-pandas.readthedocs.io")[_Strictly Typed Pandas_], or runtime schema verification like #fn-link(<pandera>, "https://pandera.readthedocs.io")[_Pandera_]@niels_bantilan-proc-scipy-2020.
 
 Midas stands in between by providing some static type-checking for dataframe schemas and operations as well as generating runtime checks when a value is cast to such a type.
 We will explore in this section how we can not only provide type-checking for frame columns, for either accessing or assigning to them, but also handle some method calls with best effort inference of the resulting type.