Which simple types have a unique inhabitant

摘要: We study the question of whether a given type has unique inhabitant modulo program equivalence. In setting simply-typed lambda-calculus with sums, equipped strong --equivalence, we show that uniqueness is decidable. present saturating focused logic introduces irreducible cuts on positive types ``as soon as possible''. Backward search in this gives an effective algorithm returns either zero, one or two distinct inhabitants for any type. Preliminary application studies such feature can be useful strongly-typed programs, inferring code highly-polymorphic library functions, ``glue code'' inside more complex terms.