199 lines
8.0 KiB
Typst
199 lines
8.0 KiB
Typst
// ___ ____ ____ _ _ _____ ___
|
|
// |_ _/ ___| / ___| | | | | ____|_ _| Informatique et
|
|
// | |\___ \| | ___ | |_| | _| | | systèmes de communication
|
|
// | | ___) | |__|___| | _ | |___ | | HEI Sion · HES-SO Valais / mui 24-26
|
|
// |___|____/ \____| |_| |_|_____|___|
|
|
//
|
|
// 52 65 61 64 69 6e 67 20 68 65 78 20 66 6f 72 20 66 75 6e 3f 20 49 53 43 20 66 6f 72 65 76 65 72
|
|
//
|
|
|
|
#import "@preview/isc-hei-poster:0.8.1": isc-poster, isc-card, isc-colbreak
|
|
#import "@preview/cetz:0.5.2": canvas, draw
|
|
#import "../meta.typ"
|
|
#import "../report/figs/architecture.typ"
|
|
#import "@local/codly:1.3.1": codly, codly-init, local
|
|
#import "@preview/codly-languages:0.1.10": codly-languages
|
|
|
|
#let poster-orientation = "portrait"
|
|
|
|
#show: codly-init
|
|
#codly(
|
|
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 raw.where(block: true): set text(size: 0.9em)
|
|
|
|
/*
|
|
#show columns: it => {
|
|
it
|
|
|
|
place(
|
|
top + center,
|
|
//dx: 0cm,
|
|
//dy: 21cm,
|
|
dx: -6cm,
|
|
dy: 21.3cm,
|
|
rect(
|
|
stroke: gray + 2pt,
|
|
fill: white,
|
|
radius: 0.5cm,
|
|
//image("../assets/icon.svg", width: 3cm)
|
|
image("../assets/icon.svg", width: 4cm)
|
|
)
|
|
)
|
|
}
|
|
*/
|
|
|
|
#show: isc-poster.with(
|
|
title: meta.title,
|
|
subtitle: meta.subtitle,
|
|
student: meta.authors,
|
|
permanent-email: meta.permanent-email,
|
|
supervisor:meta.thesis-supervisor,
|
|
co-supervisor: none,
|
|
expert: meta.thesis-expert,
|
|
thesis-id: meta.thesis-id,
|
|
academic-year: "2025-2026",
|
|
school: meta.school,
|
|
programme: "Informatique et systèmes de communication",
|
|
major: meta.major,
|
|
orientation: poster-orientation,
|
|
language: "en", // Valid values are [en, fr, de]
|
|
num-columns: 2,
|
|
distribute-columns: true,
|
|
)
|
|
|
|
#isc-card(title: "Summary")[
|
|
Python is one of the most popular programming languages, especially in data science. Although highly flexible and somewhat easy to learn, its leniency can often lead to type errors. Indeed, with duck-typing, the developer is responsible for making sure operations are valid and do what they are meant to do.
|
|
This project introduces *Midas*, a new type system built on top of Python's type hints, capable of checking types at *compile-time* and generating *runtime assertions* for cases that are not statically known.
|
|
Midas allows users to define *custom types* in a simple DSL, use them in Python type hints and compile their code to a fully type-checked script with added assertions.
|
|
Its typing rules are stricter than Python's and allow typing complex operations on Pandas dataframes too.
|
|
]
|
|
|
|
#isc-card(title: "Introduction")[
|
|
Data science and data engineering, by definition, involve handling some kind of data. In the real world, data comes in a variety of forms. Sometimes, different kinds of values can be mixed, such as when computing a speed from a distance and a duration, but sometimes they cannot. This is exactly what happened to NASA's Mars Climate Orbiter, which failed its orbital insertion because of a unit mixup@MCOReport.
|
|
|
|
To avoid such mistakes, many programming languages and frameworks use some form of static typing, which allows compiler to detect, report and prevent mixing incompatible values before even running the program. Python does not use such a system but rather implements _duck-typing_. This allows developers to completely omit typing annotations and the interpreter will only check the necessary attributes and methods when they are accessed *at runtime*.
|
|
|
|
Static type checkers such as Pyright and MyPy already provide some informational diagnostics, but do not _enforce_ safety.
|
|
I developed *Midas* to help developers and data engineers even further by (1)~allowing custom type definitions in a more powerful language than Python's type annotations and (2)~generating assertions to verify at runtime values which cannot be checked statically. This new type system also allows users to define some *dependent types*, binding value constraints which are checked at runtime.
|
|
|
|
#figure(
|
|
{
|
|
set par(justify: false)
|
|
architecture.overview
|
|
},
|
|
caption: [Implementation architecture overview]
|
|
) <fig:architecture>
|
|
]
|
|
|
|
#isc-card(title: "Implementation")[
|
|
The type checker is composed of four main elements, as shown in @fig:architecture:
|
|
- *Types Registry*: holds all builtin and user-defined types
|
|
- *Midas Typer*: parses custom definitions and registers types
|
|
- *Python Typer*: checks Python source code
|
|
- *Generator*: inserts runtime assertions to produce a runnable script
|
|
|
|
Typing rules were first formally defined, drawing heavily on _Types and Progamming Languages_@tapl.
|
|
The definition language parser's implementation follows R. Nystrom's _Crafting Interpreters_@Nystrom2021. The whole system is itself implemented in Python, leveraging the language's own `ast` module to parse and manipulate source code.
|
|
|
|
The type checker also includes some machinery to infer the result types of several *dataframe operations* and *aggregation methods*.
|
|
]
|
|
|
|
#isc-colbreak()
|
|
|
|
#isc-card(title: "Results")[
|
|
Developers can define *custom types* and *predicates* using the Midas language. *Dependent types* and *dataframe schemas* are supported, as shown in @fig:example-midas.
|
|
|
|
#codly(
|
|
header: [types.midas]
|
|
)
|
|
#figure(
|
|
```midas
|
|
predicate not_empty(text: str) = len(text) != 0
|
|
type Height = float where _ >= 0
|
|
alias People = Frame[
|
|
name: str where not_empty(_),
|
|
height: Height
|
|
]
|
|
```,
|
|
caption: [Example custom type definitions]
|
|
) <fig:example-midas>
|
|
|
|
These types can then be used in a regular Python script. Running the type checker and compiler will then produce _diagnostics_. Some may be simple warnings about unknown variables, but definite type errors will prevent compilation. As demonstrated in @fig:example-python, type checking of dataframe operations is rather extensive, providing great coverage of common data science applications.
|
|
#codly(
|
|
header: [script.py],
|
|
highlights: (
|
|
(
|
|
line: 3,
|
|
start: 11,
|
|
tag: [#h(2pt)Column[Height]],
|
|
fill: blue.lighten(60%)
|
|
),
|
|
(
|
|
line: 4,
|
|
start: 17,
|
|
tag: [#h(2pt)Height],
|
|
fill: blue.lighten(60%)
|
|
),
|
|
)
|
|
)
|
|
#figure(
|
|
```python
|
|
import pandas as pd
|
|
people: People = cast(People, pd.read_csv(...))
|
|
heights = people["height"]
|
|
median_height = heights.median()
|
|
```,
|
|
caption: [Example type checking of dataframe operations]
|
|
) <fig:example-python>
|
|
|
|
Cast expressions such as in @fig:example-python:2 insert runtime assertion to check that values do conform to the expect type.
|
|
]
|
|
|
|
#isc-card(title: "Discussion")[
|
|
*Strengths~:* strict static checking of a great subset of Python, thorough runtime checking of cast expressions and dependent types, extensive type inference of dataframe operations, modular and easily extensible
|
|
|
|
*Current Limitations~:* bypass of logical short-circuiting, unsupported reverse operators, oblivious to references and remote modifications
|
|
|
|
*Possible Extensions~:* multi-file projects with ```py import``` statements, Numpy arrays, constraint solving
|
|
]
|
|
|
|
#let repos = (
|
|
([Main repository], path("figs/qr_gitea.svg"), meta.project-repos),
|
|
([Mirror], path("figs/qr_github.svg"), meta.mirror-repo),
|
|
)
|
|
|
|
#isc-card(title: "Conclusion")[
|
|
Midas provides a solid foundation for a hybrid typing system which can make Python better and safer. Its modular architecture makes it easily extensible.
|
|
The source code is published openly under the Apache 2.0 license.
|
|
|
|
#grid(
|
|
columns: (1fr,) * repos.len(),
|
|
align: center,
|
|
..repos.map(r => strong(text(size: 0.8em, r.at(0)))),
|
|
..repos.map(r => image(r.at(1), width: 3cm)),
|
|
..repos.map(r => text(size: 0.8em, r.at(2)))
|
|
)
|
|
]
|
|
|
|
#isc-card(title: "References")[
|
|
#bibliography("../report/bibliography.bib", title: none)
|
|
]
|