208 lines
7.8 KiB
Typst
208 lines
7.8 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,
|
|
)
|
|
|
|
#let Midas = [_*Midas*_]
|
|
|
|
#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*, as well as *dependent types*.
|
|
]
|
|
|
|
#isc-card(title: "Motivations")[
|
|
In real world data science, values may come in a variety of forms.
|
|
Sometimes they can be mixed 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.
|
|
|
|
While some programming languages use some form of static typing, Python applies the principles of _duck-typing_. This defers attributes and methods checks to *runtime* access, and omits any real type checks.
|
|
For example, the following:
|
|
```python
|
|
price_chf = 3.2
|
|
price_usd = 9.5
|
|
total = price_chf + price_usd
|
|
```
|
|
|
|
is perfectly valid Python code that will execute without error and even pass static type checking. However, the result will be a meaningless combination of two float values of different types.
|
|
|
|
#Midas was created to help developers and data engineers by (1)~allowing custom type definitions in a more powerful language than Python's type annotations, (2)~strictly carrying out static type checking and (3)~generating assertions to verify at runtime values which cannot be checked statically. This new type system also allows users to define some *dependent types*.
|
|
]
|
|
|
|
#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
|
|
|
|
#figure(
|
|
{
|
|
set par(justify: false)
|
|
architecture.overview
|
|
},
|
|
caption: [Implementation architecture overview]
|
|
) <fig:architecture>
|
|
|
|
First, typing rules were formally defined, drawing heavily on _Types and Progamming Languages_@tapl.
|
|
The implementation of the parser for the definition language 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 assertions to check that values do conform to the expected type.
|
|
]
|
|
|
|
#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.
|
|
|
|
*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
|
|
|
|
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)
|
|
]
|