LibNDT: Towards a Formal Library on Spreadable Properties over Linked Nested Datatypes

TL;DR

This paper introduces LibNDT, a formal library in Agda and Coq for spreadable properties over Linked Nested DataTypes, enabling formal reasoning about recursive polymorphic datatypes with practical applications.

Contribution

It presents a novel library for formal manipulation of spreadable properties over Linked Nested DataTypes in dependently typed languages.

Findings

LibNDT supports spreadable functions like folds and maps.

LibNDT models properties such as map congruence and predicate satisfaction.

The library is implemented in both Agda and Coq.

Abstract

Nested datatypes have been widely studied in the past 25 years, both theoretically using category theory, and practically in programming languages such as Haskell. They consist in recursive polymorphic datatypes where the type parameter changes throughout the recursion. They have a variety of applications such as modelling memory or modelling constraints over regular datatypes without relying on dependent types. In this work, we focus on a specific subset of nested datatypes which we call Linked Nested DataTypes (LNDT). We show that some usual datatypes such has List and Maybe, as well as some well-known nested datatypes such as Nest and even Bush can be built as various instances of LNDT. We proceed by presenting LibNDT, a library, developed both in Agda and Coq, which focuses on the set of constructs that can be spread directly from the parameter on which a LNDT is built, to the LNDT itself. These spreadable elements are of two kinds, functions, such as folds and map, and properties, such as the congruence of map or the satisfaction of a given predicate for at least one, or all, elements of the structure. We make use of the dependent type system of both Coq and Agda to model the latter. This paper ends with a discussion about various interesting topics that were raised throughout our development such as the issue of termination, the comparison of our tools and the proof effort required to extend LibNDT with additional elements.