We use a semantic interpretation to investigate the problem of defining an expressive but decidable type system with bounded quantification. Typechecking in the widely studied System Fsub is undecidable thanks to an undecidable subtyping relation, for which the culprit is the rule for subtyping bounded quantification. Weaker versions of this rule, allowing decidable subtyping, have been proposed. One of the resulting type systems (Kernel Fsub) lacks expressiveness, another (System Fsubtop) lacks the minimal typing property and thus has no evident typechecking algorithm. We consider these rules as defining distinct forms of bounded quantification, one for interpreting type variable abstraction, and the other for type instantiation. By giving a semantic interpretation for both in terms of unbounded quantification, using the dinaturality of type instantiation with respect to subsumption, we show that they can coexist within a single type system. This does have the minimal typing property and thus a simple typechecking procedure. We consider the fragments of this unified type system over types which contain only one form of bounded quantifier. One of these is equivalent to Kernel Fsub, while the other can type strictly more terms than System Fsubtop but the same set of beta-normal terms. We show decidability of typechecking for this fragment, and thus for System Fsubtop typechecking of beta-normal terms.

翻译：我们使用语义解释来研究定义一种具有有界量化的表达力强且可判定的类型系统的问题。在广泛研究的System Fsub中，由于子类型关系的不可判定性（其根源在于有界量化的子类型规则），类型检查是不可判定的。已有研究提出了该规则的弱化版本，使得子类型可判定。由此产生的类型系统之一（Kernel Fsub）缺乏表达力，另一种（System Fsubtop）则缺少最小类型性质，因而没有明确的类型检查算法。我们将这些规则视为定义了不同形式的有界量化：一种用于解释类型变量抽象，另一种用于类型实例化。通过利用类型实例化关于子类型关系的自然性，以无界量化为两者给出语义解释，我们证明它们可以在单一类型系统中共存。该类型系统确实具有最小类型性质，因此拥有简单的类型检查过程。我们考虑该统一类型系统在仅包含一种有界量词的类型上的子片段。其中一个子片段等价于Kernel Fsub，而另一个可类型化的项严格多于System Fsubtop，但同样的β-正规项集合能被类型化。我们证明了该子片段类型检查的可判定性，进而也证明了System Fsubtop中β-正规项类型检查的可判定性。