fix(poster): improve
remove redundant parts, rephrase, add example of error
This commit is contained in:
+36
-27
@@ -79,28 +79,31 @@
|
||||
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 too.
|
||||
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: "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.
|
||||
#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.
|
||||
|
||||
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*.
|
||||
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
|
||||
```
|
||||
|
||||
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.
|
||||
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.
|
||||
|
||||
#figure(
|
||||
{
|
||||
set par(justify: false)
|
||||
architecture.overview
|
||||
},
|
||||
caption: [Implementation architecture overview]
|
||||
) <fig:architecture>
|
||||
#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")[
|
||||
@@ -110,9 +113,16 @@
|
||||
- *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.
|
||||
#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*.
|
||||
]
|
||||
|
||||
@@ -164,15 +174,7 @@
|
||||
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
|
||||
Cast expressions such as in @fig:example-python:2 insert runtime assertions to check that values do conform to the expected type.
|
||||
]
|
||||
|
||||
#let repos = (
|
||||
@@ -181,7 +183,14 @@
|
||||
)
|
||||
|
||||
#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.
|
||||
#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(
|
||||
|
||||
Reference in New Issue
Block a user