576 lines
11 KiB
Typst
576 lines
11 KiB
Typst
#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
|
|
#import "@preview/conch:0.1.0"
|
|
|
|
#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)
|
|
|
|
---
|
|
|
|
#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))
|
|
)
|
|
])
|
|
|
|
#header-process(3)
|
|
|
|
#align(
|
|
center + horizon,
|
|
grid(
|
|
columns: 3,
|
|
column-gutter: 2em,
|
|
row-gutter: 1em,
|
|
[AST], none, none,
|
|
text(size: 2em)[+],
|
|
uncover("2-", text(size: 2em)[$stretch(->)^#{set text(size: 0.6em);```py ast.unparse(tree)```}$]),
|
|
uncover("2-")[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
|
|
|
|
#{
|
|
show raw: set text(size: 0.8em)
|
|
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()
|
|
```
|
|
|
|
#pause
|
|
|
|
#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
|
|
$
|
|
|
|
#pause
|
|
|
|
$
|
|
"type_of"(overline(x)) &= "type_of"( ("type_of"(x) + "type_of"(x)) / "type_of"(n) )\
|
|
pause
|
|
&= "type_of"( ("Meter" + "Meter") / "int") pause = "Meter"
|
|
$
|