feat(report): write results chapter

report/acronyms.typ

@@ -6,6 +6,10 @@
   "AST": ([Abstract Syntax Tree],),
   "LUB": ([Least Upper Bound],),
   "CLI": ([Command-Line Interface],),
+  "CSV": ([Comma-Separated Values],),
 )
 
-#init-acronyms(acronyms)
+#init-acronyms(acronyms)
+
+// Don't think this needs a long form on first use
+#mark-acr-used("CSV")

report/appendices/example_pipeline.typ

@@ -0,0 +1,23 @@
+#show raw: set text(size: .8em)
+
+#let midas = raw(
+  block: true,
+  lang: "midas",
+  read("../code/example_pipeline/custom_types.midas")
+)
+
+#let python = raw(
+  block: true,
+  lang: "python",
+  read("../code/example_pipeline/pipeline.py")
+)
+
+#figure(
+  midas,
+  caption: [Example Pipeline: custom type definitions]
+) <fig:example-pipeline-types>
+
+#figure(
+  python,
+  caption: [Example Pipeline: Python source code]
+) <fig:example-pipeline-code>

report/bachelor_thesis.typ

@@ -191,6 +191,10 @@ You can also change the order or the names of the sections, for instance, if you
 
 #include-offset("appendices/python_parsing.typ")
 
+= Example Pipeline <app:example-pipeline>
+
+#include-offset("appendices/example_pipeline.typ")
+
 #pdf.attach(
   "../manual.pdf",
   relationship: "supplement",

report/chapters/05_results_discussion.typ

@@ -1,4 +1,173 @@
 #import "../requirements.typ": isc-hei-bthesis
 #import isc-hei-bthesis: todo
+#import "../utils.typ": code-ref
+#import "../appendices/example_pipeline.typ"
+#import "@preview/codly:1.3.0": codly
+#import "@preview/acrostiche:0.7.0": acr
 
 = Results and Discussion <chap:results>
