Related Work
This is a list of documents that are related to the design & implementation of Aya, randomly ordered.
Universes
- Crude but Effective Stratification, byUnpublished ManuscriptThis is the foundation of universe polymorphism in Aya. I prefer calling this design 'McBride universes' to emphasize the origin. The design decision is subject to changes, though -- in case there is any substantial expressiveness limitation in practice.
- Generalized Universe Hierarchies and First-Class Universe Levels, byJust an interesting idea, not used in Aya.
- Dependently typed lambda calculus with a lifting operator, byA more implementation-oriented write-up of McBride universe, specifying the equational theory for terms.
- An Order-Theoretic Analysis of Universe Polymorphism, by , ,POPL 2023This paper justifies the theoretical strength and generality of McBride universe.
- Impredicative Observational Equality, by ,POPL 2023This paper adds observational equality to calculus of constructions. The impredicativity part I don't really care that much, but the overly complicated treatment of indexed families reminds me of transpX in cubical Agda. Maybe Aya is right about avoiding indexed families in the core type theory.
- Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality, by ,LMCS 2020TL;DR: the normal form of proofs of strict propositions need a special definition, and do not try to reduce these proof terms.
Quotients and Mutual Recursion related to Inductive Types
- Signatures and Induction Principles for Higher Inductive-Inductive Types, by ,LMCS 2020This paper contributes a way to compute induction principles and β-laws for qiits/hiits, but does not justify the existence of the initial algebras.
- Type Theory in Type Theory using Quotient Inductive Types, by ,POPL 2016This paper defines a dependent type theory as an interleaved qiit, which is supported natively by Aya. To do the same in Agda, one will need to use forward declarations.
- The Münchhausen Method in Type Theory, by , , ,TYPES 2022This paper justifies very dependent types in extensional type theory (or optionally in intensional type theory with transports), and motivates this feature with some examples. Aya supports this with automatic inference of type checking order and internal generation of forward declarations, without having to introduce mutual blocks or whatever special syntax for it.
- Observational Equality: Now for Good, by ,POPL 2022Observational type theory with effective quotients. Not very useful paper for implementation -- you will be able to guess the design without reading this paper.
Cubical Type Theory
- Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types, by , ,ICFP 2019The journal vesion of the Cubical Agda paper with more details, including transpX. This paper describes how the Cubical part of Cubical Agda works, which is not exactly how Aya works. But the ideas should transfer, such as the treatment of canonical hcomp in pattern matching. Cubical Agda uses De Morgan cubes, while Aya uses Cartesian cubes. But this shouldn't matter much with the presence of UIP anyway.
- Normalization for Cubical Type theory, by ,LICS 2020Unrelated to Aya, but very cool paper.
- Automating Kan composition, byMight be useful for automated cube filling in Aya in the future. The basic idea is to use forward reasoning to construct all cubes as we can.
- Syntax and models of Cartesian cubical type theory, by , , , , ,MSCS 2021The theoretical foundation of Cartesian cubical type theory, but it's full cubical type theory -- including the Glue type, which Aya does not need.
- A cubical type theory for higher inductive types, byA document listing all the rules for a variant of the CCHM cubical type theory (see below) with the possibility to have canonical hcomps. The reason is that hcomp can commute with point constructors, but for path constructors you can't really do anything about it. So they should be canonical. In CCHM, the primitive operation is heterogeneous comp (denoted just comp, without h, which is horrible notation), and it computes on all type formers. This document decomposes comp into hcomp and transp, and make hcomp conditionally canonical, but not transp. This design influences all the subsequent cubical type theories, I think.
- Cubical Type Theory: a constructive interpretation of the univalence axiom, by , , ,TYPES 2015The original CCHM paper. Good read, but use a different paper for reference if you want to implement cubical type theory.
- Computational Semantics of Cartesian Cubical Type Theory, byPhD thesisA good introduction to computational type theory, a flavor of type theory that defines types as their logical relation, and prove typing rules as theorems. Clearly, it is extrinsic typing, and type checking is very undecidable. But you get much stronger typing, including but not limited to equality reflection.
- A Cubical Language for Bishop Sets, by , ,LMCS 2022The XTT reference paper. Aya's cubical and related features are strictly weaker than this, because we want to avoid type cases and strict propositions. It's also unclear how to implement boundary separation efficiently. This paper can be used as a justification of the metatheory of Aya. If there is a consistency/soundness bug in Aya's cubical features, this paper will help us fix it.
Performance and Code Generation
- Staged Compilation with Two-Level Type Theory, byICFP 2022Cool paper, not directly related to Aya.
- Full Reduction at Full Throttle, by , ,CPP 2011Coq's native_compute. Similar but not exactly the same as Aya's JIT.
- A Compiled Implementation of Strong Reduction, by ,ICFP 2002Coq's vm_compute. The preliminary work of the above paper.
Implicits and Inference
- A Categorical Perspective on Pattern Unification, by ,
- The "Elaboration Zoo", byA basic tutorial on type theory elaboration using normalization by evaluation and explicit substitution closures, and solve implicits (also known as metavariables, which is a very bad name) using a not-so-good version of pattern unification.
- Elaboration with First-Class Implicit Function Types, byICFP 2020Fun paper, but I'd rather spend effort to avoid first-class implicit functions, because it's always unclear if you should infer the implicit at the end of a call, and manual annotation feels awkward.
- Higher-Order Constraint Simplification In Dependent Type Theory, byLFMTP 2009This paper extends pattern unification to allow delayed equations. Aya has exactly this. For implementers you only read page 10, and maybe refer to earlier pages if you don't understand the notations.
- Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference, by , , ,I haven't read this paper, but it can be useful. Aya pays extra attention to error messages.
Pattern Matching
- Copatterns: programming infinite structures by observations, by , , ,POPL 2013Everyone should know about copatterns because they are so cool, but no one cares about how productivity checking works except for very few people.
- Overlapping and Order-Independent Patterns, by , ,A cool pattern matching feature that's exclusively available in Aya. There is a more efficient implementation in Aya, but I have no time writing a paper about it.
- Elaborating Dependent (Co)Pattern Matching, by ,ICFP 2018The paper you need to read about coverage checking of dependent pattern matching. The uniform treatment of patterns and copatterns is very elegant.
Miscellaneous
- Contributions to Multimode and Presheaf Type Theory, bySome results on syntax and semantics of multimodal dependent type theory. Aya will eventually add native support for modalities, and this paper can be used as a reference of the type theory.
- Tabled Typeclass Resolution, by , ,Basically teaches you how to design the cache for type class resolution, to deal with multi-param typeclasses and class inheritance with large depth. It concerns with complicated instance resolution with backtracking.
- Coq's Vibrant Ecosystem for Verification Engineering, byCPP 2022
- The End of History? Using a Proof Assistant to Replace Language Design with Library Design, by , , , , , , ,SNAPL 2017