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.
Type de document :
Communication dans un congrès
The 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015), Aug 2015, Vancouver, Canada. The 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015), 2015, 〈http://icfpconference.org/icfp2015/〉
Liste complète des métadonnées

Littérature citée [31 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01235596
Contributeur : Scherer Gabriel <>
Soumis le : lundi 30 novembre 2015 - 12:51:28
Dernière modification le : samedi 12 décembre 2015 - 01:05:56
Document(s) archivé(s) le : samedi 29 avril 2017 - 03:41:10

Fichiers

unique_stlc_sums.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01235596, version 1

Collections

Citation

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. The 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015), 2015, 〈http://icfpconference.org/icfp2015/〉. 〈hal-01235596〉

Partager

Métriques

Consultations de
la notice

106

Téléchargements du document

98