-
Coverage Semantics for Dependent Pattern Matching
Authors:
Joseph Eremondi,
Ohad Kammar
Abstract:
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…
▽ More
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.
△ Less
Submitted 29 January, 2025;
originally announced January 2025.
-
Strictly Monotone Brouwer Trees for Well-founded Recursion Over Multiple Arguments
Authors:
Joseph Eremondi
Abstract:
Ordinals can help prove termination for dependently typed programs. Brouwer trees are a particular ordinal notation that make it very easy to assign sizes to higher order data structures. They extend natural numbers with a limit constructor, so a function's size can be the supremum of the sizes of values from its image. These can then be used to define well-founded recursion: any recursive calls a…
▽ More
Ordinals can help prove termination for dependently typed programs. Brouwer trees are a particular ordinal notation that make it very easy to assign sizes to higher order data structures. They extend natural numbers with a limit constructor, so a function's size can be the supremum of the sizes of values from its image. These can then be used to define well-founded recursion: any recursive calls are allowed so long as they are on values whose sizes are strictly smaller than the current size. Unfortunately, Brouwer trees are not algebraically well-behaved. They can be characterized equationally as a join-semilattice, where the join takes the maximum of two trees. However, it does not interact well with the successor constructor, so it does not interact properly with the strict ordering used in well-founded recursion. We present Strictly Monotone Brouwer trees (SMB-trees), a refinement of Brouwer trees that are algebraically well-behaved. SMB-trees are built using functions with the same signatures as Brouwer tree constructors, and they satisfy all Brouwer tree inequalities. However, their join operator distributes over the successor, making them suited for well-founded recursion or equational reasoning. We show how, using dependent pairs and careful definitions, an ill-behaved definition can be turned into a well-behaved one, with light axiomatic requirements. We implement a recursively-defined maximum operator for Brouwer trees that matches on successors and handles them specifically. Then, we define SMB-trees as the subset of Brouwer trees for which the recursive maximum computes a least upper bound. Finally, we show that every Brouwer tree can be transformed into a corresponding SMB-tree by joining it with itself an infinite number of times. All definitions and theorems are implemented in Agda.
△ Less
Submitted 11 December, 2023;
originally announced December 2023.
-
Propositional Equality for Gradual Dependently Typed Programming
Authors:
Joseph Eremondi,
Ronald Garcia,
Éric Tanter
Abstract:
Gradual dependent types can help with the incremental adoption of dependently typed code by providing a principled semantics for imprecise types and proofs, where some parts have been omitted. Current theories of gradual dependent types, though, lack a central feature of type theory: propositional equality. Lennon-Bertrand et al. show that, when the reflexive proof $\mathit{refl}$ is the only clos…
▽ More
Gradual dependent types can help with the incremental adoption of dependently typed code by providing a principled semantics for imprecise types and proofs, where some parts have been omitted. Current theories of gradual dependent types, though, lack a central feature of type theory: propositional equality. Lennon-Bertrand et al. show that, when the reflexive proof $\mathit{refl}$ is the only closed value of an equality type, a gradual extension of CIC with propositional equality violates static observational equivalences. Extensionally-equal functions should be indistinguishable at run time, but the combination of equality and type imprecision allows for contexts that distinguish extensionally-equal but syntactically-different functions.
This work presents a gradually typed language that supports propositional equality. We avoid the above issues by devising an equality type where $\mathit{refl}$ is not the only closed inhabitant. Instead, each equality proof carries a term that is at least as precise as the equated terms, acting as a witness of their plausible equality. These witnesses track partial type information as a program runs, raising errors when that information shows that two equated terms are undeniably inconsistent. Composition of type information is internalized as a construct of the language, and is deferred for function bodies whose evaluation is blocked by variables. By deferring, we ensure that extensionally equal functions compose without error, thereby preventing contexts from distinguishing them. We describe the challenges of designing consistency and precision relations for this system, along with solutions to these challenges. Finally, we prove important metatheory: type-safety, conservative embedding of CIC, canonicity, and the gradual guarantees of Siek et al.
△ Less
Submitted 2 May, 2022;
originally announced May 2022.
-
Approximate Normalization and Eager Equality Checking for Gradual Inductive Families
Authors:
Joseph Eremondi,
Ronald Garcia,
Éric Tanter
Abstract:
Harnessing the power of dependently typed languages can be difficult. Programmers must manually construct proofs to produce well-typed programs, which is not an easy task. In particular, migrating code to these languages is challenging. Gradual typing can make dependently-typed languages easier to use by mixing static and dynamic checking in a principled way. With gradual types, programmers can in…
▽ More
Harnessing the power of dependently typed languages can be difficult. Programmers must manually construct proofs to produce well-typed programs, which is not an easy task. In particular, migrating code to these languages is challenging. Gradual typing can make dependently-typed languages easier to use by mixing static and dynamic checking in a principled way. With gradual types, programmers can incrementally migrate code to a dependently typed language.
However, adding gradual types to dependent types creates a new challenge: mixing decidable type-checking and incremental migration in a full-featured language is a precarious balance. Programmers expect type-checking to terminate, but dependent type-checkers evaluate terms at compile time, which is problematic because gradual types can introduce non-termination into an otherwise terminating language. Steps taken to mitigate this non-termination must not jeopardize the smooth transitions between dynamic and static.
We present a gradual dependently-typed language that supports inductive type families, has decidable type-checking, and provably supports smooth migration between static and dynamic, as codified by the refined criteria for gradual typing proposed by Siek et al. (2015). Like Eremondi et al. (2019), we use approximate normalization for terminating compile-time evaluation. Unlike Eremondi et al., our normalization does not require comparison of variables, allowing us to show termination with a syntactic model that accommodates inductive types. Moreover, we design a novel a technique for tracking constraints on type indices, so that dynamic constraint violations signal run-time errors eagerly. To facilitate these checks, we define an algebraic notion of gradual precision, axiomatizing certain semantic properties of gradual terms.
△ Less
Submitted 10 July, 2021;
originally announced July 2021.
-
Approximate Normalization for Gradual Dependent Types
Authors:
Joseph Eremondi,
Éric Tanter,
Ronald Garcia
Abstract:
Dependent types help programmers write highly reliable code. However, this reliability comes at a cost: it can be challenging to write new prototypes in (or migrate old code to) dependently-typed programming languages. Gradual typing makes static type disciplines more flexible, so an appropriate notion of gradual dependent types could fruitfully lower this cost. However, dependent types raise uniq…
▽ More
Dependent types help programmers write highly reliable code. However, this reliability comes at a cost: it can be challenging to write new prototypes in (or migrate old code to) dependently-typed programming languages. Gradual typing makes static type disciplines more flexible, so an appropriate notion of gradual dependent types could fruitfully lower this cost. However, dependent types raise unique challenges for gradual typing. Dependent typechecking involves the execution of program code, but gradually-typed code can signal runtime type errors or diverge. These runtime errors threaten the soundness guarantees that make dependent types so attractive, while divergence spoils the type-driven programming experience.
This paper presents GDTL, a gradual dependently-typed language that emphasizes pragmatic dependently-typed programming. GDTL fully embeds both an untyped and dependently-typed language, and allows for smooth transitions between the two. In addition to gradual types we introduce gradual terms , which allow the user to be imprecise in type indices and to omit proof terms; runtime checks ensure type safety . To account for nontermination and failure, we distinguish between compile-time normalization and run-time execution: compile-time normalization is approximate but total, while runtime execution is exact , but may fail or diverge. We prove that GDTL has decidable typechecking and satisfies all the expected properties of gradual languages. In particular, GDTL satisfies the static and dynamic gradual guarantees: reducing type precision preserves typedness, and altering type precision does not change program behavior outside of dynamic type failures. To prove these properties, we were led to establish a novel normalization gradual guarantee that captures the monotonicity of approximate normalization with respect to imprecision.
△ Less
Submitted 22 August, 2019; v1 submitted 15 June, 2019;
originally announced June 2019.
-
Set Constraints, Pattern Match Analysis, and SMT
Authors:
Joseph Eremondi
Abstract:
Set constraints provide a highly general way to formulate program analyses. However, solving arbitrary boolean combinations of set constraints is NEXPTIME-hard. Moreover, while theoretical algorithms to solve arbitrary set constraints exist, they are either too complex to realistically implement or too slow to ever run.
We present a translation that converts a set constraint formula into an SMT…
▽ More
Set constraints provide a highly general way to formulate program analyses. However, solving arbitrary boolean combinations of set constraints is NEXPTIME-hard. Moreover, while theoretical algorithms to solve arbitrary set constraints exist, they are either too complex to realistically implement or too slow to ever run.
We present a translation that converts a set constraint formula into an SMT problem. Our technique allows for arbitrary boolean combinations of set constraints, and leverages the performance of modern SMT solvers. To show the usefulness of unrestricted set constraints, we use them to devise a pattern match analysis for functional languages, which ensures that missing cases of pattern matches are always unreachable. We implement our analysis in the Elm compiler and show that our translation is fast enough to be used in practical verification.
△ Less
Submitted 1 March, 2020; v1 submitted 22 May, 2019;
originally announced May 2019.
-
Insertion Operations on Deterministic Reversal-Bounded Counter Machines
Authors:
Joey Eremondi,
Oscar H. Ibarra,
Ian McQuillan
Abstract:
Several insertion operations are studied applied to languages accepted by one-way and two-way deterministic reversal-bounded multicounter machines. These operations are defined by the ideals obtained from relations such as the prefix, infix, suffix, and outfix relations, as well as operations defined from inverses of a type of deterministic transducer with reversal-bounded counters attached. The q…
▽ More
Several insertion operations are studied applied to languages accepted by one-way and two-way deterministic reversal-bounded multicounter machines. These operations are defined by the ideals obtained from relations such as the prefix, infix, suffix, and outfix relations, as well as operations defined from inverses of a type of deterministic transducer with reversal-bounded counters attached. The question of whether the resulting languages can always be accepted by deterministic machines with the same number (or larger number) of input-turns (resp., counters, counter-reversals, etc.) is investigated.
△ Less
Submitted 8 March, 2019;
originally announced March 2019.
-
On the Density of Context-Free and Counter Languages
Authors:
Joey Eremondi,
Oscar H. Ibarra,
Ian McQuillan
Abstract:
A language $L$ is said to be dense if every word in the universe is an infix of some word in $L$. This notion has been generalized from the infix operation to arbitrary word operations $\varrho$ in place of the infix operation ($\varrho$-dense, with infix-dense being the standard notion of dense). It is shown here that it is decidable, for a language $L$ accepted by a one-way nondeterministic reve…
▽ More
A language $L$ is said to be dense if every word in the universe is an infix of some word in $L$. This notion has been generalized from the infix operation to arbitrary word operations $\varrho$ in place of the infix operation ($\varrho$-dense, with infix-dense being the standard notion of dense). It is shown here that it is decidable, for a language $L$ accepted by a one-way nondeterministic reversal-bounded pushdown automaton, whether $L$ is infix-dense. However, it becomes undecidable for both deterministic pushdown automata (with no reversal-bound), and for nondeterministic one-counter automata. When examining suffix-density, it is undecidable for more restricted families such as deterministic one-counter automata that make three reversals on the counter, but it is decidable with less reversals. Other decidability results are also presented on dense languages, and contrasted with a marked version called $\varrho$-marked-density. Also, new languages are demonstrated to be outside various deterministic language families after applying different deletion operations from smaller families. Lastly, bounded-dense languages are defined and examined.
△ Less
Submitted 7 March, 2019;
originally announced March 2019.
-
Deletion Operations on Deterministic Families of Automata
Authors:
Joey Eremondi,
Oscar H. Ibarra,
Ian McQuillan
Abstract:
Many different deletion operations are investigated applied to languages accepted by one-way and two-way deterministic reversal-bounded multicounter machines, deterministic pushdown automata, and finite automata. Operations studied include the prefix, suffix, infix and outfix operations, as well as left and right quotient with languages from different families. It is often expected that language f…
▽ More
Many different deletion operations are investigated applied to languages accepted by one-way and two-way deterministic reversal-bounded multicounter machines, deterministic pushdown automata, and finite automata. Operations studied include the prefix, suffix, infix and outfix operations, as well as left and right quotient with languages from different families. It is often expected that language families defined from deterministic machines will not be closed under deletion operations. However, here, it is shown that one-way deterministic reversal-bounded multicounter languages are closed under right quotient with languages from many different language families; even those defined by nondeterministic machines such as the context-free languages. Also, it is shown that when starting with one-way deterministic machines with one counter that makes only one reversal, taking the left quotient with languages from many different language families -- again including those defined by nondeterministic machines such as the context-free languages -- yields only one-way deterministic reversal-bounded multicounter languages (by increasing the number of counters). However, if there are two more reversals on the counter, or a second 1-reversal-bounded counter, taking the left quotient (or even just the suffix operation) yields languages that can neither be accepted by deterministic reversal-bounded multicounter machines, nor by 2-way nondeterministic machines with one reversal-bounded counter.
△ Less
Submitted 18 October, 2016; v1 submitted 4 July, 2016;
originally announced July 2016.
-
On the Complexity and Decidability of Some Problems Involving Shuffle
Authors:
Joey Eremondi,
Oscar H. Ibarra,
Ian McQuillan
Abstract:
The complexity and decidability of various decision problems involving the shuffle operation are studied. The following three problems are all shown to be $NP$-complete: given a nondeterministic finite automaton (NFA) $M$, and two words $u$ and $v$, is $L(M)$ not a subset of $u$ shuffled with $v$, is $u$ shuffled with $v$ not a subset of $L(M)$, and is $L(M)$ not equal to $u$ shuffled with $v$? It…
▽ More
The complexity and decidability of various decision problems involving the shuffle operation are studied. The following three problems are all shown to be $NP$-complete: given a nondeterministic finite automaton (NFA) $M$, and two words $u$ and $v$, is $L(M)$ not a subset of $u$ shuffled with $v$, is $u$ shuffled with $v$ not a subset of $L(M)$, and is $L(M)$ not equal to $u$ shuffled with $v$? It is also shown that there is a polynomial-time algorithm to determine, for $NFA$s $M_1, M_2$ and a deterministic pushdown automaton $M_3$, whether $L(M_1)$ shuffled with $L(M_2)$ is a subset of $L(M_3)$. The same is true when $M_1, M_2,M_3$ are one-way nondeterministic $l$-reversal-bounded $k$-counter machines, with $M_3$ being deterministic. Other decidability and complexity results are presented for testing whether given languages $L_1, L_2$ and $R$ from various languages families satisfy $L_1$ shuffled with $L_2$ is a subset of $R$, and $R$ is a subset of $L_1$ shuffled with $L_2$. Several closure results on shuffle are also shown.
△ Less
Submitted 7 March, 2019; v1 submitted 3 June, 2016;
originally announced June 2016.
