diff --git a/presentation/figs/midas_df_types.txt b/presentation/figs/midas_df_types.txt new file mode 100644 index 0000000..587310a --- /dev/null +++ b/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 diff --git a/presentation/figs/python_output.txt b/presentation/figs/python_output.txt new file mode 100644 index 0000000..3efedd8 --- /dev/null +++ b/presentation/figs/python_output.txt @@ -0,0 +1,5 @@ +Traceback (most recent call last): + File "script.py", line 31, in  + 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' diff --git a/presentation/figs/python_output2.txt b/presentation/figs/python_output2.txt new file mode 100644 index 0000000..f14dc18 --- /dev/null +++ b/presentation/figs/python_output2.txt @@ -0,0 +1,5 @@ +Traceback (most recent call last): + File "script.py", line 32, in  + 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' diff --git a/presentation/presentation.typ b/presentation/presentation.typ index ba7a851..f6b10a9 100644 --- a/presentation/presentation.typ +++ b/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( diff --git a/presentation/sections/03_midas.typ b/presentation/sections/03_midas.typ index 98b1ced..23bae00 100644 --- a/presentation/sections/03_midas.typ +++ b/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 \ No newline at end of file +#{ + 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" + $ +] \ No newline at end of file