Stories with Tag dependent types

• The Lisp in the Cellar: Dependent Types That Live Upstairs [pdf]

  permalink

  Posted: 2025-05-20 13:38:07

  Verbose tl;dr

  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.

  • Lisp
  • dependent types
  • type systems
  • Programming Languages
  • Functional Programming
  • Static Typing
  • Formal Verification
  • Theoretical Computer Science
  • PDF
  • Zenodo

  Summary of Comments ( 1 )
  https://news.ycombinator.com/item?id=44041515

  Verbose tl;dr

  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.

• Programming in Martin-Lof's Type Theory: An Introduction (1990)

  permalink

  Posted: 2025-05-17 06:30:59

  Verbose tl;dr

  Nordström, Petersson, and Smith's "Programming in Martin-Löf's Type Theory" provides a comprehensive introduction to Martin-Löf's constructive type theory, emphasizing its practical application as a programming language. The book covers the foundational concepts of type theory, including dependent types, inductive definitions, and universes, demonstrating how these powerful tools can be used to express mathematical proofs and develop correct-by-construction programs. It explores various programming paradigms within this framework, like functional programming and modular development, and provides numerous examples to illustrate the theory in action. The focus is on demonstrating the expressive power and rigor of type theory for program specification, verification, and development.

  Nordström, Petersson, and Smith's "Programming in Martin-Löf's Type Theory: An Introduction," published in 1990, provides a comprehensive and accessible exploration of Martin-Löf's type theory, emphasizing its practical application as a programming language. This seminal work meticulously outlines the theoretical underpinnings of the type theory, demonstrating its power as a foundation for both program specification and verification.

  The book meticulously constructs the type theory, starting with basic concepts and progressively introducing more complex ideas. It begins by elucidating the fundamental notion of types and their inhabitants, clarifying how these concepts correspond to specifications and programs, respectively. It details the principle of propositions as types, a cornerstone of the theory where mathematical propositions are represented as types, and their proofs are represented as elements inhabiting those types. This equivalence enables the formalization of mathematical reasoning within the type theory itself.

  The authors carefully explain the various type constructors available within Martin-Löf's system, including dependent function types (allowing functions whose output type depends on the input value), dependent product types (generalizing Cartesian products to allow the type of the second component to depend on the value of the first), and disjoint union types (allowing the representation of alternative choices). They meticulously illustrate the use of these constructors through numerous examples, showcasing how they facilitate the creation of complex data structures and algorithms.

  A significant portion of the book is dedicated to demonstrating the practical use of Martin-Löf's type theory for program development. The authors employ a constructive approach, whereby programs are extracted directly from proofs of their specifications. This methodology ensures that developed programs are demonstrably correct with respect to their intended behavior. Several concrete examples of program derivation are meticulously presented, demonstrating the application of this constructive methodology in practice.

  Moreover, the book explores the computational interpretation of Martin-Löf's type theory, showing how the evaluation of expressions within the theory can be viewed as a form of computation. This computational aspect connects the theoretical framework to practical programming, emphasizing the duality of types as both specifications and computational entities.

  Finally, the book delves into the formal system of Martin-Löf's type theory, providing a rigorous presentation of its rules and axioms. This formal treatment allows for a precise understanding of the theory's underlying logic and its properties, crucial for reasoning about the correctness and behavior of programs developed within the framework. Overall, "Programming in Martin-Löf's Type Theory: An Introduction" serves as a valuable resource for those seeking a deep understanding of the theory and its application in program construction and verification, offering a detailed and pedagogical introduction to a powerful and influential system for both logical reasoning and program development.

  • Martin-Lof Type Theory
  • type theory
  • programming
  • Functional Programming
  • dependent types
  • Constructive Mathematics
  • Intuitionistic Logic
  • proof assistants
  • formal methods
  • Theoretical Computer Science
  • Programming Language Theory
  • 1990
  • Introduction
  • Textbook
  • Computer Science

  Summary of Comments ( 0 )
  https://news.ycombinator.com/item?id=44012418

  Verbose tl;dr

  Hacker News users discuss the linked book, "Programming in Martin-Löf's Type Theory," primarily focusing on its historical significance and influence on functional programming and dependent types. Some commenters note its dense and challenging nature, even for those familiar with type theory, but acknowledge its importance as a foundational text. Others highlight the book's role in shaping languages like Agda and Idris, and its impact on the development of theorem provers. The practicality of dependent types in everyday programming is also debated, with some suggesting their benefits remain largely theoretical while others point to emerging use cases. Several users express interest in revisiting or finally tackling the book, prompted by the discussion.

  The Hacker News thread for "Programming in Martin-Lof's Type Theory: An Introduction (1990)" contains several comments discussing various aspects of the book and type theory in general.

  Several commenters praise the book for its clarity and accessibility, especially given the complexity of the subject matter. One user describes it as a "good introduction" and notes that it's available for free, which is appreciated. Another points out that it is "surprisingly readable" for a book on this topic. This readability is echoed by another commenter who suggests starting with this book before moving on to the more demanding "Homotopy Type Theory."

  The discussion also touches upon the practical applications of type theory. One commenter expresses interest in the connection between type theory and formal verification, a field using mathematical logic to guarantee the correctness of software and hardware systems. Another user raises the topic of dependent types, a key feature of Martin-Löf type theory, and their role in improving the reliability and expressiveness of programming languages like Idris.

  There's a brief exchange regarding the relationship between constructive mathematics and type theory. A commenter highlights the book's approach of explaining type theory through the lens of constructive mathematics, which is further elaborated on by another user stating that propositions as types makes for a practical implementation of the Brouwer-Heyting-Kolmogorov interpretation. This discussion emphasizes the deep connections between these areas of theoretical computer science and mathematics.

  The challenges of understanding and applying type theory are also acknowledged. One user admits to struggling with the material despite having a background in mathematics. However, the overall sentiment in the comments is positive, with many encouraging others to explore the book and the field of type theory. The free availability of the book is mentioned multiple times as a major advantage for those interested in learning.

  Finally, a few comments provide additional resources related to type theory, including links to online courses and other relevant books. This further contributes to the thread's role as a valuable starting point for anyone interested in delving into the world of Martin-Löf type theory and its applications.

