feat(report): add draft plan
This commit is contained in:
159
report/plan.typ
Normal file
159
report/plan.typ
Normal file
@@ -0,0 +1,159 @@
|
||||
= General Plan
|
||||
1. *Abstract*: concise summary, includes: research question, methodology, results, conclusions
|
||||
2. *Résumé*: summary in French
|
||||
3. *Acknowledgements*: [Optional] thank those who supported your work
|
||||
4. *Table of Contents*
|
||||
5. *Introduction*: background/context, motivation, objectives, scope and plan
|
||||
6. *State of the Art / Literature Review*: existing research and situates thesis within academic context, if relevant to the work
|
||||
7. *Development and Methodology*: methods, materials, and procedures
|
||||
8. *Results*: findings, often with tables, figures, and analysis
|
||||
9. *Discussion*: Interpret results, discuss implications, and relate findings to research question
|
||||
10. *Conclusion*: Summarize main findings and contributions, suggest future work
|
||||
11. *References / Bibliography*: List all sources cited
|
||||
12. *Appendices*: (Optional) Contains supplementary material such as raw data, code, or additional explanations
|
||||
|
||||
|
||||
= Introduction
|
||||
|
||||
== Background / context
|
||||
- Programming
|
||||
- Deterministic -> ask the machine to do something, does it
|
||||
- Ambiguities come from developer
|
||||
- Python
|
||||
- Duck typing
|
||||
- (Highly) Dynamic
|
||||
- Very popular, especially in data science
|
||||
- Type hints
|
||||
- Type theory introduction
|
||||
- Why does the IDE know that float + str not valid, but not that EUR + USD is also invalid
|
||||
|
||||
== Motivation
|
||||
|
||||
- Python is often too flexible
|
||||
- Can be good but also confusing for beginners
|
||||
- Dangerous for production use
|
||||
- Even type-checkers can be too lenient
|
||||
- Runtime errors are the worst
|
||||
- Hour-long pipeline process crashing in the middle can be costly
|
||||
- Silent errors producing the wrong results are close to impossible to locate
|
||||
- Manually checking things can be tedious and unrewarding
|
||||
|
||||
== Objectives
|
||||
|
||||
Create a type system on top of Python, using type hints, which can help detect non-trivial type errors (i.e. not necessarily structurally wrong, and also on complex types like dataframes), and produces runtime assertions to check type conformity where static checking is not possible.
|
||||
|
||||
This system should ensure soundness where types are annotated or inferred, while leaving the user free to omit some and perform unsafe operations.
|
||||
|
||||
The system must be flexible to allow checking various kinds of constraints (e.g. value domain, geometric shape, distribution, etc.) and allow extension.
|
||||
|
||||
Finally, the system must be simple to use for average Python developers, and be able to seamlessly integrate into existing Python code.
|
||||
|
||||
== Scope and plan
|
||||
|
||||
TODO
|
||||
|
||||
= State of the art
|
||||
|
||||
- Python type hints (https://peps.python.org/pep-0484/):
|
||||
- base types
|
||||
- type aliases
|
||||
- structural subtyping with Protocols -> matches duck-typing (https://peps.python.org/pep-0544/)
|
||||
|
||||
- Existing type checkers
|
||||
- MyPy / Pylance
|
||||
|
||||
- Existing libraries
|
||||
- Pandera: runtime only, syntax heavy, but quite complete
|
||||
|
||||
- Similar ideas
|
||||
- Gator system (https://capra.cs.cornell.edu/research/gator/)
|
||||
|
||||
= Development and methodology
|
||||
|
||||
2 sections:
|
||||
1. theory
|
||||
2. implementation
|
||||
|
||||
== Theory
|
||||
|
||||
- Identify requirements
|
||||
- Introduction to TAPL
|
||||
- Grammar and typing rules for Midas, paralleled with TAPL
|
||||
- Omitted rules, simplifications, mechanisms not implemented
|
||||
|
||||
== Implementation
|
||||
|
||||
- Main elements
|
||||
- Definition language
|
||||
- Supported Python syntax (cf. grammar and typing rules)
|
||||
- Parse and type check
|
||||
- Produce user-facing diagnostics
|
||||
- Generate runtime assertions
|
||||
- Architecture overview
|
||||
|
||||
- Midas definition language
|
||||
- Lexer + parser (Crafting Interpreters, Pebble)
|
||||
- reference theory for grammar rules
|
||||
- token location -> necessary later for diagnostics
|
||||
- AST node generation, similar to CI (3 kinds, Stmt/Expr/Type)
|
||||
- Typer
|
||||
- reference theory for typing rules
|
||||
- type structures
|
||||
- types registry
|
||||
|
||||
- Python type checking
|
||||
- Parsing (short paragraph about AST nodes)
|
||||
- Resolver
|
||||
- Cf. CI
|
||||
- Assignment analysis
|
||||
- Typer
|
||||
- Returns / if-else
|
||||
- Environment
|
||||
- Static constraint evaluation
|
||||
|
||||
- Code generation
|
||||
- Stubs
|
||||
- Assertions
|
||||
|
||||
/*
|
||||
Subjects:
|
||||
- Variance inference
|
||||
- Environment
|
||||
- Resolver
|
||||
- Evaluator
|
||||
- CallDispatcher
|
||||
- Registry (`is_subtype`)
|
||||
- MethodRegistry (frames and columns)
|
||||
*/
|
||||
|
||||
|
||||
= Results
|
||||
|
||||
TODO
|
||||
|
||||
= Discussion
|
||||
|
||||
TODO
|
||||
|
||||
= Conclusion
|
||||
|
||||
TODO
|
||||
|
||||
== Future work
|
||||
|
||||
=== Python features
|
||||
- support for more common structures and methods (e.g. numpy array, more methods on dataframes)
|
||||
- support for more builtin types: Iterator, Sequence, etc.
|
||||
- argument sinks
|
||||
- while loops, lambdas, classes
|
||||
- multi-file project and imports
|
||||
|
||||
=== Typing features
|
||||
- expected type
|
||||
- literal value propagation
|
||||
|
||||
=== Improvements
|
||||
- more control on assertion type, for example to avoid expensive checks
|
||||
- less redundant check for know part of type (e.g. a dataframe is still a dataframe if only the columns have changed)
|
||||
- better integration with VSCode (e.g. inline diagnostics)
|
||||
- generate checks for members (does the object being cast have the given properties and methods?)
|
||||
Reference in New Issue
Block a user