A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille

TL;DR

This paper explores higher-order abstract syntax within Cedille, a pure type theory system, and introduces a novel approach using Kripke function-spaces to derive a weakly initial algebra, enabling advanced inductive datatypes.

Contribution

It presents a new method for modeling HOAS in pure type theory by employing Kripke function-spaces to obtain a weakly initial algebra in Cedille.

Findings

Derived a weakly initial algebra for HOAS in Cedille.

Introduced Kripke function-spaces as an alternative to environment models.

Demonstrated examples of HOAS encoding in Cedille.

Abstract

Cedille is a relatively recent tool based on a Curry-style pure type theory, without a primitive datatype system. Using novel techniques based on dependent intersection types, inductive datatypes with their induction principles are derived. One benefit of this approach is that it allows exploration of new or advanced forms of inductive datatypes. This paper reports work in progress on one such form, namely higher-order abstract syntax (HOAS). We consider the nature of HOAS in the setting of pure type theory, comparing with the traditional concept of environment models for lambda calculus. We see an alternative, based on what we term Kripke function-spaces, for which we can derive a weakly initial algebra in Cedille. Several examples are given using the encoding.