我正在尝试设计一个本体，例如可以使用 OWL 或 Topic Maps 定义，其中包括对 List[T] 等多态类型的支持，其中 T 是 Interval Kind In(Nothing, Any) 的类型参数，List 是函数种类 * -> *. 最终，我想用足够详细和严谨的语义语言描述类型系统本体，它可以成为用相同语义语言编写的类型安全软件代码的基础。
考虑到这个目标，我试图找出种类的层次结构，其中类型、间隔种类和函数种类都是种类的实例。所有种类的共同“超类”有正式名称吗？我能想到的最好的术语是“Kind Instance”。这甚至是类型论中的一个有意义的概念吗？即使不是，我也需要这样一个概念来表达诸如（在主题地图术语中）“函数-参数-类型-约束关联有一个角色'允许类型'，其玩家必须是'种类实例'类型'”。
除此之外，我才刚刚开始为这个项目自学类型理论，在完成它之前我还有很多东西要学。我已经阅读了一些关于类型理论的与 scala 相关的论文，包括更高种类的泛型 (http://adriaanm.github.com/files/higher.pdf)，并开始通过 Scala 中的安全类型级抽象 ( http://adriaanm.github.com/files/scalina-final.pdf) 和Scala 的类型构造函数多态性[pdf]。我对 Haskell 的熟悉程度不如 Scala，但我遇到过一些相关的论文，例如System F with Type Equality Coercions[pdf]我需要更深入地掌握 Haskell 才能理解。如果有人可以建议从初学者级别开始学习 Haskell 类型系统的阅读材料的进展，一直到广义代数数据类型等高级原则，那也将不胜感激。
最后，如果您知道任何现有的尝试使用语义本体语言（如 OWL 或主题映射）来描述类型系统，或者您对如何做到这一点有任何建议，我也很想听听。