feat(presentation): more slides on typing

presentation/figs/midas_df_types.txt

@@ -0,0 +1,13 @@
+Info in /tmp/test3.py from L1:15 to L1:17:
+    mean_height = df["height"].mean()
+                  ~~> Type: Frame[name: Column[str], height: Column[Meter], age: Column[Age]]
+
+Info in /tmp/test3.py from L1:15 to L1:27:
+    mean_height = df["height"].mean()
+                  ~~~~~~~~~~~~> Type: Column[Meter]
+
+Info in /tmp/test3.py from L1:15 to L1:34:
+    mean_height = df["height"].mean()
+                  ~~~~~~~~~~~~~~~~~~~> Type: Meter
+
+Infos: 3

presentation/figs/python_output.txt

@@ -0,0 +1,5 @@
+Traceback (most recent call last):
+  File "script.py", line 31, in <module>
+    assert isinstance(value, float), f"script.py:L2:6: CastError: Cannot cast {type(value).__name__} to float, in column 'age'"
+           ~~~~~~~~~~^^^^^^^^^^^^^^
+AssertionError: script.py:L2:6: CastError: Cannot cast int to float, in column 'age'

presentation/figs/python_output2.txt

@@ -0,0 +1,5 @@
+Traceback (most recent call last):
+  File "script.py", line 32, in <module>
+    assert __midas_p0__(value), "script.py:L2:6: ConstraintError: Value does not fit constraint 'in_range(0.0, 150.0)(_)', in column 'age'"
+           ~~~~~~~~~~~~^^^^^^^
+AssertionError: script.py:L2:6: ConstraintError: Value does not fit constraint 'in_range(0.0, 150.0)(_)', in column 'age'

presentation/presentation.typ

@@ -12,7 +12,24 @@
 #show raw.where(block: true): set text(size: 0.8em)
 #show: codly-init.with()
 #codly(
-  languages: codly-languages,
+  languages: codly-languages
+    + (
+      midas: (
+        name: "Midas",
+        color: rgb("#eedd47"),
+        icon: box(
+          image(
+            "../assets/icon.svg",
+            height: 130%,
+            fit: "contain",
+          ),
+        ),
+      ),
+    ),
+)
+
+#set raw(
+  syntaxes: path("../midas.sublime-syntax")
 )
 
 #show: unistra-theme.with(

presentation/sections/03_midas.typ

@@ -4,6 +4,7 @@
 #import codly: codly, codly-enable, codly-disable, local
 #import "@preview/cetz:0.5.2" as cetz: canvas, draw, tree
 #import "@preview/cetz-plot:0.1.4": smartart
+#import "@preview/conch:0.1.0"
 
 #focus-slide(theme: "forest")[Making Python Better]
 // = Making Python Better
@@ -351,8 +352,6 @@ Steps:
 
 ---
 
-#import "@preview/conch:0.1.0"
-
 #let midas-outputs = (
   check: read("../figs/midas_output.txt"),
   types: read("../figs/midas_output2.txt"),
@@ -395,8 +394,183 @@ Steps:
   )
 ])
 
+#header-process(3)
+
+#align(
+  center + horizon,
+  grid(
+    columns: 3,
+    column-gutter: 2em,
+    row-gutter: 1em,
+    [AST], none, none,
+    text(size: 2em)[+],
+    text(size: 2em)[$stretch(->)^#{set text(size: 0.6em);```py ast.unparse(tree)```}$],
+    [Code],
+    [Typing\ Judgements],
+  )
+)
+
+// What's the point? What about constraints?
+
 == Runtime Verification
 
+#{
+  show raw: set text(size: 0.7em)
+
+  grid(
+    columns: 2,
+    column-gutter: 1em,
+    row-gutter: 1em,
+    align: horizon,
+    rotate(-90deg, reflow: true)[*Source*],
+    ```python
+    from lib import fetch_data
+    unknown = fetch_data()
+    speed = cast(Meter, unknown)
+    ```,
+    rotate(-90deg, reflow: true)[*Generated*],
+    ```python
+    from lib import fetch_data
+    unknown = fetch_data()
+    __midas_a0__ = unknown
+    assert isinstance(__midas_a0__, float), f'script.py:L3:9: CastError: Cannot cast {type(__midas_a0__).__name__} to float'
+    speed = __midas_a0__
+    del __midas_a0__
+    ```
+  )
+}
+
 == Customization
 
-== Advanced Typing
+#{
+  show raw: set text(size: 0.69em)
+  item-by-item()[
+    - Domain Specific Types (e.g. units, scores, transformed data)
+      ```midas
+      type Meter = float
+      extend Meter {
+          def __add__: fn(Meter, /) -> Meter
+          def __truediv__: fn(float, /) -> Meter
+      }
+      ```
+
+    - Dependent Types (i.e. with value constraints)
+      ```midas
+      predicate in_range(mn: float, mx: float)(v: float) = mn <= v & v <= mx
+      type Age = int where in_range(0.0, 150.0)(_)
+      ```
+  ]
+}
+
+== Advanced Typing
+
+Defining a dataframe schema
+```midas
+alias Data = Frame[
+  name: str,
+  height: Meter,
+  age: Age
+]
+```
+
+---
+
+Using a dataframe schema
+```python
+import pandas as pd
+df = cast(Data, pd.read_csv("data.csv"))
+```
+
+#pause
+
+Generates runtime checks
+
+
+#let python-outputs = (
+  data1: read("../figs/python_output.txt"),
+  data2: read("../figs/python_output2.txt"),
+)
+
+#let python-cmd(args, stdin, files, output: "") = {
+  (
+    stdout: output,
+    exit-code: 0,
+  )
+}
+
+#let make-cast-error(output) = conch.terminal-block(
+  system: conch.system(
+    plugins: (
+      ("midas", (..args) => (stdout: "", exit-code: 0)),
+      ("python", python-cmd.with(output: output)),
+    ),
+    hostname: "XANA",
+  ),
+  user: "louis",
+  show-cursor: false,
+  theme: "monokai",
+  height: 150pt,
+  width: 660pt,
+  ```
+  midas compile script.py -t types.midas
+  python build/midas/script.py
+  ```
+)
+
+#figure(
+  align(
+    left + top,
+    alternatives(
+      make-cast-error(python-outputs.data1),
+      make-cast-error(python-outputs.data2),
+    )
+  )
+)
+
+---
+
+```python
+mean_height = df["height"].mean()
+```
+
+#figure(
+  align(
+    left + top,
+    conch.terminal-block(
+      system: conch.system(
+        plugins: (
+          (
+            "midas",
+            (..args) => (
+              stdout: read("../figs/midas_df_types.txt"),
+              exit-code: 0
+            )
+          ),
+        ),
+        hostname: "XANA",
+      ),
+      user: "louis",
+      show-cursor: false,
+      theme: "monokai",
+      ```
+      midas types script.py -t types.midas
+      ```
+    )
+  )
+)
+
+---
+
+$
+  overline(x) = 1 / n sum_(i=0)^n x_i
+$
+
+#alternatives[
+  $
+    "type_of"(overline(x)) = "type_of"( ("type_of"(x) + "type_of"(x)) / "int" )
+  $
+][
+  $
+    "type_of"(overline(x)) = "type_of"( ("Meter" + "Meter") / "int") = "Meter"
+  $
+]