Skip to Main content Skip to Navigation
New interface

Which types have a unique inhabitant?: Focusing on pure program equivalence

Abstract : Some programming language features (coercions, type-classes, implicits) rely on inferring a part of the code that is determined by its usage context. In order to better understand the theoretical underpinnings of this mechanism, we ask: when is it the case that there is a *unique* program that could have been guessed, or in other words that all possible guesses result in equivalent program fragments? Which types have a unique inhabitant? To approach the question of unicity, we build on work in proof theory on more canonical representation of proofs. Using the proofs-as-programs correspondence, we can adapt the logical technique of focusing to obtain more canonical program representations. In the setting of simply-typed lambda-calculus with sums and the empty type, equipped with the strong beta-eta-equivalence, we show that uniqueness is decidable. We present a saturating focused logic that introduces irreducible cuts on positive types “as soon as possible”. Goal-directed proof search in this logic gives an effective algorithm that returns either zero, one or two distinct inhabitants for any given type.
Complete list of metadata
Contributor : Scherer Gabriel Connect in order to contact the contributor
Submitted on : Tuesday, December 27, 2016 - 4:03:45 AM
Last modification on : Thursday, February 3, 2022 - 11:16:48 AM
Long-term archiving on: : Tuesday, March 21, 2017 - 12:32:40 AM


Distributed under a Creative Commons Attribution - ShareAlike 4.0 International License


  • HAL Id : tel-01309712, version 2



Gabriel Scherer. Which types have a unique inhabitant?: Focusing on pure program equivalence. Programming Languages [cs.PL]. Université Paris-Diderot, 2016. English. ⟨NNT : ⟩. ⟨tel-01309712v2⟩



Record views


Files downloads