TB-Docs/report/chapters/05_results_discussion.typ

#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
- 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, 14),
  smart-skip: true
)
#figure(
  example_pipeline.midas,
  caption: [Example Pipeline: domain specific types]
) <fig:pipeline-base-types>

#pagebreak(weak: true)

Additionally, we can define operations to preserve some of these semantics, as shown in @fig:pipeline-operations.

#codly(
  range: (16, 28),
  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: (30, 61),
  smart-skip: true
)
#figure(
  example_pipeline.midas,
  caption: [Example Pipeline: dataframe schemas]
) <fig:pipeline-schemas>

#pagebreak(weak: true)

=== 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, 23),
  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: (26, 37),
  smart-skip: true
)
#figure(
  example_pipeline.python,
  caption: [Example Pipeline: arithmetic operations on columns]
) <fig:pipeline-heat-index>

#pagebreak(weak: true)

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: (40, 53),
  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: (56, 64),
  smart-skip: true
)
#figure(
  example_pipeline.python,
  caption: [Example Pipeline: unknown types and `unsafe_cast`]
) <fig:pipeline-plot>

#pagebreak(weak: true)

== 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>