AI 中文总结
本文提出名为Hippogriff的语言，其模块系统统一核心层与模块层语法，通过扩展二阶广义代数理论框架构建范畴语义以支撑值级一般递归，同时提供Haskell实现与类型理论附录。
AI 中文摘要
本文介绍Hippogriff，这是一种具有模块系统的语言，可统一核心层与模块层之间的语法。Hippogriff的类型理论是依存类型，其模块化特性通过小型类型的论域实现，同时Hippogriff仍支持一般递归，且不会使类型检查变为非终止。本文分为两部分：第一部分描述Hippogriff及其实现；第二部分构建用于支撑值级一般递归使用的依存类型的范畴语义，具体而言，我们对二阶广义代数理论框架进行扩展，以纳入综合阶段区分，这使我们能够在依存类型理论与分裂语境类型理论（如System F）之间建立数学联系。补充内容包括Hippogriff的Haskell实现，以及一份用带阶段区分的二阶广义代数理论描述Hippogriff完整类型理论的附录。
英文摘要
In this paper we introduce Hippogriff, a language with a module system that unifies syntax between the core level and the module level. Hippogriff's type theory is dependent, with modularity features enabled via a universe of small types, but Hippogriff still supports general recursion without making typechecking nonterminating. This paper contains two halves. In the first half, we describe Hippogriff and its implementation. In the second half, we build categorical semantics for our use of dependent types that justify the use of general recursion at the value level. Specifically, we use an extension of the second-order generalized algebraic theory framework to include a synthetic phase distinction, and this allows us to make a mathematical connection between dependent type theories and split-context type theories (like System F). Included as supplements are a Haskell implementation of Hippogriff and an appendix describing the full type theory of Hippogriff using a second-order generalized algebraic theory with phase distinction.
Comments36 pages, including supplemental appendix
