A Short Note on Collecting Dependently Typed Values

TL;DR

This paper introduces two dependently typed data structures, DList and PList, enabling collection of dependently typed values in a more concise and unified manner within dependently typed languages like Idris.

Contribution

The paper presents novel dependently typed data structures that simplify collecting dependently typed values, reducing verbosity and complexity in type-dependent collections.

Findings

DList and PList enable collection of dependently typed values.

These structures simplify the creation of complex inductive ADTs.

They improve code succinctness and expressiveness in dependently typed programming.

Abstract

Within dependently typed languages, such as Idris, types can depend on values. This dependency, however, can limit the collection of items in standard containers: all elements must have the same type, and as such their types must contain the same values. We present two dependently typed data structures for collecting dependent types: \texttt{DList} and \texttt{PList}. Use of these new data structures allow for the creation of single succinct inductive ADT whose constructions were previously verbose and split across many data structures.