Programming languages with sufficiently expressive type theories provide users with essentially two levels of data ‘bundling’. This applies in particular to dependently-typed languages such as Agda, Coq, and Idris, where one can choose to make certain constituents of a record either parameters or fields. For example, we can speak of graphs /over/ a particular vertex set, or speak of arbitrary graphs wherein the vertex set is a component. These create isomorphic types, but differ with respect to convenience. Traditionally, a library designer would make this choice between parameters and fields; if a user wants a different variant, they are forced to build conversion utilities as well as duplicate functionality. In our earlier example about graph datatypes, if a library only provides a Haskell-like typeclass view of graphs /over/ a vertex set, yet a user wishes to work with the category of graphs, they must now package a vertex set as a component in a record along with a graph over that set.

We design and implement a language feature that allows both the library designer and the user to make the choice of information exposure only when necessary and otherwise leave the distinguishing line between parameters and fields unspecified. Our language feature is currently prototypically implemented as a meta-program that is not only easily incorporated into Agda’s Emacs ecosystem, but is also unobtrusive to Agda users.