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.

翻译：我们用语义解释来调查定义一个有约束量化的表达式但可分解的类型系统的问题。 在广泛研究的系统 Fsub 中进行输入检查是不可分解的, 这是由于一种不可分解的亚型关系, 罪魁祸首是分解约束量化规则的规则。 已经提出了这项规则的变弱版本, 允许分解亚型, 允许分解分解。 由此产生的一种类型系统( Kernel Fsub) 缺乏表达性, 另一种( System Fsubtop) 缺乏最小的打字属性, 因此没有明显的打字算法。 我们认为, 这些规则定义了不同形式的受约束的量化, 一种是解释类型变异的抽象, 另一种是描述类型即直线性, 使用类型快速的解析, 我们显示它们可以在单一的系统内存最小的打字属性, 简单的打字框程序。 我们认为, 这种统一型系统的碎块系统在类型中, 仅含有一定格式的易变式 Kirtical 。