类型栖息

在类型理论（数理逻辑的一个分支）中，在一个给定的类型微积分中，这个微积分的类型栖息问题是如下问题：给定一个类型

在简单类型的λ微积分中，当且仅当一个类型的相应命题是最小隐含逻辑的同义反复时，它才有一个居民。同样地，当且仅当一个系统F类型的相应命题是直觉二阶逻辑的同义反复时，它才有一个居民。吉拉德悖论表明，类型的栖息地与具有库里-霍华德对应关系的类型系统的一致性密切相关。为了健全，这样的系统必须有无人居住的类型。

对于大多数类型计算，类型驻留问题是非常困难的。对于其他计算体，该问题甚至是不可解的。