Hippogriff: a semantic approach to uniting core and modules

Abstract

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.