Data.Ten.Sigma

An approximation of a dependent pair type.

Documentation

data k :** m infixr 5

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.

Constructors

forall a. (k a) :** (m a) infixr 5

Instances

Foldable10 ((:**) k :: (Type -> Type) -> Type)

Defined in Data.Ten.Sigma

Methods

foldMap10 :: Monoid w => (forall (a :: k0). m a -> w) -> (k :** m) -> w

Functor10 ((:**) k :: (Type -> Type) -> Type)

Defined in Data.Ten.Sigma

Methods

fmap10 :: (forall (a :: k0). m a -> n a) -> (k :** m) -> k :** n

Functor10WithIndex ((:**) k :: (Type -> Type) -> Type)

Defined in Data.Ten.Sigma

Methods

imap10 :: (forall (a :: k0). Index10 ((:**) k) a -> m a -> n a) -> (k :** m) -> k :** n

Foldable10WithIndex ((:**) k :: (Type -> Type) -> Type)

Defined in Data.Ten.Sigma

Methods

ifoldMap10 :: Monoid w => (forall (a :: k0). Index10 ((:**) k) a -> m a -> w) -> (k :** m) -> w

Traversable10 ((:**) k :: (Type -> Type) -> Type)

Defined in Data.Ten.Sigma

Methods

mapTraverse10 :: forall f m n r. Applicative f => ((k :** n) -> r) -> (forall (a :: k0). m a -> f (n a)) -> (k :** m) -> f r

Traversable10WithIndex ((:**) k :: (Type -> Type) -> Type)

Defined in Data.Ten.Sigma

Methods

imapTraverse10 :: Applicative g => ((k :** n) -> r) -> (forall (a :: k0). Index10 ((:**) k) a -> m a -> g (n a)) -> (k :** m) -> g r

(GEq k, Entails k (Eq :!: m)) => Eq (k :** m)

Defined in Data.Ten.Sigma

Methods

(==) :: (k :** m) -> (k :** m) -> Bool

(/=) :: (k :** m) -> (k :** m) -> Bool

(forall a. Show (k a), Entails k (Show :!: m)) => Show (k :** m)

Defined in Data.Ten.Sigma

Methods

showsPrec :: Int -> (k :** m) -> ShowS

show :: (k :** m) -> String

showList :: [k :** m] -> ShowS

(forall a. NFData (k a), Entails k (NFData :!: m)) => NFData (k :** m)

Defined in Data.Ten.Sigma

Methods

rnf :: (k :** m) -> ()

(forall a. Portray (k a), Entails k (Portray :!: m)) => Portray (k :** m)

Defined in Data.Ten.Sigma

Methods

portray :: (k :** m) -> Portrayal

(TestEquality k, forall a. Portray (k a), forall a. Diff (k a), Entails k (Portray :!: m), Entails k (Diff :!: m)) => Diff (k :** m)

Defined in Data.Ten.Sigma

Methods

diff :: (k :** m) -> (k :** m) -> Maybe Portrayal

type Index10 ((:**) k :: (Type -> Type) -> Type)

Defined in Data.Ten.Sigma

type Index10 ((:**) k :: (Type -> Type) -> Type) = k

overFragment :: Update10 rec => (forall a. m a -> n a -> n a) -> (Rep10 rec :** m) -> rec n -> rec n

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.

lmapFragment :: forall recA recB m f. (Representable10 recA, Representable10 recB, f ~ OpCostar m (Rep10 recB :** m)) => (recB f -> recA f) -> (Rep10 recA :** m) -> Rep10 recB :** m

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.

eqKey :: GEq k => (k :** m) -> (k :** n) -> Bool

Check if two pairs have the same key.

newtype OpCostar f r a

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".

Constructors

OpCostar

Fields

• getOpCostar :: f a -> r

Instances

Functor f => Contravariant (OpCostar f r)

Defined in Data.Ten.Sigma

Methods

contramap :: (a -> b) -> OpCostar f r b -> OpCostar f r a

(>$) :: b -> OpCostar f r b -> OpCostar f r a

caseFragment :: Representable10 f => f (OpCostar m r) -> (Rep10 f :** m) -> r

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