Gradual Typing is the idea of using both static and dynamic typing in the same program. Most notably, TypeScript is a gradually-typed version of JavaScript, allowing users to add statically-checked type annotations to parts of their otherwise dynamically-typed JavaScript code. However, TypeScript is unsound, meaning that its type annotations do not necessarily reflect what actual values a variable or field may contain at runtime. As such, type annotations cannot be used for optimization purposes, though they are still useful for IDE functionality and for finding obvious type errors.
In order to guarantee soundness, i.e. the property that type annotations do correctly characterize the relevant run-time values, a gradually-typed language needs to insert run-time type-checks, which can be very expensive. Finally, many language features and idioms are specific to either dynamically- or statically-typed languages; a gradually-typed language will have to support its features and idioms in both disciplines, which can be tricky and lead to unexpected behaviors.
The projects advertised here will be in the context of the ongoing research on programming language design and implementation for gradual typing to find a way to avoid all three problems (unsoundness, low performance, unexpected behaviors) in an industrial object-oriented language, as roughly a mix of a Python/JavaScript-style language on the dynamic end and a Java/C#-style language on the static end, including
- implementation techniques for efficient run-time checks
- design and implementation of common language features adapted to gradual typing
- efficiently expressing dynamic/static idioms in the respective other setting
Example problems:
- Generics in Gradual Typing
- Run-Time Type Evolution/Gradual Type-State
- Dynamic handling of member visibility (public/private/protected)
- Static member initialization