+
+In @chap:theory and @chap:impl, we have theorized and implemented a complete type system, along with a type checker and code generator. Many features have been integrated, including but not limited to:
+- generic types
+- structural subtyping for functions
+- static evaluation of `cast` expressions on literal values
+- runtime assertion generation for `cast` expressions
+- dataframe schema definition and manipulation
+- arithmetic and aggregation methods on dataframes and columns
+
+This is more than enough to make Midas usable in a wide range of contexts, including data science. The following sections demonstrate how Midas can be used to provide powerful type checking, both statically and at runtime.
+
+== Weather pipeline example
+
+As an example, we will consider a sample weather-data transformation pipeline as shown in @app:example-pipeline, also available in the repository in #code-ref(<example-pipeline>, "examples/02_demonstration/weather/").
+
+=== Domain specific types
+
+Using the Midas language, we are able to define domain-specific types, as demonstrated in @fig:pipeline-base-types.
+
+#codly(
+  range: (1, 15),
+  smart-skip: true
+)
+#figure(
+  example_pipeline.midas,
+  caption: [Example Pipeline: domain specific types]
+) <fig:pipeline-base-types>
+
+Additionally, we can define operations to preserve some of these semantics, as shown in @fig:pipeline-operations.
+
+#codly(
+  range: (17, 29),
+  smart-skip: true
+)
+#figure(
+  example_pipeline.midas,
+  caption: [Example Pipeline: operation definitions]
+) <fig:pipeline-operations>
+
+Finally, we can concisely define frame schemas that will become useful when manipulating dataframes in Python, as shown in @fig:pipeline-schemas.
+
+#codly(
+  range: (31, 62),
+  smart-skip: true
+)
+#figure(
+  example_pipeline.midas,
+  caption: [Example Pipeline: dataframe schemas]
+) <fig:pipeline-schemas>
+
+=== Type checking in action
+
+Now what is the time for Midas to shine. The first step in a transformation pipeline is load some data. We will used `pandas` to read a dataframe from a #acr("CSV") file. Now, the compiler or type checker has no idea what this #acr("CSV") file might look like. Even if we specify a schema, there is no guarantee that the runtime file will conform to it. At most, the type checker can say that the result of `read_csv` is a dataframe. We thus introduce a `cast` expression to actually tell the type checker what the dataframe contains. Furthermore, a runtime assertion will check that the value returned by `read_csv` does indeed match our expectations.
+
+Our load function thus looks like @fig:pipeline-load.
+
+#codly(
+  range: (10, 12),
+  smart-skip: true
+)
+#figure(
+  example_pipeline.python,
+  caption: [Example Pipeline: data loading and casting]
+) <fig:pipeline-load>
+
+In a second step, we might want to transform some values to more appropriate types, such as parsing timestamps from strings. This is also the place where we cast the dataframe to a schema with our domain-specific types, which will ensure that values conform to the defined constraints, as shown in @fig:pipeline-convert.
+
+#codly(
+  range: (15, 24),
+  smart-skip: true
+)
+#figure(
+  example_pipeline.python,
+  caption: [Example Pipeline: converting columns and enforcing constraints]
+) <fig:pipeline-convert>
+
+This does highlight two current weaknesses of Midas. The first is the need to copy the dataframe in @fig:pipeline-convert:16. This is due to the fact that Midas does not support reference types (see chapter 13 of #acr("TaPL")@tapl). This means the type checker is completely oblivious to the fact that modifying a dataframe somewhere might change other references in other places.
+The second issue, which is more of a possible optimization, is the fact that `cast` will re-check the whole dataframe at runtime, even though some checks are irrelevant given the parameter's type. This is made even more noticeable in @fig:pipeline-aggregation which will check base types again (e.g. `float`).
+
+#codly(
+  range: (27, 38),
+  smart-skip: true
+)
+#figure(
+  example_pipeline.python,
+  caption: [Example Pipeline: arithmetic operations on columns]
+) <fig:pipeline-heat-index>
+
+As implemented in @sec:python-df-methods, Midas will type check many operations on dataframes and columns, including `groupby` and aggregation methods. The result the computation shown in @fig:pipeline-aggregation is already typed as a dataframe of `float` columns by the type checker. We only add a `cast` to bring back our domain specific types, while re-checking value constraints. This latter point reveals one great feature missing from Midas: constraint unification (this will be discussed in @chap:conclusion).
+
+#codly(
+  range: (41, 54),
+  smart-skip: true
+)
+#figure(
+  example_pipeline.python,
+  caption: [Example Pipeline: data aggregation]
+) <fig:pipeline-aggregation>
+
+Finally, there are some cases where Midas is not capable of properly type-checking some expressions, either by choice of the user or because some syntax is not yet supported. In either case, the type checker will gracefully handle untyped values by propagating them as `UnknownType`. Not only is `UnknownType` a top-type, it will also accept any operation, attribute or subscript access, etc.
+
+Moreover, users may want to cast an expression to a type but cannot afford the cost of checking it at runtime or feel it is too redundant with a previous known typing judgment. Alternatively, they may want to use a value with an unknown type which _behaves_ as another for all practical purposes (e.g. `np.float32`). In that case, they can use an escape hatch with `unsafe_cast` which blindly accepts that the given expression is of the specified type, as used in @fig:pipeline-plot.
+
+#codly(
+  range: (57, 65),
+  smart-skip: true
+)
+#figure(
+  example_pipeline.python,
+  caption: [Example Pipeline: unknown types and `unsafe_cast`]
+) <fig:pipeline-plot>
+
+== Type errors
+
+In the previous section, we focused on dataframe operations, casts and runtime type errors, but Midas also catches static type errors. One classical but sneaky kind of error is mixing incompatible units. While using millimeters instead of centimeters when 3D-printing a pen holder might be comical, mixing monetary currencies while handling enterprise assets will probably get you fired. As demonstrated in @fig:caught-errors, Midas can help you avoid this kind of errors that can happen when some values share the same base representation (`float`).
+
+#let highlights = (
+  (
+    line: 3,
+    start: 6,
+    end: 12,
+    fill: green,
+    tag: [_Price[EUR]_],
+  ),
+  (
+    line: 4,
+    start: 6,
+    end: 12,
+    fill: red,
+    tag: [Wrong type for argument '0', expected Price[EUR], got Price[USD]],
+  ),
+  (
+    line: 5,
+    start: 1,
+    end: 7,
+    fill: red,
+    tag: [Cannot assign Price[USD] to variable 'a3' of type Price[EUR]],
+  ),
+)
+
+#figure(
+  [
+    *Types*
+    ```midas
+    type Currency = float
+    type Price[T <: Currency] = T where _ >= 0
+    type EUR = Currency
+    type USD = Currency
+    extend Price[T <: Currency] {
+        def __add__: fn(Price[T], /) -> Price[T]
+    }
+    ```
+
+    *Code*
+    #codly(highlights: highlights)
+    ```python
+    p1 = cast(Price[EUR], 3.2)
+    p2 = cast(Price[USD], 10.4)
+    p3 = p1 + p1
+    p4 = p1 + p2
+    p3 = p2
+    ```
+  ],
+  caption: [Example type errors caught by Midas]
+) <fig:caught-errors>

