Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Conference papers

Which simple types have a unique inhabitant?

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [31 references]  Display  Hide  Download
Contributor : Scherer Gabriel Connect in order to contact the contributor
Submitted on : Monday, November 30, 2015 - 12:51:28 PM
Last modification on : Friday, February 4, 2022 - 3:08:12 AM
Long-term archiving on: : Saturday, April 29, 2017 - 3:41:10 AM


Files produced by the author(s)


  • HAL Id : hal-01235596, version 1



Gabriel Scherer, Didier Rémy. Which simple types have a unique inhabitant?. The 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015), Aug 2015, Vancouver, Canada. ⟨hal-01235596⟩



Record views


Files downloads