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中β-正规项类型检查的可判定性。