类型论中所有 Kind 实例的共同超类型是啥

Posted 2023-02-24

【中文标题】类型论中所有 Kind 实例的共同超类型是啥

【英文标题】：What is the common supertype of all instances of Kind in Type Theory类型论中所有 Kind 实例的共同超类型是什么

【发布时间】：2012-12-13 08:33:25

【问题描述】：

我正在尝试设计一个本体，例如可以使用 OWL 或 Topic Maps 定义，其中包括对 List[T] 等多态类型的支持，其中 T 是 Interval Kind In(Nothing, Any) 的类型参数和列表是函数种类 * -> *。最终，我想用足够详细和严谨的语义语言描述一个类型系统本体，它可以成为用相同语义语言编写的类型安全软件代码的基础。

考虑到这个目标，我试图找出种类的层次结构，其中类型、间隔种类和函数种类都是种类的实例。所有种类的共同“超类”有正式名称吗？我能想到的最好的术语是“Kind Instance”。这甚至是类型论中的一个有意义的概念吗？即使不是，我也需要这样一个概念来表达诸如（在主题地图术语中）“函数-参数-类型-约束关联有一个角色'允许类型'，其玩家必须是'种类实例'类型'"。

除此之外，我才刚刚开始为这个项目自学类型理论，在完成它之前我还有很多东西要学。我已经阅读了一些关于类型理论的 scala 相关论文，包括更高种类的泛型 (http://adriaanm.github.com/files/higher.pdf) 并开始通过 Scala 中的安全类型级抽象 ( http://adriaanm.github.com/files/scalina-final.pdf）和Type Constructor Polymorphism for Scala[pdf]。我对 Haskell 的熟悉程度不如 Scala，但我遇到了一些相关的论文，例如 System F with Type Equality Coercions[pdf]，我需要更深入地掌握 Haskell 才能理解。如果有人可以建议从初学者级别开始学习 Haskell 类型系统的阅读材料的进展，一直到广义代数数据类型等高级原理，那也将不胜感激。

最后，如果您知道任何现有的尝试用语义本体语言（如 OWL 或主题映射）来描述类型系统，或者如果您对如何做到这一点有任何建议，我也很想听听。

【参考方案1】：

没有比 Benjamin Pierce 的“类型和编程语言”更好的类型论介绍了。我认为上面的级别没有标准化的名称，但“排序”是一种常见的选择。另一种常见的选择是直接跳转到依赖类型，将层次结构展平，这样毕竟只有一个层次。在这种情况下（在处理逻辑内容通常不那么重要的日常编程语言时）要添加的一个常见类型规则是“Type : Type”规则，例如，3 : Int : Type : 类型 : 类型 : ...

【讨论】：

IIUC，具有依赖类型和Type : Type 规则，存在会导致类型检查器无限循环的程序——但因为这些程序必须非常努力，这不是每天都会发生的——因此，如果您考虑的是程序而不是证明，那么Type : Type 的简单性与其一致的替代方案相比可能值得牺牲。

您能否给我一个链接来解释“类型：类型”规则，并举例说明它在实践中的使用情况。此外，是否有某种方法可以防止或识别会导致无限循环的程序？这可能会成为我想到的应用程序中的一个安全问题，因为它会涉及执行由 3rd 方编写的代码。

@ChrisBarnett CoqArt 中有一些关于Type : Type 的讨论；谷歌也建议webcache.googleusercontent.com/search?q=cache:http://…。至于无限循环，我相信你知道停止问题。基本上，如果你需要检查终止，你唯一的希望就是写一些保守的东西，然后你不可避免地会排除一些有趣的程序。 Coq 和 Agda 有相当复杂的终止检查器，但即便如此，每个开发的某些部分都涉及证明类型检查器的满意程度，即事物终止。