Name
Abstract | ||
|---|---|---|
We study the question of whether a given type has a unique inhabitant modulo program equivalence. In the setting of simply-typed lambda-calculus with sums, equipped with the strong --equivalence, we show that uniqueness is decidable. We present a saturating focused logic that introduces irreducible cuts on positive types ``as soon as possible''. Backward search in this logic gives an effective algorithm that returns either zero, one or two distinct inhabitants for any given type. Preliminary application studies show that such a feature can be useful in strongly-typed programs, inferring the code of highly-polymorphic library functions, or ``glue code'' inside more complex terms. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1145/2784731.2784757 | International Conf on Function Programming |
Keywords | Field | DocType |
Unique inhabitants,canonicity,code inference,focusing,proof search,saturation,simply-typed lambda-calculus,sums | Uniqueness,Proof search,Simply typed lambda calculus,Algebra,Computer science,Modulo,Algorithm,Decidability,Theoretical computer science,Equivalence (measure theory) | Conference |
Volume | Issue | ISSN |
50 | 9 | 0362-1340 |
Citations | PageRank | References |
3 | 0.47 | 31 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gabriel Scherer | 1 | 13 | 4.82 |
| Didier Rémy | 2 | 682 | 49.82 |