Generic constructors and eliminators from descriptions: type theory as a dependently typed internal DSL.

ABSTRACTDependently typed languages with an "open" type theory introduce new datatypes using an axiomatic approach. Each new datatype introduces axioms for constructing values of the datatype, and an elimination axiom (which we call the standard eliminator) for consuming such values. In a "closed" type theory a single introduction rule primitive and a single elimination rule primitive can be used for all datatypes, without adding axioms to the theory. We review a closed type theory, specified as an Agda program, that uses descriptions for datatype construction. Descriptions make datatype definitions first class values, but writing programs using such datatypes requires low-level understanding of how the datatypes are encoded in terms of descriptions. In this work we derive constructors and standard eliminators, by defining generic functions parameterized by a description. Our generic type theory constructions are defined as generic wrappers around the closed type theory primitives, which are themselves generic functions in the Agda model. Thus, we allow users to write programs in the model without understanding the details of the description-based encoding of datatypes, by using open type theory constructions as an internal domain-specific language (IDSL).