Reference. The view from the left
Pattern matching has proved an extremely powerful and durable notion in functional programming. This paper contributes a new programming notation for type theory which elaborates the notion in various ways. First, as is by now quite well-known in the type theory community, definition by pattern matching becomes a more discriminating tool in the presence of dependent types, since it refines the explanation of types as well as values. This becomes all the more true in the presence of the rich class of datatypes known as inductive families (Dybjer, 1991). Secondly, as proposed by Peyton Jones (1997) for Haskell, and independently rediscovered by us, subsidiary case analyses on the results of intermediate computations, which commonly take place on the right-hand side of definitions by pattern matching, should rather be handled on the left. In simply-typed languages, this subsumes the trivial case of Boolean guards; in our setting it becomes yet more powerful. Thirdly, elementary pattern matching decompositions have a well-defined interface given by a dependent type; they correspond to the statement of an induction principle for the datatype. More general, user-definable decompositions may be defined which also have types of the same general form. Elementary pattern matching may therefore be recast in abstract form, with a semantics given by translation. Such abstract decompositions of data generalize Wadler’s (1987) notion of ‘view’. The programmer wishing to introduce a new view of a type , and exploit it directly in pattern matching, may do so via a standard programming idiom. The type theorist, looking through the Curry–Howard lens, may see this as proving a theorem , one which establishes the validity of a new induction principle for . We develop enough syntax and semantics to account for this high-level style of programming in dependent type theory. We close with the development of a typechecker for the simply-typed lambda calculus, which furnishes a view of raw terms as either being well-typed, or containing an error. The implementation of this view is ipso facto a proof that typechecking is decidable.
Cite
Cited by (8)
Intrinsically Correct Sorting in Cubical Agda alexandruIntrinsicallyCorrectSorting2025
The paper “Sorting with Bialgebras and Distributive Laws” by Hinze et al. uses the framework of bialgebraic semantics to define sorting algorithms. From distributive laws between functors they construct pairs of sorting algorithms using both folds and unfolds. Pairs of sorting algorithms arising this way include insertion/selection sort and quick/tree sort. We extend this work to define intrinsically correct variants in cubical Agda. Our key idea is to index our data types by multisets, which concisely captures that a sorting algorithm terminates with an ordered permutation of its input list. By lifting bialgebraic semantics to the indexed setting, we obtain the correctness of sorting algorithms purely from the distributive law.
Coverage Semantics for Dependent Pattern Matching eremondi-2025-coverage
Dependent pattern matching is a key feature in dependently typed programming. However, there is a theory-practice disconnect: while many proof assistants implement pattern matching as primitive, theoretical presentations give semantics to pattern matching by elaborating to eliminators. Though theoretically convenient, eliminators can be awkward and verbose, particularly for complex combinations of patterns. This work aims to bridge the theory-practice gap by presenting a direct categorical semantics for pattern matching, which does not elaborate to eliminators. This is achieved using sheaf theory to describe when sets of arrows (terms) can be amalgamated into a single arrow. We present a language with top-level dependent pattern matching, without specifying which sets of patterns are considered covering for a match. Then, we give a sufficient criterion for which pattern-sets admit a sound model: patterns should be in the canonical coverage for the category of contexts. Finally, we use sheaf-theoretic saturation conditions to devise some allowable sets of patterns. We are able to express and exceed the status quo, giving semantics for datatype constructors, nested patterns, absurd patterns, propositional equality, and dot patterns.
Focusing on Refinement Typing economou-2023-focusing
We present a logically principled foundation for systematizing, in a way that works with any computational effect and evaluation order, SMT constraint generation seen in refinement type systems for functional programming languages. By carefully combining a focalized variant of call-by-push-value, bidirectional typing, and our novel technique of value-determined indexes, our system generates solvable SMT constraints without existential (unification) variables. We design a polarized subtyping relation allowing us to prove our logically focused typing algorithm is sound, complete, and decidable. We prove type soundness of our declarative system with respect to an elementary domain-theoretic denotational semantics. Type soundness implies, relatively simply, the total correctness and logical consistency of our system. The relative ease with which we obtain both algorithmic and semantic results ultimately stems from the proof-theoretic technique of focalization.
A type- and scope-safe universe of syntaxes with binding: their semantics and proofs allais-2021-a
The syntax of almost every programming language includes a notion of binder and corresponding bound occurrences, along with the accompanying notions of α-equivalence, capture-avoiding substitution, typing contexts, runtime environments, and so on. In the past, implementing and reasoning about programming languages required careful handling to maintain the correct behaviour of bound variables. Modern programming languages include features that enable constraints like scope safety to be expressed in types. Nevertheless, the programmer is still forced to write the same boilerplate over again for each new implementation of a scope-safe operation (e.g., renaming, substitution, desugaring, printing), and then again for correctness proofs. We present an expressive universe of syntaxes with binding and demonstrate how to (1) implement scope-safe traversals once and for all by generic programming; and (2) how to derive properties of these traversals by generic proving. Our universe description, generic traversals and proofs, and our examples have all been formalised in Agda and are available in the accompanying material available online at https://github.com/gallais/generic-syntax .
Algorithmics bird-2021-algorithmics
First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory sterling_2021
The implementation and semantics of dependent type theories can be studied in a syntax-independent way: the objective metatheory of dependent type theories exploits the universal properties of their syntactic categories to endow them with computational content, mathematical meaning, and practical implementation (normalization, type checking, elaboration). The semantic methods of the objective metatheory inform the design and implementation of correct-by-construction elaboration algorithms, promising a principled interface between real proof assistants and ideal mathematics. In this dissertation, I add synthetic Tait computability to the arsenal of the objective metatheorist. Synthetic Tait computability is a mathematical machine to reduce difficult problems of type theory and programming languages to trivial theorems of topos theory. First employed by Sterling and Harper to reconstruct the theory of program modules and their phase separated parametricity, synthetic Tait computability is deployed here to resolve the last major open question in the syntactic metatheory of cubical type theory: normalization of open terms.
Type-and-scope safe programs and their proofs allais-2017-type
Observational equality, now! altenkirch-2007-observational
Cites 56 works (1 here)
With notes (1)
Elimination with a Motive mcbride-2002-elimination
External (55)
- Generic programming within dependently typed programming (2002)
- Views for recursion (2002)
- What do we gain by integrating a programming language with a theorem prover? (2002)
- Nested general recursion and partiality in type theory (2001)
- The Coq Proof Assistant Reference Manual (2001)
- First-order unification by structural recursion (2001)
- A predicative analysis of structural recursion (2000)
- Implementation techniques for inductive types in plastic (2000)
- Pattern guards and transformational patterns (2000)
- Dependently typed records for representing mathematical structure (2000)
- Monadic presentations of lambda-terms using generalized inductive types (1999)
- An exercise in dependent types: A well-typed interpreter (1999)
- de Bruijn notation as a nested datatype (1999)
- Domain specific embedded compilers (1999)
- Generalising techniques for type explanation (1999)
- Dependently Typed Functional Programs and their Proofs (1999)
- Some lambda calculus and type theory formalized (1999)
- Haskell’98: A Non-Strict Functional Language (1999)
- Cayenne—a language with dependent types (1998)
- Structural recursive definitions in type theory (1998)
- Inverting inductively defined relations in LEGO (1998)
- Dependent types in practical programming (1998)
- Conception d’un langage de haut niveau de répresentation de preuves (1997)
- The Definition of Standard ML, revised edn (1997)
- A new view of guards (1997)
- Views: An Extension to Haskell Pattern Matching (1996)
- The Theory of LEGO (1995)
- Codifying guarded definitions with recursive schemes (1994)
- A Typed Operational Semantics for Type Theory (1994)
- A groupoid model refutes uniqueness of identity proofs (1994)
- Computation and Reasoning: A Type Theory for Computer Science (1994)
- The implementation of ALF—A Proof Editor based on Martin-Löf ’s Monomorphic Type Theory with Explicit Substitution (1994)
- Incremental Changes in LEGO:1994 (1994)
- Pure Type Systems with definitions (1994)
- Checking algorithms for Pure Type Systems (1994)
- Pure type systems formalized (1993)
- Investigations into intensional type theory (1993)
- Lambda calculi with types (1992)
- Pattern matching with dependent types (1992)
- LEGO Proof Development System: User’s Manual (1992)
- Telescopic mappings in typed lambda-calculus (1991)
- Inductive sets and families in Martin-Löf’s Type Theory (1991)
- Type checking with universes (1991)
- Electronic Proceedings of the First Annual BRA Workshop on Logical Frameworks (Antibes, France) (1990)
- ECC: An Extended Calculus of Constructions (1990)
- Programming in Martin-Löf’s type theory: an introduction (1990)
- Deforestation: transforming programs to eliminate trees (1990)
- Theorems for Free! (1989)
- Views: A way for pattern matching to cohabit with data abstraction (1987)
- Compiling pattern matching (1985)
- Unfold/fold transformation of logic programs (1984)
- Negation as failure (1978)
- Lambda Calculus notation with nameless dummies: a tool for automatic formula manipulation (1972)
- Computer aided manipulation of symbols (1970)
- Proving properties of programs by structural induction (1969)