report/code/example_pipeline/custom_types.midas

@@ -0,0 +1,62 @@
+predicate in_range(min: float, max: float)(v: float) = min <= v & v <= max
+predicate is_percentage = in_range(0.0, 100.0)
+
+type Celsius = float
+type Kelvin = float where _ >= 0
+type Hectopascal = float
+
+type Temperature = Celsius where in_range(-30.0, 100.0)(_)
+type Pressure = Hectopascal where in_range(800.0, 1100.0)(_)
+type Humidity = float where is_percentage(_)
+type HeatIndex = float
+
+type StationID = str where len(_) == 3 & _.isupper()
+
+type Mean[T <: float] = float
+
+extend Celsius {
+    def __add__: fn(Celsius, /) -> Celsius
+    def __sub__: fn(Celsius, /) -> Celsius
+}
+
+extend Kelvin {
+    def __add__: fn(Kelvin, /) -> Kelvin
+}
+
+extend Hectopascal {
+    def __add__: fn(Hectopascal, /) -> Hectopascal
+    def __sub__: fn(Hectopascal, /) -> Hectopascal
+}
+
+alias RawData = Frame[
+    station_id: str,
+    timestamp: str,
+    temperature: float,
+    pressure: float,
+    humidity: float,
+]
+
+alias Data = Frame[
+    station_id: StationID,
+    timestamp: Any,
+    temperature: Temperature,
+    pressure: Pressure,
+    humidity: Humidity,
+]
+
+alias DataWithHI = Frame[
+    station_id: StationID,
+    timestamp: Any,
+    temperature: Temperature,
+    pressure: Pressure,
+    humidity: Humidity,
+    heat_index: HeatIndex,
+]
+
+alias DailyAverages = Frame[
+    timestamp: Any,
+    temperature: Mean[Temperature],
+    pressure: Mean[Pressure],
+    humidity: Mean[Humidity],
+    heat_index: Mean[HeatIndex],
+]

report/code/example_pipeline/pipeline.py

@@ -0,0 +1,79 @@
+from pathlib import Path
+
+import matplotlib.pyplot as plt
+import pandas as pd
+from custom_types import DailyAverages, Data, DataWithHI, HeatIndex, RawData
+
+from midas.typing import Column, cast, unsafe_cast
+
+
+def load_data(path: Path) -> RawData:
+    # Check base types and dataframe structure
+    return cast(RawData, pd.read_csv(path))
+
+
+def convert_data(raw_df: RawData) -> Data:
+    new_df = raw_df.copy()
+    new_df["timestamp"] = cast(
+        Column[object],
+        pd.to_datetime(new_df["timestamp"]),
+    )
+
+    # Check types and constraints at runtime, catches out-of-range values and
+    # invalid types / malformed data
+    return cast(Data, new_df)
+
+
+def compute_heat_index(df: Data):
+    # The computation's result can only be typed as `Column[float]`
+    # Casting is necessary to bring back semantic
+    df["heat_index"] = cast(
+        Column[HeatIndex],
+        (
+            df["temperature"] * 2.0
+            + df["humidity"] * 10.0
+            - df["temperature"] * df["humidity"] * 0.2
+        ),
+    )
+    return df
+
+
+def daily_avg(df: DataWithHI):
+    # Group-by and aggregation methods keep the structure of the dataframe but
+    # may erase the exact types
+    return cast(
+        DailyAverages,
+        df.groupby(
+            by=[
+                "station_id",
+                df["timestamp"].dt.day.rename("day"),
+            ],
+        )
+        .mean()
+        .sort_values(by="timestamp"),
+    )
+
+
+def plot(df: DailyAverages):
+    # Some operations are not implemented in Midas but the user can still use
+    # them, they will just not be fully type-checked
+    # `unsafe_cast` can also be used to avoid trivial, redundant or costly checks
+    stations = unsafe_cast(list[str], list(df.index.get_level_values(0).unique()))
+    for station in stations:
+        sub_df = unsafe_cast(DailyAverages, df.loc[station])
+        plt.plot(sub_df["timestamp"], sub_df["heat_index"])
+    plt.show()
+
+
+def main():
+    # Assigning to annotated variables help catch errors
+    raw_df: RawData = load_data(Path("data.csv"))
+    df: Data = convert_data(raw_df)
+
+    with_hi = compute_heat_index(df)
+    dailies = daily_avg(with_hi)
+    plot(dailies)
+
+
+if __name__ == "__main__":
+    main()