Quels types ont un habitant unique ?: Focalisons-nous sur l'équivalence de programmes

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.Certaines constructions des langages de programmation permettent à un ordinateur de “deviner” des parties du programe que le programmeur humain aurait écrit. Pour mieux comprendre les fondements théoriques de cette opération, nous étudions le cas où la solution à cette devinette est unique, c'est-à-dire où tous les réponses possibles donnent des programmes équivalents. Quels types ont un habitant unique ?Pour étudier cette question, nous avons décidé de partir des travaux de théorie des preuves sur des représentations plus canoniques des termes de preuve. En utilisant la correspondance preuve-programme, nous pouvons adapter la technique logiuqe de “concentration“ (focusing) pour obtenir des représentations plus canoniques des programmes. Cela nécessite de porter une attention particulière à la façon dont cette technique préserve l'équivalence de programmes.Dans le cadre du lambda-calcul simplement typé avec des sommes et le type vide, muni de la βη-équivalence forte, nous montrons que la question de l'unicité est décidable. Nous présentons une logique concentrée saturée qui introduit des coupures irréductibles sur les types positifs “dès que possible”. La recherche en arrière dans cette logique donne un algorithme effectif qui fournit zéro, un ou deux habitants distincts pour tout type fourni en entrée