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 metadatas

https://hal.inria.fr/tel-01309712
Contributor : Scherer Gabriel <>
Submitted on : Saturday, April 30, 2016 - 3:40:50 PM
Last modification on : Tuesday, November 20, 2018 - 11:06:03 PM
Long-term archiving on: Tuesday, May 24, 2016 - 4:00:01 PM

Licence


Distributed under a Creative Commons Attribution - ShareAlike 4.0 International License

Identifiers

  • HAL Id : tel-01309712, version 1

Collections

Citation

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

Share

Metrics

Record views

139

Files downloads

68