Richard talks with José Valim, creator of Elixir, about gradual vs static typing. They discuss dynamic typing in TypeScript, expressiveness and correctness in API design, resurgence of static typing, notebooks in data science, and the tug of war between gradual and static typing.
The Elixir programming language is exploring set theoretic types to find a type system that can model idioms while maintaining correctness.
Gradual typing strikes a balance between expressiveness and correctness by allowing dynamic parts of the code while introducing static typing.
Using more expressive types, like intersections, allows for fine-grained control over types and avoids breaking changes while evolving functions.
Deep dives
Set theoretic types for Elixir
The Elixir programming language is exploring the use of set theoretic types, partnering with a researcher from CNRS. They have developed a prototype to validate the concept. The goal is to find a type system that can model as many idioms as possible while maintaining correctness. The challenge lies in understanding complex conditional code and ensuring the type system can handle it. There is also a consideration for message passing between processes, where gradual typing is useful for handling complex data structures. However, there are still open questions on how to handle occurrence typing and the limitations in dynamic aspects of the language.
Trade-offs between static and gradual typing
The discussion explores the trade-offs between static typing and gradual typing. Static typing provides more correctness but can impact the developer experience and expressiveness. Gradual typing seeks to balance expressiveness and correctness by allowing some parts of the code to remain dynamic while introducing static typing. The debate considers the impact on API design and readability, as well as the challenges of evolving a static type system without breaking existing code.
Considering expressiveness and correctness
The use of gradual typing in existing dynamic languages allows for more correctness without sacrificing expressiveness. The dynamic aspects of a language can be gradually typed while preserving flexibility and allowing for evolutionary changes. Structural typing and handling of specific use cases, like nullable types, can contribute to a more secure type system without compromising expressive power.
Future considerations for gradual typing
The discussion touches on the possibility of gradually typed languages exploring structural typing and the benefits it can bring. As gradual typing continues to evolve, new expressive powers may be discovered that can inspire changes in static languages. Striking the right balance between expressiveness and correctness will continue to be a topic of exploration and discussion in the future.
The power and challenges of type variables
Type variables are a useful tool in programming languages for defining functions that can return different types based on the input. However, type variables have limitations when it comes to expressing precise behavior and can lead to problems when evolving functions. By using more expressive types, such as intersections, it is possible to encode additional information about the behavior of a function and evolve it without breaking existing code. This approach allows for more fine-grained control over types and prevents the need to choose between breaking changes and maintaining backward compatibility.
Gradual typing and soundness
Gradual typing offers a way to combine static and dynamic typing in a single language. However, one challenge is maintaining soundness while avoiding excessive runtime checks or sacrificing performance. A new approach called strong arrows leverages runtime checks already performed by the runtime to determine whether dynamic behavior is needed. This approach allows for a sound gradual typing system without introducing additional runtime checks. While the implications for runtime representation and performance optimizations are still being explored, it holds promise for achieving the benefits of both static and dynamic typing.
