Documentation

The Select class provides a way to access subparts of a product type using a reified Selector. A Selector a b is essentially a function from a to b, and indeed select converts a Selector to such a function. However, unlike functions, Selectors can be compared for equality using GEq and ordered using GCompare.

This is useful to implement dependency tracking, since it’s possible to track in a reified form exactly which parts of a data structure are used.

Instances of Select can be automatically derived for record types (just define an empty instance). The instance uses the magical HasField constraints, and Selectors for the type can be written using OverloadedLabels.

The constant selector, which is useful for representing selectors into data structures where all fields have the same type. Matching on a value of type ConstS k a b causes a and b to unify, effectively “pinning” b to a.

A UniqueS is, as the name implies, a globally-unique Selector, which can be created using newUniqueS. If a value of type UniqueS a is found to be equal (via geq) with another value of type UniqueS b, then a and b must be the same type. This effectively allows the creation of a dynamically-extensible sum type, where new constructors can be created at runtime using newUniqueS.