This paper introduces Deputy, a dependently typed language designed for practical programming. Deputy integrates dependent types into a Lisp-like language, aiming to balance the power of dependent types with the flexibility and practicality of dynamic languages. It achieves this through a novel combination of features: gradual typing, allowing seamless mixing of typed and untyped code; a hybrid type checker employing both static and dynamic checks; and a focus on intensional type equality, allowing for type-level computation and manipulation. This approach makes dependent types more accessible for everyday tasks by allowing programmers to incrementally add type annotations and leverage dynamic checking when full static verification is impractical or undesirable, ultimately bridging the gap between the theoretical power of dependent types and their use in real-world software development.
The paper "The Lisp in the Cellar: Dependent Types That Live Upstairs" explores a novel approach to integrating dependent types into a practical programming language, specifically targeting the challenges of combining the flexibility and dynamism of Lisp with the strong static guarantees offered by dependent types. It argues against the common strategy of embedding a dependently typed core within a dynamic language, likened to keeping a powerful but restricted "Lisp in the cellar," accessed only for specific, type-checked components. Instead, the paper proposes bringing dependent types "upstairs" to permeate the entire language, empowering programmers to leverage their benefits throughout the codebase.
This approach centers around the concept of "Transient Gradual Typing," a system designed to gracefully bridge the gap between dynamic and static typing within the same language. This allows for the incremental adoption of dependent types, meaning programmers can selectively apply them to critical parts of their code while leaving other sections dynamically typed. This flexibility accommodates the evolutionary nature of software development, where initial exploration and rapid prototyping might benefit from dynamic typing, while later stages require the rigor and safety of dependent types.
The key mechanism enabling Transient Gradual Typing is a sophisticated form of runtime contract checking. When a dependently typed function interacts with dynamically typed code, contracts are generated and enforced at runtime. These contracts ensure that the dynamically typed values adhere to the expected types specified by the dependently typed functions, thus preserving type safety even across the dynamic-static boundary. This differs from traditional gradual typing, which relies on type coercions and may introduce runtime errors if coercions fail. Transient Gradual Typing, on the other hand, provides stronger guarantees by explicitly checking the expected types.
Furthermore, the paper introduces a novel approach to contract generation and enforcement, leveraging a technique termed "contract specialization." This technique optimizes the runtime overhead of contract checking by generating specialized contracts based on the specific context of the interaction between statically and dynamically typed code. This avoids the performance penalties typically associated with generic contract checking.
The proposed system is implemented in a prototype language called "Deputy." Deputy is a dialect of Lisp augmented with dependent types and the mechanisms for Transient Gradual Typing. The paper details the design and implementation of Deputy, including its type system, contract generation algorithm, and runtime environment. It also provides examples demonstrating how Deputy allows programmers to seamlessly mix dynamic and dependent typing, highlighting the practical benefits of the proposed approach.
Finally, the paper evaluates the performance of Deputy using a series of benchmarks. The results suggest that the overhead introduced by contract checking and Transient Gradual Typing is manageable, demonstrating the feasibility of integrating dependent types into a dynamic language without sacrificing performance. The paper concludes by discussing future research directions, including further optimizations for contract specialization and the exploration of more advanced type system features. The overall contribution is a compelling vision for a more unified approach to integrating dependent types into practical programming languages, enabling programmers to benefit from both the flexibility of dynamic typing and the rigor of static typing within a single, cohesive environment.
Summary of Comments ( 1 )
https://news.ycombinator.com/item?id=44041515
Hacker News users discuss the paper "The Lisp in the Cellar: Dependent Types That Live Upstairs," focusing on the practicality and implications of its approach to dependent types. Some express skepticism about the claimed performance benefits and question the trade-offs made for compile-time checking. Others praise the novelty of the approach, comparing it favorably to other dependently-typed languages like Idris and highlighting the potential for more efficient and reliable software. A key point of discussion revolves around the use of a "cellar" for runtime values and an "upstairs" for compile-time values, with users debating the elegance and effectiveness of this separation. There's also interest in the language's metaprogramming capabilities and its potential for broader adoption within the functional programming community. Several commenters express a desire to experiment with the language and see further development.
The Hacker News post titled "The Lisp in the Cellar: Dependent Types That Live Upstairs [pdf]" links to a PDF describing a programming language called Deputy. The discussion in the comments section is relatively brief, with a focus on the practicality and implications of the presented ideas.
One commenter expresses skepticism about the overall benefit of dependent types, questioning if the added complexity is worth the effort and if the advantages primarily apply to specific niches like formal verification. They seem to imply that for general-purpose programming, the trade-offs might not be favorable.
Another commenter points out a perceived similarity between Deputy's approach and the concept of gradual typing. They suggest that Deputy seems to be striving for a system where dependent types can be introduced incrementally, allowing developers to choose where and when to apply the stricter typing discipline.
A third comment delves into the technical details of Deputy's type system, highlighting its use of elaboration and normalization. They specifically mention that values are normalized during elaboration, comparing this approach to how Agda, another dependently typed language, handles type checking. They also raise a question about the implementation of large eliminations, a technical aspect related to how dependent types are handled in practice.
Finally, someone notes the irony in the paper's title, "The Lisp in the Cellar: Dependent Types That Live Upstairs," by pointing out that historically, Lisp has often been associated with more academic or advanced programming concepts, while dependent types are now being brought into that same realm. This comment focuses on the shifting perceptions and adoption of these programming paradigms.
While there are other comments, they are largely short expressions of interest, questions about specific technical details, or requests for clarification. The comments summarized above represent the most substantial points of discussion and offer insights into the community's reaction to the Deputy language and its features.