Dependent lenses

Dependent lenses
Nils Anders Danielsson
Draft, 2016. [pdf, accompanying code (may include more recent developments)]

Abstract

Very well-behaved lenses provide a convenient mechanism for defining setters and getters for nested records (among other things). However, they do not work very well for dependent records, in which one field's type can depend on the value of a previous field.

This paper discusses dependent lenses, a generalisation of ordinary lenses with better support for dependent records. It is shown that a certain notion of composition cannot be defined for such lenses (under certain assumptions), but that another, different notion of composition can be defined.