• Show HN: Formalizing Principia Mathematica using Lean

  permalink

  Posted: 2025-04-25 18:49:30

  Verbose tl;dr

  Andrew N. Aguib has launched a project to formalize Alfred North Whitehead and Bertrand Russell's Principia Mathematica within the Lean theorem prover. This ambitious undertaking aims to translate the foundational work of mathematical logic, known for its dense symbolism and intricate proofs, into a computer-verifiable format. The project leverages Lean's powerful type theory and automated proof assistance to rigorously check the Principia's theorems and definitions, offering a modern perspective on this historical text and potentially revealing new insights. The project is ongoing and currently covers a portion of the first volume. The code and progress are available on GitHub.

  This GitHub repository, titled "Formalizing Principia Mathematica using Lean," documents an ambitious project undertaken by Andrew N. Aguib to translate and verify Alfred North Whitehead and Bertrand Russell's monumental work, Principia Mathematica, within the Lean proof assistant. Principia Mathematica, a three-volume work published between 1910 and 1913, represents a landmark attempt to ground mathematics in symbolic logic, aiming to demonstrate that all mathematical truths could be derived from a small set of logical axioms and inference rules. Aguib's project leverages the power of Lean, a modern, interactive theorem prover, to rigorously formalize the definitions, theorems, and proofs presented in Principia. This involves translating the often-opaque symbolic language and intricate arguments of the original text into Lean's precise and computationally verifiable format. The repository contains Lean code corresponding to various sections of Principia, effectively creating a digital, interactive version of the foundational text. This allows for a level of scrutiny and analysis not possible with the original printed work. The formalization process not only helps verify the correctness of the original proofs but also provides a clearer and more accessible representation of the underlying logic. The project is ongoing, with the current state reflecting progress made in formalizing different parts of Principia. The repository serves as a dynamic record of this effort, allowing others to follow, contribute to, and benefit from the ongoing work of translating this historically significant mathematical text into a modern, computationally verifiable form. This endeavor offers valuable insights into the foundations of mathematics, the evolution of logical systems, and the capabilities of modern proof assistants in tackling complex mathematical formalizations. By making Principia Mathematica accessible and verifiable within a powerful computational framework like Lean, the project aims to facilitate a deeper understanding and appreciation of this seminal work in mathematical logic.

  • lean
  • Theorem Prover
  • Principia Mathematica
  • Formalization
  • mathematics
  • Logic
  • Automated Reasoning
  • formal systems
  • Russell
  • Whitehead
  • proof assistant
  • type theory
  • dependent types
  • interactive theorem proving

  Summary of Comments ( 32 )
  https://news.ycombinator.com/item?id=43797256

  Verbose tl;dr

  Hacker News users discussed the impressive feat of formalizing parts of Principia Mathematica in Lean, praising the project for its ambition and clarity. Several commenters highlighted the accessibility of the formalized proofs compared to the original text, making the dense mathematical reasoning easier to follow. Some discussed the potential educational benefits, while others pointed out the limitations of formalization, particularly regarding the philosophical foundations of mathematics addressed in Principia. The project's use of Lean 4 also sparked a brief discussion on the theorem prover itself, with some commenters noting its relative novelty and expressing interest in learning more. A few users referenced similar formalization efforts, emphasizing the growing trend of using proof assistants to verify complex mathematical work.

  The Hacker News post titled "Show HN: Formalizing Principia Mathematica using Lean" (https://news.ycombinator.com/item?id=43797256) has generated a modest number of comments, primarily focusing on the complexities and nuances of formalizing mathematical proofs, particularly within the context of Principia Mathematica.

  One commenter highlights the historical context of Principia, emphasizing its significance as a pre-computer-era attempt to formalize mathematics. They point out the inherent challenges in such an endeavor, particularly the book's verbose and intricate symbolic notation. This comment also touches on the evolution of logical systems and proof assistants, contrasting Principia's methods with more modern approaches.

  Another commenter questions the practical applications of formalizing Principia. They acknowledge the intellectual value of the project but wonder about its relevance to modern mathematics, particularly given the availability of more efficient and powerful proof assistants. This sparks a discussion about the differences between simply verifying existing proofs and actually creating new ones within a formal system.

  A subsequent comment clarifies the distinction between verifying and formalizing a proof. They explain that formalization involves encoding the entire logical structure of a proof within a computer system, allowing for automated checking of each individual step. This is contrasted with mere verification, which might involve a human checking the overall logic of a proof without necessarily breaking down every minute detail.

  Another thread delves into the specifics of Lean, the proof assistant used in this project. Commenters discuss its strengths and weaknesses, comparing it to other systems like Coq and Isabelle. The discussion touches upon the tradeoffs between the accessibility and expressiveness of different proof assistants. One commenter mentions the potential of using Lean for educational purposes, given its relatively user-friendly interface.

  Finally, a comment praises the project for its ambition and potential to contribute to the field of automated theorem proving. They acknowledge the limitations of current technology but express optimism about the future of formal mathematics and the role projects like this can play in advancing the field.

  In summary, the comments on this Hacker News post reflect a nuanced understanding of the challenges and opportunities associated with formalizing mathematical proofs. They range from discussions about the historical significance of Principia Mathematica to the practicalities of using modern proof assistants like Lean. The overall tone is one of cautious optimism, acknowledging the limitations of current technology while recognizing the potential for future advancements.

• The Future Is Niri

  permalink

  Posted: 2025-03-12 11:42:16

  Verbose tl;dr

  Niri is a new programming language designed for building distributed systems. It aims to simplify concurrent and parallel programming by introducing the concept of "isolated objects" which communicate via explicit message passing, eliminating shared mutable state and thus avoiding data races and other concurrency bugs. This approach, coupled with automatic memory management and a focus on performance, makes Niri suitable for developing robust and efficient distributed applications, potentially replacing complex actor models or other concurrency paradigms. The language is still under development, but shows promise for streamlining the creation of complex distributed systems.

  The blog post "The Future Is Niri" by Alexej Diez introduces Niri, a novel programming language designed to address the limitations of existing languages, particularly regarding concurrency and memory management. Diez posits that the current landscape of programming languages, while offering a variety of paradigms and tools, struggles to adequately manage the increasing complexities of modern hardware and software architectures, especially in the realm of parallel and distributed computing. He argues that prevalent approaches to concurrency, like shared memory with mutexes or message passing, are inherently prone to errors and difficult to reason about, leading to significant development overhead and susceptibility to subtle bugs.

  Niri, as Diez elaborates, aims to overcome these challenges by introducing a fundamentally different model centered around the concept of isolated state, inspired by the actor model and offering a "shared nothing" concurrency paradigm. Each computational unit in Niri operates within its own isolated state, precluding shared mutable state and thus eliminating data races and other concurrency-related issues. Communication between these isolated units is achieved through asynchronous message passing, ensuring a deterministic and predictable execution flow, irrespective of the underlying hardware architecture or the number of concurrent operations.

  The post delves into the specifics of Niri's syntax and semantics, highlighting its focus on simplicity and clarity. It emphasizes a type system designed for both safety and performance, allowing for compile-time detection of various errors and enabling efficient code generation. Diez further explains the memory management model of Niri, which leverages a combination of automatic memory management, employing techniques akin to garbage collection, along with explicit memory allocation control for fine-grained optimization when necessary. This dual approach provides the convenience of automated memory management without sacrificing the potential for performance optimization in critical sections of code.

  Furthermore, the post underscores the potential of Niri to facilitate the development of robust and scalable distributed systems. By inherent design, Niri's isolation model and asynchronous communication primitives naturally align with the requirements of distributed computing, simplifying the process of designing and implementing complex distributed applications. Diez concludes by expressing his belief that Niri represents a significant step towards a future where concurrent and distributed programming is significantly more accessible and less error-prone, ultimately leading to more robust and performant software systems. He anticipates that Niri’s unique features will pave the way for innovation in various domains, particularly those demanding high concurrency and reliability.

  • Niri
  • Ersei
  • programming language
  • Functional Programming
  • Static Typing
  • dependent types
  • theorem proving
  • Formal Verification
  • Software Development
  • Compilers

  Summary of Comments ( 21 )
  https://news.ycombinator.com/item?id=43342178

  Verbose tl;dr

  Hacker News users discussed Niri's potential, focusing on its novel approach to UI design. Several commenters expressed excitement about the demo, praising its speed and the innovative concept of manipulating data directly within the interface. Concerns were raised about the practicality of text-based interaction for complex tasks and the potential learning curve. Some questioned the long-term viability of relying solely on a keyboard-driven interface, while others saw it as a powerful tool for experienced users. The discussion also touched upon comparisons to other tools like spreadsheets and the potential benefits for specific use cases like data analysis and programming. Some users expressed skepticism, finding the current implementation limited and wanting to see more concrete examples of its capabilities.

  The Hacker News post "The Future Is Niri," linking to an article describing a hypothetical new internet protocol called Niri, generated several comments discussing its feasibility, potential benefits, and drawbacks.

  Several commenters expressed skepticism about Niri's claims and its ability to overcome existing internet infrastructure challenges. One commenter questioned the practicality of Niri's micropayment system for content retrieval, highlighting the existing complexities and costs associated with micropayment infrastructure. They also pointed out the potential for abuse and the difficulty in determining fair pricing for various types of content. Another skeptic argued that the benefits of Niri, such as censorship resistance and improved efficiency, are overstated and that similar functionalities are already achievable or in development within existing protocols. The commenter also raised concerns about the cost and complexity of transitioning to a new internet architecture.

  A recurring theme in the comments was the difficulty of replacing the existing internet infrastructure. Commenters pointed out the entrenched nature of TCP/IP and the massive undertaking required to transition to a new protocol. They also questioned the economic incentives for such a shift, given the significant investments already made in current technologies. One commenter drew parallels with previous attempts to create alternative internet architectures, suggesting that Niri might face similar challenges in gaining widespread adoption.

  Despite the skepticism, some commenters expressed interest in Niri's potential. One commenter praised the innovative approach and the focus on addressing some of the internet's limitations, particularly in the areas of security and efficiency. They acknowledged the significant hurdles to implementation but encouraged further exploration of the concept. Another commenter specifically highlighted the potential of Niri's addressing system to improve routing efficiency and reduce latency.

  The discussion also touched upon the technical aspects of Niri, with some commenters questioning the specifics of its implementation and its ability to scale to the size of the current internet. One commenter raised concerns about the potential for denial-of-service attacks and the need for robust mechanisms to mitigate such threats.

  Overall, the comments on the Hacker News post reflect a mix of skepticism and cautious optimism towards Niri. While some commenters see potential in its innovative approach, others remain unconvinced of its practicality and ability to overcome the significant challenges associated with replacing the existing internet infrastructure. The discussion highlights the complex considerations involved in developing and deploying a new internet protocol and the importance of addressing issues such as scalability, security, and economic incentives.