diff --git a/justfile b/justfile index 55ddc87..9cb3878 100644 --- a/justfile +++ b/justfile @@ -7,6 +7,8 @@ outdir := "out" report_out_path := outdir / "report.pdf" summary_out_path := outdir / "summary.pdf" poster_out_path := outdir / "poster.pdf" +presentation_out_path := outdir / "presentation.pdf" +presentation_pdfpc_path := outdir / "presentation.pdfpc" default: all @@ -39,4 +41,11 @@ summary: _setup poster: _setup typst c --root . poster/poster.typ {{poster_out_path}} -all: report summary poster \ No newline at end of file +presentation: _setup + typst c --root . presentation/presentation.typ {{presentation_out_path}} + typst eval --root . 'query().first().value' --in presentation/presentation.typ > {{presentation_pdfpc_path}} + +present: presentation + pympress {{presentation_out_path}} + +all: report summary poster presentation \ No newline at end of file diff --git a/presentation/figs/HES-SO_logo_CMJN.svg b/presentation/figs/HES-SO_logo_CMJN.svg new file mode 100644 index 0000000..09eee69 --- /dev/null +++ b/presentation/figs/HES-SO_logo_CMJN.svg @@ -0,0 +1,133 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/presentation/figs/hei_logo.svg b/presentation/figs/hei_logo.svg new file mode 100644 index 0000000..d94f8f6 --- /dev/null +++ b/presentation/figs/hei_logo.svg @@ -0,0 +1,99 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + \ No newline at end of file diff --git a/presentation/figs/isc_logo.svg b/presentation/figs/isc_logo.svg new file mode 100644 index 0000000..deb0239 --- /dev/null +++ b/presentation/figs/isc_logo.svg @@ -0,0 +1,988 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/presentation/figs/midas_output.txt b/presentation/figs/midas_output.txt new file mode 100644 index 0000000..3e16728 --- /dev/null +++ b/presentation/figs/midas_output.txt @@ -0,0 +1,5 @@ +Error in /tmp/script.py from L2:12 to L2:15: + fib.append(3.0) + ~~~> Wrong type for argument 'object', expected int, got float + +Errors: 1 diff --git a/presentation/figs/midas_output2.txt b/presentation/figs/midas_output2.txt new file mode 100644 index 0000000..2790607 --- /dev/null +++ b/presentation/figs/midas_output2.txt @@ -0,0 +1,33 @@ +Info in /tmp/script.py from L1:8 to L1:9: + fib = [1,1,2] + ~> Type: int + +Info in /tmp/script.py from L1:10 to L1:11: + fib = [1,1,2] + ~> Type: int + +Info in /tmp/script.py from L1:12 to L1:13: + fib = [1,1,2] + ~> Type: int + +Info in /tmp/script.py from L1:7 to L1:14: + fib = [1,1,2] + ~~~~~~~> Type: list[int] + +Info in /tmp/script.py from L2:12 to L2:15: + fib.append(3.0) + ~~~> Type: float + +Info in /tmp/script.py from L2:1 to L2:4: + fib.append(3.0) + ~~~> Type: list[int] + +Info in /tmp/script.py from L2:1 to L2:16: + fib.append(3.0) + ~~~~~~~~~~~~~~~> Type:  + +Error in /tmp/script.py from L2:12 to L2:15: + fib.append(3.0) + ~~~> Wrong type for argument 'object', expected int, got float + +Errors: 1 Infos: 7 diff --git a/presentation/figs/mypy_logo.svg b/presentation/figs/mypy_logo.svg new file mode 100644 index 0000000..4eaf65d --- /dev/null +++ b/presentation/figs/mypy_logo.svg @@ -0,0 +1,99 @@ + + + + + + + + image/svg+xml + + + + + + + + + + + + + + + diff --git a/presentation/figs/pyright-logo.png b/presentation/figs/pyright-logo.png new file mode 100644 index 0000000..5a06866 Binary files /dev/null and b/presentation/figs/pyright-logo.png differ diff --git a/presentation/figs/python-logo.svg b/presentation/figs/python-logo.svg new file mode 100644 index 0000000..eb946c7 --- /dev/null +++ b/presentation/figs/python-logo.svg @@ -0,0 +1,243 @@ + + + + + + + + image/svg+xml + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/presentation/figs/script.py b/presentation/figs/script.py new file mode 100644 index 0000000..ac2f2d9 --- /dev/null +++ b/presentation/figs/script.py @@ -0,0 +1,2 @@ +fib = [1, 1, 2] +fib.append(3.0) \ No newline at end of file diff --git a/presentation/presentation.typ b/presentation/presentation.typ new file mode 100644 index 0000000..ba7a851 --- /dev/null +++ b/presentation/presentation.typ @@ -0,0 +1,49 @@ +#import "requirements.typ": * +#import "../meta.typ" +#import codly: codly-init, codly +#import "@preview/codly-languages:0.1.10": codly-languages + +#pdfpc.config( + start-time: datetime(hour: 13, minute: 15, second: 0), + end-time: datetime(hour: 13, minute: 55, second: 0), + duration-minutes: 20, +) + +#show raw.where(block: true): set text(size: 0.8em) +#show: codly-init.with() +#codly( + languages: codly-languages, +) + +#show: unistra-theme.with( + config-info( + author: meta.authors, + institution: meta.school, + date: datetime(year: 2026, month: 8, day: 24).display("[day].[month].[year]"), + title: [Midas], + subtitle: [Hybrid Type Checking for Python], + //title: meta.title, + //subtitle: meta.subtitle, + //short-title: [Midas], + //short-subtitle: [Hybrid Type Checking for Python], + logo: image("figs/isc_logo.svg"), + ), + config-common( + enable-pdfpc: true, + ), + config-store( + font: "Source Sans Pro" + ) +) + +#title-slide( + logos: ( + box(inset: (x: 0.8em), image("figs/hei_logo.svg", height: 2cm)), + box(inset: (x: 0.8em), image("figs/isc_logo.svg", height: 2cm)), + ) +) + +#include "sections/01_introduction.typ" +#include "sections/02_state_of_the_art.typ" +#include "sections/03_midas.typ" +#include "sections/04_status_and_future.typ" diff --git a/presentation/requirements.typ b/presentation/requirements.typ new file mode 100644 index 0000000..45f8a0f --- /dev/null +++ b/presentation/requirements.typ @@ -0,0 +1,3 @@ +#import "@preview/touying:0.7.4": * +#import "@preview/touying-unistra-pristine:1.4.3": * +#import "@local/codly:1.3.1" \ No newline at end of file diff --git a/presentation/sections/01_introduction.typ b/presentation/sections/01_introduction.typ new file mode 100644 index 0000000..453194d --- /dev/null +++ b/presentation/sections/01_introduction.typ @@ -0,0 +1,85 @@ +#import "../requirements.typ": * + +#focus-slide(theme: "berry")[The Issue] +// = The issue + +== A popular language + +#align(center, image("../figs/python-logo.svg")) + +Python is a widely used language, especially in data science + +== It can bite + +Everything is fine... + +```python +transactions = load_transactions() +mean_amount = np.mean(transactions) +``` + +// Il y a comme un couac -> duck-typing + +#pause + +Until its not + +```python +def load_transactions(): + return [ + usd_transaction, + chf_transaction + ] +``` + +--- + +#{ + set text(size: 0.4em) + table( + columns: (1fr, 2fr, 0.5fr, 3.5fr), + table.header[*Height*][*Country*][*Age*][*Profession*], + // range(5 * 10).map(_ => line()) + ..range(4 * 28).map( + i => line( + start: (0%, 0%), + end: (100%, 0%), + stroke: ( + dash: ( + array: (6pt, 3pt, "dot", 3pt), + phase: calc.rem(i * 13, 31) * 1pt + ), + paint: gray + ) + ) + ) + ) + + pause + + place( + center + horizon, + dx: -2.5em, + box( + stroke: 1pt, + radius: 4pt, + width: 8em, + height: 6em, + clip: true, + fill: white, + move( + dx: -5em, + dy: -1em, + table( + columns: (6em, 6em, 6em), + rows: 1.5em, + [], [61], [], + [], [18], [], + [], [1963#place(center + horizon, ellipse(width: 2.5em, height: 2em, stroke: std.red))], [], + [], [35], [], + [], [42], [], + ) + ) + ) + ) +} \ No newline at end of file diff --git a/presentation/sections/02_state_of_the_art.typ b/presentation/sections/02_state_of_the_art.typ new file mode 100644 index 0000000..279a81e --- /dev/null +++ b/presentation/sections/02_state_of_the_art.typ @@ -0,0 +1,32 @@ +#import "../requirements.typ": * + +#focus-slide(theme: "mandarine")[What's Out There?] +// = What's out there? + +#gallery( + image("../figs/mypy_logo.svg"), + image("../figs/pyright-logo.png"), + title: [Existing Type Checkers], + columns: 2, + gutter: 3em, +) + +== Community Packages for Pandas + +=== Strictly Typing Pandas +#{ + set text(size: 0.8em) + emph(link("https://strictly-typed-pandas.readthedocs.io")) +} + +- Static typing of schema +- Quite limited + +=== Pandera +#{ + set text(size: 0.8em) + emph(link("https://pandera.readthedocs.io")) +} + +- Dynamic verification and data validation +- Powerful but verbose diff --git a/presentation/sections/03_midas.typ b/presentation/sections/03_midas.typ new file mode 100644 index 0000000..98b1ced --- /dev/null +++ b/presentation/sections/03_midas.typ @@ -0,0 +1,402 @@ +#import "../requirements.typ": * +#import "@preview/curryst:0.6.0": prooftree, rule +#import "@preview/pinit:0.2.2": pin, pinit-point-from +#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 + +#focus-slide(theme: "forest")[Making Python Better] +// = Making Python Better + +== Strict Typing Rules + +#let syntax(body) = { + set text(weight: "bold", fill: rgb(100, 50, 0)) + body +} + +#slide(repeat: 5, self => { + let (uncover, only, alternatives-match) = utils.methods(self) + let typing-rule = prooftree( + rule( + name: smallcaps[(T-Tern)], + uncover("3-", $Gamma tack "t"_1: "bool"$), + uncover("4-", $Gamma tack "t"_21: "T"$), + uncover("4-", $Gamma tack "t"_22: "T"$), + alternatives-match(( + "1": [], + "2-4": $"t"_21 #syntax[if] "t"_1 #syntax[else] "t"_22$, + "5-": $Gamma tack "t"_21 #syntax[if] "t"_1 #syntax[else] "t"_22: "T"$, + )) + ) + ) + + show raw: it => { + show regex("pin\d+"): it => pin(int(it.text.slice(3))) + it + } + + figure( + ```python + value = pin1e1pin2 if pin3conditionpin4 else pin5e2pin6 + ``` + ) + + pause + + /* + pinit-point-from( + (1, 2), + offset-dx: -20pt, + body-dx: -0.8em, + body-dy: -0.2em, + $"t"_21$ + ) + + pinit-point-from( + (5, 6), + offset-dx: 20pt, + body-dx: 0.2em, + body-dy: -0.2em, + $"t"_22$ + ) + + pinit-point-from( + (3, 4), + offset-dx: 0pt, + pin-dx: 0pt, + body-dx: -0.2em, + body-dy: 0.2em, + $"t"_1$ + ) + */ + + v(2cm) + + figure(typing-rule) +}) + +#codly( + highlights: ( + ( + line: 2, + start: 9, + tag: [#set text(size: 1.25em);```python int```], + fill: std.yellow + ), + ) +) +#figure( + ```python + value: float + value = 2026 + ``` +) + +#pause + +Liskov Substitution Principle $->$ Subsumption Rule + +#figure( + prooftree( + rule( + name: smallcaps[(T-Sub)], + $Gamma tack "t": "S"$, + $"S" <: "T"$, + $Gamma tack "t": "T"$, + ), + ) +) + +== Enforcing Rules + +/* +#set enum( + full: true, + numbering: (..n) => strong( + numbering( + if n.pos().len() == 1 { + "1." + } else { + "a." + }, + n.pos().last() + ) + ) +) +Steps: ++ Parsing ++ Type-checking ++ + Reporting + + Code generation +*/ + +#let palette1 = ( + std.purple, + std.blue, + std.orange, + std.green, +) +#let palette2 = ( + std.red, + std.orange, + std.green, + std.blue, +) +#let steps = ( + [Parsing], + [Type-checking], + [Reporting], + [Code generation], +) +#let palette = palette2.map(c => c.lighten(50%)) + +#{ + slide(repeat: 4, self => context { + let max-step-height = calc.max(..steps.map(s => measure(box(width: 5em, s)).height)) + + align(left + horizon, canvas({ + smartart.process.chevron( + steps.map(s => box(height: max-step-height, align(center + horizon, s))).slice(0, calc.min(steps.len(), self.subslide)), + step-style: palette, + steps: ( + max-width: 5em, + ), + ) + })) + }) +} + +#let header-process(n) = place( + top + right, + { + set text(size: 0.5em) + canvas({ + smartart.process.chevron( + steps, + step-style: palette.enumerate().map(((i, c)) => { + if i == n {c} + else {c.lighten(70%)} + }), + steps: (max-width: 5em), + equal-length: true + ) + }) + } +) + +#header-process(0) +#{ + show raw: set text(size: 0.7em) + grid( + columns: (11em, auto), + column-gutter: 1em, + row-gutter: 0.2em, + align: (x, y) => if y == 0 {center} else if x == 0 and y == 2 {top + right} else {left}, + grid.header[*Source*][*Raw AST*], + ```python + value = 3.0 + int("4") + ```, + grid.cell(rowspan: 2, uncover("2-", ```python + Module( + body=[ + Assign( + targets=[ + Name(id='value')], + value=BinOp( + left=Constant(value=3.0), + op=Add(), + right=Call( + func=Name(id='int'), + args=[ + Constant(value='4')], + keywords=[])))]) + ```)), + uncover("2-", canvas({ + draw.bezier-through( + (0, 0), + (1.5, -2.5), + (5, -4), + mark: (end: ">", fill: black), + name: "arrow" + ) + draw.content( + (1.5, -2.5), + ```python ast.parse(source)```, + anchor: "north-east", + padding: 3pt, + ) + })) + ) +} + +--- + + +#header-process(0) +#{ + show raw: set text(size: 0.7em) + grid( + columns: (auto, auto), + column-gutter: 1em, + row-gutter: 0.2em, + align: (x, y) => if y == 0 {center} else if x == 0 and y == 2 {top + right} else {left}, + grid.header[*Raw AST*][*Custom AST*], + ```python + Module( + body=[ + Assign( + targets=[ + Name(id='value')], + value=BinOp( + left=Constant(value=3.0), + op=Add(), + right=Call( + func=Name(id='int'), + args=[ + Constant(value='4')], + keywords=[])))]) + ```, + local( + inset: (x: 0.32em, y: 0.15em), + lang-outset: (x: 0.32em, y: 0.2em), + ```AST + AssignStmt + ├── targets + │ └── [0] VariableExpr + │ └── name: value + └── value + └── BinaryExpr + ├── left + │ └── LiteralExpr + │ └── value: 3.0 + ├── operator: Add + └── right + └── CallExpr + ├── callee + │ └── VariableExpr + │ └── name: int + ├── arguments + │ └── [0] LiteralExpr + │ └── value: '4' + └── keywords + ``` + ) + ) +} + +--- + +#header-process(1) + +#let cetz-canvas = touying-reduce.with(cetz) +#let typing-tree = cetz-canvas({ + draw.set-style(content: (padding: 0.5em)) + tree.tree( + name: "tree", + ([`type_of`(```py 3.0 + int("4")```)], + [`type_of`(```py 3.0```)], + ([`type_of`(```py int("4")```)], + [`type_of`(```py int```)], + [`type_of`(```py "4"```)], + ) + ) + ) + let type(pos, typ) = { + draw.content( + "tree.g" + pos.map(str).join("-") + ".south", + box( + inset: (x: 0.4em, y: 0.2em), + stroke: std.orange, + fill: std.orange.lighten(90%), + radius: 0.4em, + { + set text(size: 0.8em) + raw(lang: "python", typ) + } + ), + padding: 0pt, + anchor: "north" + ) + } + + (pause,) + type((0, 0), "float") + type((0, 1, 1), "str") + (pause,) + type((0, 1, 0), "(Any, /) -> int") + (pause,) + type((0, 1), "int") + (pause,) + draw.content( + ( + rel: (3, 0), + to: ( + "tree.g0.south", + 50%, + "tree.g0-1.north", + ) + ), + { + set text(size: 0.8em) + ```py float.__add__(int) -> float``` + }, + anchor: "west" + ) + (pause,) + type((0,), "float") +}) + +#align(center + horizon, typing-tree) + +--- + +#import "@preview/conch:0.1.0" + +#let midas-outputs = ( + check: read("../figs/midas_output.txt"), + types: read("../figs/midas_output2.txt"), +) + +#let midas-cmd(args, stdin, files) = { + ( + stdout: midas-outputs.at(args.first()), + exit-code: 0 + ) +} + +#let frames = conch.terminal-frames( + system: conch.system( + plugins: ( + ("midas", midas-cmd), + ), + files: ( + "script.py": read("../figs/script.py") + ), + hostname: "XANA", + ), + user: "louis", + commands: ( + "cat script.py", + "midas check script.py", + "midas types script.py", + "", + ), + mode: "key-frames", + show-cursor: false, + theme: "monokai", + height: 300pt +) + +#slide(repeat: frames.len() - 2, self => [ + #header-process(2) + #figure( + align(left + top, frames.at(self.subslide)) + ) +]) + +== Runtime Verification + +== Customization + +== Advanced Typing \ No newline at end of file diff --git a/presentation/sections/04_status_and_future.typ b/presentation/sections/04_status_and_future.typ new file mode 100644 index 0000000..0cd9a0a --- /dev/null +++ b/presentation/sections/04_status_and_future.typ @@ -0,0 +1,4 @@ +#import "../requirements.typ": * + +#focus-slide(theme: "neon")[Current Status and Future] +// = Current Status and Future \ No newline at end of file