Search papers, labs, and topics across Lattice.
This paper introduces Hippogriff, a language designed to unify syntax between core and module levels through a dependent type theory that supports modularity while maintaining general recursion. The authors establish a categorical semantics for dependent types, demonstrating that general recursion can be justified at the value level without compromising typechecking termination. The implementation, along with a Haskell version and an appendix detailing the type theory, provides a comprehensive framework for understanding the interplay between dependent and split-context type theories.
Hippogriff reveals a novel way to maintain general recursion in dependent type systems without sacrificing typechecking efficiency.
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.
