Documentation

A pair of k a and m a for any (existential) a.

This is a lot like a dependent pair, in that it contains a left-hand-side value that's meant to identify a type, and a right-hand-side parameterized by that type. For example, the true dependent pair type (in e.g. Idris) (n :: Nat ** Vec n Bool) could be approximated in Haskell as SInt :** Ap10 Bool Vec.

This can be used to represent one field of a Representable10, where k is set to Rep10 f. The k a identifies which field (and locks down its type), and the m a provides its value.

Zip a single field of a record with a (:**).

Since we're only operating on a single field, the n type can't vary like in a traditional zip function.

Convert a (:**) to a different key type contravariantly.

Example usage:

data MyRecord1 m = MyRecord1 { _mr1A :: Ap10 Int m, _mr1B :: Ap10 Int m } data MyRecord2 m = MyRecord2 { _mr2A :: Ap10 Int m }

• - Collapse both fields _mr1A and _mr1B onto _mr2A. example :: Rep10 MyRecord1 :** Identity
• > Rep10 MyRecord2 :** Identity example = lmapFragment $ MyRecord2{..} -> MyRecord1 { _mr1A = _mr2A , _mr1B = _mr2A }

It looks weird that the argument converts from recB to recA in order to convert (:**) the other way, so it merits some explanation: first, note that, by Representable10 recA, we know that recA m is isomorphic to forall a. Rep10 recA a -> m a. That is, Rep10 recA effectively appears in negative position in recA m. So, a function from recB to recA hand-wavingly contains a function in the opposite direction from Rep10 recA to Rep10 recB.

With the intuition out of the way, here's how we actually accomplish the conversion: start off with a record recB where each field is a function that trivially rebuilds the corresponding (:**) in each field with k :: Rep10 recB we literally just put (k :**) with the appropriate newtype constructors. Then, apply the user's contravariant conversion function, to turn our recB of recB-pair-builders into an recA of recB-pair-builders. If the user-provided conversion function involves changing any field types, it must have done so by contramapping the pair-builders: instead of a function that just directly applies (k :=) to its argument, they will now contain functions equivalent to ma -> k := _f ma. Finally, unpack the recA pair and use its k to fetch that field's recB-pair-builder (potentially with a conversion inserted at the front), and apply it to the payload.

Usage will typically involve applying contramap to some number of fields and leaving the rest unchanged. If you have a type-changing Setter at hand, it's probably easier to use fragmented.

Check if two pairs have the same key.

Newtype used in implementing contravariant conversion of Fragments. See lmapFragment. Only exported because it's used in the type of lmapFragment, but it can be largely ignored, like the many ALens etc. types in "lens".

Simulate a case statement on a (:**) with a record of functions.

    caseFragment (MyRecord1 (OpCostar isJust) (OpCostar isNothing)) x

Is analogous to (pseudo-code):

    case x of { (_mr1A :** mx) -> isJust mx; (_mr1B :** mx) -> isNothing mx }

This is just the action of Representable10 (whereby f m is isomorphic to forall a. Rep10 f a -> m a) plus some newtyping:

    f (OpCostar m r)                      ~=  (by Representable10)
    forall a. Rep10 f a -> OpCostar m r a ~=  (by newtype)
    forall a. Rep10 f a -> f a -> r       ~=  (by GADT constructor)
    Rep10 f :** m -> r