-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Surgery for generic data types
--
-- Transform data types before passing them to generic functions.
@package generic-data-surgery
@version 0.3.0.0
-- | Operate on data types: insert/modify/delete fields and constructors.
module Generic.Data.Surgery.Internal
-- | A sterile Operating Room, where generic data comes to be
-- altered.
--
-- Generic representation in a simplified shape l at the type
-- level (reusing the constructors from GHC.Generics for
-- convenience). This representation makes it easy to modify fields and
-- constructors.
--
-- We may also refer to the representation l as a "row" of
-- constructors, if it represents a sum type, otherwise it is a "row" of
-- unnamed fields or record fields for single-constructor types.
--
-- x corresponds to the last parameter of Rep, and is
-- currently ignored by this module (no support for Generic1).
--
-- General sketch
--
--
-- toOR surgeries fromOR'
-- data MyType --------> OR (Rep MyType) ----------> OR alteredRep ---------> Data alteredRep
-- |
-- | myGenericFun :: Generic a => a -> a
-- fromOR surgeries toOR' v
-- data MyType <-------- OR (Rep MyType) <---------- OR alteredRep <--------- Data alteredRep
--
--
-- If instead myGenericFun is only a consumer of a
-- (resp. producer), then you only need the top half of the diagram
-- (resp. bottom half). For example, in aeson: genericToJSON
-- (consumer), genericParseJSON (producer).
newtype OR (l :: k -> Type) (x :: k)
OR :: l x -> OR
[unOR] :: OR -> l x
-- | Move fresh data to the Operating Room, where surgeries can be
-- applied.
--
-- Convert a generic type to a generic representation.
--
-- When inserting or removing fields, there may be a mismatch with
-- strict/unpacked fields. To work around this, you can switch to
-- toORLazy, if your operations don't care about dealing with a
-- normalized Rep (in which all the strictness annotations have
-- been replaced with lazy defaults).
--
-- Details
--
-- Type parameters
--
--
-- a :: Type -- Generic type
-- l :: k -> Type -- Generic representation (simplified)
-- x :: k -- Ignored
--
--
-- Functional dependencies
--
--
-- a -> l
--
toOR :: forall a l x. (Generic a, ToORRep a l) => a -> OR l x
-- | Move normalized data to the Operating Room, where surgeries can be
-- applied.
--
-- Convert a generic type to a generic representation, in which all the
-- strictness annotations have been normalized to lazy defaults.
--
-- This variant is useful when one needs to operate on fields whose
-- Rep has different strictness annotations than the ones used by
-- DefaultMetaSel.
--
-- Details
--
-- Type parameters
--
--
-- a :: Type -- Generic type
-- l :: k -> Type -- Generic representation (simplified and normalized)
-- x :: k -- Ignored
--
--
-- Functional dependencies
--
--
-- a -> l
--
toORLazy :: forall a l x. (Generic a, ToORRepLazy a l) => a -> OR l x
-- | Move altered data out of the Operating Room, to be consumed by
-- some generic function.
--
-- Convert a generic representation to a "synthetic" type that behaves
-- like a generic type.
--
-- Details
--
-- Type parameters
--
--
-- f :: k -> Type -- Generic representation (proper)
-- l :: k -> Type -- Generic representation (simplified)
-- x :: k -- Ignored
--
--
-- Functional dependencies
--
--
-- f -> l
-- l -> f
--
--
-- Implementation details
--
-- The synthesized representation is made of balanced binary trees,
-- corresponding closely to what GHC would generate for an actual data
-- type.
--
-- That structure assumed by at least one piece of code out there
-- (aeson).
fromOR' :: forall f l x. FromOR f l => OR l x -> Data f x
-- | Move altered data, produced by some generic function, to the
-- operating room.
--
-- The inverse of fromOR'.
--
-- Details
--
-- Type parameters
--
--
-- f :: k -> Type -- Generic representation (proper)
-- l :: k -> Type -- Generic representation (simplified)
-- x :: k -- Ignored
--
--
-- Functional dependencies
--
--
-- f -> l
-- l -> f
--
toOR' :: forall f l x. ToOR f l => Data f x -> OR l x
-- | Move restored data out of the Operating Room and back to the
-- real world.
--
-- The inverse of toOR.
--
-- It may be useful to annotate the output type of fromOR, since
-- the rest of the type depends on it and the only way to infer it
-- otherwise is from the context. The following annotations are possible:
--
--
-- fromOR :: OROf a -> a
-- fromOR @a -- with TypeApplications
--
--
-- When inserting or removing fields, there may be a mismatch with
-- strict/unpacked fields. To work around this, you can switch to
-- fromORLazy, if your operations don't care about dealing with a
-- normalized Rep (in which all the strictness annotations have
-- been replaced with lazy defaults).
--
-- Details
--
-- Type parameters
--
--
-- a :: Type -- Generic type
-- l :: k -> Type -- Generic representation (simplified)
-- x :: k -- Ignored
--
--
-- Functional dependencies
--
--
-- a -> l
--
fromOR :: forall a l x. (Generic a, FromORRep a l) => OR l x -> a
-- | Move normalized data out of the Operating Room and back to the
-- real world.
--
-- The inverse of toORLazy.
--
-- It may be useful to annotate the output type of fromORLazy,
-- since the rest of the type depends on it and the only way to infer it
-- otherwise is from the context. The following annotations are possible:
--
--
-- fromORLazy :: OROfLazy a -> a
-- fromORLazy @a -- with TypeApplications
--
--
-- Details
--
-- Type parameters
--
--
-- a :: Type -- Generic type
-- l :: k -> Type -- Generic representation (simplified and normalized)
-- x :: k -- Ignored
--
--
-- Functional dependencies
--
--
-- a -> l
--
fromORLazy :: forall a l x. (Generic a, FromORRepLazy a l) => OR l x -> a
-- | The simplified generic representation type of type a, that
-- toOR and fromOR convert to and from.
type OROf a = OR (Linearize (Rep a)) ()
-- | The simplified and normalized generic representation type of type
-- a, that toORLazy and fromORLazy convert to and
-- from.
type OROfLazy a = OR (Linearize (Lazify (Rep a))) ()
-- | This constraint means that a is convertible to its
-- simplified generic representation. Implies OROf a ~
-- OR l ().
type ToORRep a l = ToOR (Rep a) l
-- | This constraint means that a is convertible from its
-- simplified generic representation. Implies OROf a ~
-- OR l ().
type FromORRep a l = FromOR (Rep a) l
-- | Similar to ToORRep, but as a constraint on the standard generic
-- representation of a directly, f ~ Rep a.
type ToOR f l = (GLinearize f, Linearize f ~ l, f ~ Arborify l)
-- | Similar to FromORRep, but as a constraint on the standard
-- generic representation of a directly, f ~ Rep
-- a.
type FromOR f l = (GArborify f, Linearize f ~ l, f ~ Arborify l)
-- | This constraint means that a is convertible to its
-- simplified and normalized generic representation (i.e., with all its
-- strictness annotations normalized to lazy defaults). Implies
-- OROfLazy a ~ OR l ().
type ToORRepLazy a l = ToORLazy (Rep a) l
-- | This constraint means that a is convertible from its
-- simplified and normalized generic representation (i.e., with all its
-- strictness annotations normalized to lazy defaults). Implies
-- OROfLazy a ~ OR l ().
type FromORRepLazy a l = FromORLazy (Rep a) l
-- | Similar to FromLazyORRep, but as a constraint on the standard
-- generic representation of a directly, f ~ Rep
-- a.
type FromORLazy f l = (FromOR (Lazify f) l, Coercible (Arborify l) f)
-- | Similar to ToORRepLazy, but as a constraint on the standard
-- generic representation of a directly, f ~ Rep
-- a.
type ToORLazy f l = (ToOR (Lazify f) l, Coercible f (Arborify l))
-- | removeCField @n @t: remove the n-th field, of
-- type t, in a non-record single-constructor type.
--
-- Inverse of insertCField.
--
-- Details
--
-- Type parameters
--
--
-- n :: Nat -- Field position
-- t :: Type -- Field type
-- lt :: k -> Type -- Row with field
-- l :: k -> Type -- Row without field
-- x :: k -- Ignored
--
--
-- Signature
--
--
-- OR lt x -- Data with field
-- ->
-- (t, OR l x) -- Field value × Data without field
--
--
-- Functional dependencies
--
--
-- n lt -> t l
-- n t l -> lt
--
removeCField :: forall n t lt l x. RmvCField n t lt l => OR lt x -> (t, OR l x)
-- | removeRField @"fdName" @n @t: remove the field
-- fdName at position n of type t in a record
-- type.
--
-- Inverse of insertRField.
--
-- Details
--
-- Type parameters
--
--
-- fd :: Symbol -- Field name
-- n :: Nat -- Field position
-- t :: Type -- Field type
-- lt :: k -> Type -- Row with field
-- l :: k -> Type -- Row without field
-- x :: k -- Ignored
--
--
-- Signature
--
--
-- OR lt x -- Data with field
-- ->
-- (t, OR l x) -- Field value × Data without field
--
--
-- Functional dependencies
--
--
-- fd lt -> n t l
-- n lt -> fd t l
-- fd n t l -> lt
--
removeRField :: forall fd n t lt l x. RmvRField fd n t lt l => OR lt x -> (t, OR l x)
-- | insertCField @n @t: insert a field of type t
-- at position n in a non-record single-constructor type.
--
-- Inverse of removeCField.
--
-- Details
--
-- Type parameters
--
--
-- n :: Nat -- Field position
-- t :: Type -- Field type
-- lt :: k -> Type -- Row with field
-- l :: k -> Type -- Row without field
-- x :: k -- Ignored
--
--
-- Signature
--
--
-- (t, OR l x) -- Field value × Data without field
-- ->
-- OR lt x -- Data with field
--
--
-- Functional dependencies
--
--
-- n lt -> t l
-- n t l -> lt
--
insertCField :: forall n t lt l x. InsCField n t lt l => (t, OR l x) -> OR lt x
-- | Curried insertCField.
insertCField' :: forall n t lt l x. InsCField n t lt l => t -> OR l x -> OR lt x
-- | insertRField @"fdName" @n @t: insert a field named
-- fdName of type t at position n in a record
-- type.
--
-- Inverse of removeRField.
--
-- Details
--
-- Type parameters
--
--
-- fd :: Symbol -- Field name
-- n :: Nat -- Field position
-- t :: Type -- Field type
-- lt :: k -> Type -- Row with field
-- l :: k -> Type -- Row without field
-- x :: k -- Ignored
--
--
-- Signature
--
--
-- (t, OR l x) -- Field value × Data without field
-- ->
-- OR lt x -- Data with field
--
--
-- Functional dependencies
--
--
-- fd lt -> n t l
-- n lt -> fd t l
-- fd n t l -> lt
--
insertRField :: forall fd n t lt l x. InsRField fd n t lt l => (t, OR l x) -> OR lt x
-- | Curried insertRField.
insertRField' :: forall fd n t lt l x. InsRField fd n t lt l => t -> OR l x -> OR lt x
-- | modifyCField @n @t @t': modify the field at position
-- n in a non-record via a function f :: t -> t'
-- (changing the type of the field).
--
-- Details
--
-- Type parameters
--
--
-- n :: Nat -- Field position
-- t :: Type -- Initial field type
-- t' :: Type -- Final field type
-- lt :: k -> Type -- Row with initial field
-- lt' :: k -> Type -- Row with final field
-- l :: k -> Type -- Row without field
-- x :: k -- Ignored
--
--
-- Signature
--
--
-- (t -> t') -- Field modification
-- ->
-- OR lt x -- Data with field t
-- ->
-- OR lt' x -- Data with field t'
--
--
-- Functional dependencies
--
--
-- n lt -> t l
-- n lt' -> t' l
-- n t l -> lt
-- n t' l -> lt'
--
modifyCField :: forall n t t' lt lt' l x. ModCField n t t' lt lt' l => (t -> t') -> OR lt x -> OR lt' x
-- | modifyRField @"fdName" @n @t @t': modify the field
-- fdName at position n in a record via a function
-- f :: t -> t' (changing the type of the field).
--
-- Details
--
-- Type parameters
--
--
-- fd :: Symbol -- Field name
-- n :: Nat -- Field position
-- t :: Type -- Initial field type
-- t' :: Type -- Final field type
-- lt :: k -> Type -- Row with initial field
-- lt' :: k -> Type -- Row with final field
-- l :: k -> Type -- Row without field
-- x :: k -- Ignored
--
--
-- Signature
--
--
-- (t -> t') -- Field modification
-- ->
-- OR lt x -- Data with field t
-- ->
-- OR lt' x -- Data with field t'
--
--
-- Functional dependencies
--
--
-- fd lt -> n t l
-- fd lt' -> n t' l
-- n lt -> fd t l
-- n lt' -> fd t' l
-- fd n t l -> lt
-- fd n t' l -> lt'
--
modifyRField :: forall fd n t t' lt lt' l x. ModRField fd n t t' lt lt' l => (t -> t') -> OR lt x -> OR lt' x
-- | removeConstr @"C" @n @t: remove the n-th
-- constructor, named C, with contents isomorphic to the tuple
-- t.
--
-- Inverse of insertConstr.
--
-- Details
--
-- Type parameters
--
--
-- c :: Symbol -- Constructor name
-- t :: Type -- Tuple type to hold c's contents
-- n :: Nat -- Constructor position
-- lc :: k -> Type -- Row with constructor
-- l :: k -> Type -- Row without constructor
-- l_t :: k -> Type -- Field row of constructor c
-- x :: k -- Ignored
--
--
-- Signature
--
--
-- OR lc x -- Data with constructor
-- ->
-- Either t (OR l x) -- Constructor (as a tuple) | Data without constructor
--
--
-- Functional dependencies
--
--
-- c lc -> n l l_t
-- n lc -> c l l_t
-- c n l l_t -> lc
--
--
-- Note that there is no dependency to determine t.
removeConstr :: forall c n t lc l x. RmvConstr c n t lc l => OR lc x -> Either t (OR l x)
-- | A variant of removeConstr that can infer the tuple type
-- t to hold the contents of the removed constructor.
--
-- See removeConstr.
--
-- Details
--
-- Extra functional dependency
--
--
-- l_t -> t
--
removeConstrT :: forall c n t lc l x. RmvConstrT c n t lc l => OR lc x -> Either t (OR l x)
-- | insertConstr @"C" @n @t: insert a constructor
-- C at position n with contents isomorphic to the
-- tuple t.
--
-- Inverse of removeConstr.
--
-- Details
--
-- Type parameters
--
--
-- c :: Symbol -- Constructor name
-- t :: Type -- Tuple type to hold c's contents
-- n :: Nat -- Constructor position
-- lc :: k -> Type -- Row with constructor
-- l :: k -> Type -- Row without constructor
-- l_t :: k -> Type -- Field row of constructor c
-- x :: k -- Ignored
--
--
-- Signature
--
--
-- Either t (OR l x) -- Constructor (as a tuple) | Data without constructor
-- ->
-- OR lc x -- Data with constructor
--
--
-- Functional dependencies
--
--
-- c lc -> n l l_t
-- n lc -> c l l_t
-- c n l l_t -> lc
--
--
-- Note that there is no dependency to determine t.
insertConstr :: forall c n t lc l x. InsConstr c n t lc l => Either t (OR l x) -> OR lc x
-- | A variant of insertConstr that can infer the tuple type
-- t to hold the contents of the inserted constructor.
--
-- See insertConstr.
--
-- Details
--
-- Extra functional dependency
--
--
-- l_t -> t
--
insertConstrT :: forall c n t lc l x. InsConstrT c n t lc l => Either t (OR l x) -> OR lc x
-- | modifyConstr @"C" @n @t @t': modify the n-th
-- constructor, named C, with contents isomorphic to the tuple
-- t, to another tuple t'.
--
-- Details
--
-- Type parameters
--
--
-- c :: Symbol -- Constructor name
-- t :: Type -- Tuple type to hold c's initial contents
-- t' :: Type -- Tuple type to hold c's final contents
-- n :: Nat -- Constructor position
-- lc :: k -> Type -- Row with initial constructor
-- lc' :: k -> Type -- Row with final constructor
-- l :: k -> Type -- Row without constructor
-- l_t :: k -> Type -- Initial field row of constructor c
-- l_t' :: k -> Type -- Final field row of constructor c
-- x :: k -- Ignored
--
--
-- Signature
--
--
-- (t -> t') -- Constructor modification
-- ->
-- OR lc x -- Data with initial constructor
-- ->
-- OR lc' x -- Data with final constructor
--
--
-- Functional dependencies
--
--
-- c lc -> n l l_t
-- c lc' -> n l l_t'
-- n lc -> c l l_t
-- n lc' -> c l l_t'
-- c n l l_t -> lc
-- c n l l_t' -> lc'
--
--
-- Note that there is no dependency to determine t and
-- t'.
modifyConstr :: forall c n t t' lc lc' l x. ModConstr c n t t' lc lc' l => (t -> t') -> OR lc x -> OR lc' x
-- | A variant of modifyConstr that can infer the tuple types
-- t and t' to hold the contents of the inserted
-- constructor.
--
-- See modifyConstr.
--
-- Details
--
-- Extra functional dependencies
--
--
-- l_t -> t
-- l_t' -> t'
--
modifyConstrT :: forall c n t t' lc lc' l x. ModConstrT c n t t' lc lc' l => (t -> t') -> OR lc x -> OR lc' x
-- | This constraint means that the (unnamed) field row lt
-- contains a field of type t at position n, and
-- removing it yields row l.
type RmvCField n t lt l = (GRemoveField n t lt l, CFieldSurgery n t lt l)
-- | This constraint means that the record field row lt contains a
-- field of type t named fd at position n, and
-- removing it yields row l.
type RmvRField fd n t lt l = (GRemoveField n t lt l, RFieldSurgery fd n t lt l)
-- | This constraint means that inserting a field t at position
-- n in the (unnamed) field row l yields row
-- lt.
type InsCField n t lt l = (GInsertField n t l lt, CFieldSurgery n t lt l)
-- | This constraint means that inserting a field t named
-- fd at position n in the record field row l
-- yields row lt.
type InsRField fd n t lt l = (GInsertField n t l lt, RFieldSurgery fd n t lt l)
-- | This constraint means that modifying a field t to t'
-- at position n in the (unnamed) field row lt yields
-- row lt'. l is the row of fields common to
-- lt and lt'.
type ModCField n t t' lt lt' l = (RmvCField n t lt l, InsCField n t' lt' l)
-- | This constraint means that modifying a field t named
-- fd at position n to t' in the record field
-- row lt yields row lt'. l is the row of
-- fields common to lt and lt'.
type ModRField fd n t t' lt lt' l = (RmvRField fd n t lt l, InsRField fd n t' lt' l)
-- | This constraint means that the constructor row lc contains a
-- constructor named c at position n, and removing it
-- from lc yields row l. Furthermore, constructor
-- c contains a field row l_t compatible with the tuple
-- type t.
type RmvConstr c n t lc l = (GRemoveConstr n t lc l, ConstrSurgery c n t lc l (Eval (ConstrAt n lc)))
-- | A variant of RmvConstr allowing t to be inferred.
type RmvConstrT c n t lc l = (RmvConstr c n t lc l, IsTuple (Arity (Eval (ConstrAt n lc))) t)
-- | This constraint means that inserting a constructor c at
-- position n in the constructor row l yields row
-- lc. Furthermore, constructor c contains a field row
-- l_t compatible with the tuple type t.
type InsConstr c n (t :: Type) lc l = (GInsertConstr n t l lc, ConstrSurgery c n t lc l (Eval (ConstrAt n lc)))
-- | A variant of InsConstr allowing t to be inferred.
type InsConstrT c n t lc l = (InsConstr c n t lc l, IsTuple (Arity (Eval (ConstrAt n lc))) t)
-- | This constraint means that the constructor row lc contains a
-- constructor named c at position n of type isomorphic
-- to t, and modifying it to t' yields row
-- lc'.
type ModConstr c n t t' lc lc' l = (RmvConstr c n t lc l, InsConstr c n t' lc' l)
-- | A variant of ModConstr allowing t and t' to
-- be inferred.
type ModConstrT c n t t' lc lc' l = (ModConstr c n t t' lc lc' l, IsTuple (Arity (Eval (ConstrAt n lc))) t, IsTuple (Arity (Eval (ConstrAt n lc'))) t')
type FieldSurgery n t lt l = (t ~ Eval (FieldTypeAt n lt), l ~ Eval (RemoveField n t lt))
type CFieldSurgery n t lt l = (lt ~ Eval (InsertField n 'Nothing t l), FieldSurgery n t lt l)
type RFieldSurgery fd n t lt l = (n ~ Eval (FieldIndex fd lt), lt ~ Eval (InsertField n ( 'Just fd) t l), FieldSurgery n t lt l)
type ConstrSurgery c n t lc l l_t = (Generic t, MatchFields (Linearize (UnM1 (Rep t))) l_t, n ~ Eval (ConstrIndex c lc), c ~ MetaConsName (MetaOf l_t), lc ~ Eval (InsertUConstrAtL n l_t l), l ~ Eval (RemoveUConstrAt_ n lc))
type family Linearize (f :: k -> Type) :: k -> Type
type family LinearizeSum (f :: k -> Type) (tl :: k -> Type) :: k -> Type
type family LinearizeProduct (f :: k -> Type) (tl :: k -> Type) :: k -> Type
class GLinearize f
gLinearize :: GLinearize f => f x -> Linearize f x
class GLinearizeSum f tl
gLinearizeSum :: GLinearizeSum f tl => Either (f x) (tl x) -> LinearizeSum f tl x
class GLinearizeProduct f tl
gLinearizeProduct :: GLinearizeProduct f tl => f x -> tl x -> LinearizeProduct f tl x
class GArborify f
gArborify :: GArborify f => Linearize f x -> f x
class GArborifySum f tl
gArborifySum :: GArborifySum f tl => LinearizeSum f tl x -> Either (f x) (tl x)
class GArborifyProduct f tl
gArborifyProduct :: GArborifyProduct f tl => LinearizeProduct f tl x -> (f x, tl x)
type family Arborify (f :: k -> Type) :: k -> Type
data ArborifySum (n :: Nat) (f :: k -> Type) :: Exp (k -> Type)
data ArborifyProduct (n :: Nat) (f :: k -> Type) :: Exp (k -> Type)
type Arborify' arb op n nDiv2 f g = (Uncurry (Pure2 op) <=< Bimap (arb nDiv2) (arb (n - nDiv2)) <=< SplitAt nDiv2) (op f g)
type family Lazify (f :: k -> Type) :: k -> Type
type family LazifyMeta (m :: Meta) :: Meta
data SplitAt :: Nat -> (k -> Type) -> Exp (k -> Type, k -> Type)
-- | Kind of surgeries: operations on generic representations of types.
--
-- Treat this as an abstract kind (don't pay attention to its
-- definition).
--
-- Implementation details
--
-- The name Surgery got taken first by generic-data.
--
-- k is the kind of the extra parameter reserved for
-- Generic1, which we just don't use.
type MajorSurgery k = MajorSurgery_ k
-- | Operate f s. Apply a surgery s to a generic
-- representation f (e.g., f = Rep a for some
-- Generic type a).
--
-- The first argument is the generic representation; the second argument
-- is the surgery, which typically has the more complex syntax, which is
-- why this reverse application order was chosen.
type Operate (f :: k -> Type) (s :: MajorSurgery k) = Operate_ f s
-- | Internal definition of MajorSurgery.
type MajorSurgery_ k = (k -> Type) -> Exp (k -> Type)
-- | Internal definition of Operate.
type Operate_ (f :: k -> Type) (s :: MajorSurgery k) = Arborify (OperateL (Linearize f) s)
-- | Apply a surgery s to a linearized generic representation
-- l.
type OperateL (l :: k -> Type) (s :: MajorSurgery k) = Eval (s l)
-- | Composition of surgeries (left-to-right).
--
-- Note
--
-- Surgeries work on normalized representations, so Operate, which
-- applies a surgery to a generic representation, inserts normalization
-- steps before and after the surgery. This means that Operate
-- r (s1 :>> s2) is not quite the same as
-- Operate (Operate r s1) s2. Instead, the latter
-- is equivalent to Operate r (s1 :>>
-- Suture :>> s2), where Suture inserts
-- some intermediate normalization steps.
data (:>>) :: MajorSurgery k -> MajorSurgery k -> MajorSurgery k
infixl 1 :>>
-- | The identity surgery: doesn't do anything.
data IdSurgery :: MajorSurgery k
-- | Use this if a patient ever needs to go out and back into the operating
-- room, when it's not just to undo the surgery up to that point.
data Suture :: MajorSurgery k
type family PerformL (l :: k -> Type) (s :: MajorSurgery k) :: Constraint
-- | A constraint Perform r s means that the surgery s
-- can be applied to the generic representation r.
class Perform_ r s => Perform (r :: k -> Type) (s :: MajorSurgery k)
type Perform_ (r :: k -> Type) (s :: MajorSurgery k) = (PerformL (Linearize r) s, ToOR r (Linearize r), FromOR (Operate r s) (OperateL (Linearize r) s))
data FieldTypeAt (n :: Nat) (f :: k -> Type) :: Exp Type
type family FieldTypeOf (f :: k -> Type) :: Type
data FieldNameAt (n :: Nat) (f :: k -> Type) :: Exp (Maybe Symbol)
data FieldNameOf (f :: k -> Type) :: Exp (Maybe Symbol)
data RemoveField (n :: Nat) (a :: Type) :: MajorSurgery k
-- | Like RemoveField but without the explicit field type.
data RemoveField_ (n :: Nat) :: MajorSurgery k
data RemoveFieldAt (n :: Nat) (fd :: Maybe Symbol) (a :: Type) :: MajorSurgery k
type PerformLRemoveFieldAt_ n fd t lt l = (GRemoveField n t lt l, t ~ Eval (FieldTypeAt n lt), lt ~ Eval (InsertField n fd t l))
class PerformLRemoveFieldAt_ n fd t lt l => PerformLRemoveFieldAt n fd t lt l
data RemoveRField (fd :: Symbol) (a :: Type) :: MajorSurgery k
type DefaultMetaSel field = 'MetaSel field 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy
data InsertField (n :: Nat) (fd :: Maybe Symbol) (t :: Type) :: MajorSurgery k
type PerformLInsert_ n fd t l tl = (GInsertField n t l tl, l ~ Eval (RemoveField_ n tl), tl ~ Eval (InsertField n fd t l), CheckField n fd tl, t ~ Eval (FieldTypeAt n tl))
class PerformLInsert_ n fd t l tl => PerformLInsert n fd t l tl
type family CheckField (n :: Nat) (fd :: Maybe Symbol) (tl :: k -> Type) :: Constraint
data Succ :: Nat -> Exp Nat
-- | Position of a record field
data FieldIndex (field :: Symbol) (f :: k -> Type) :: Exp Nat
-- | Number of fields of a single constructor
type family Arity (f :: k -> Type) :: Nat
-- | Number of constructors of a data type
type family CoArity (f :: k -> Type) :: Nat
class GRemoveField (n :: Nat) a f g
gRemoveField :: GRemoveField n a f g => f x -> (a, g x)
class GInsertField (n :: Nat) a f g
gInsertField :: GInsertField n a f g => a -> f x -> g x
data ConstrAt (n :: Nat) (f :: k -> Type) :: Exp (k -> Type)
data RemoveConstr (c :: Symbol) (t :: Type) :: MajorSurgery k
type PerformLRemoveConstr lc c n (t :: Type) = PerformLRemoveConstrAt c n t (Eval (ConstrAt n lc)) lc (Eval (RemoveUConstrAt_ n lc))
type PerformLRemoveConstrAt_ c n t l_t lc l = (GRemoveConstr n t lc l, c ~ MetaConsName (MetaOf l_t), lc ~ Eval (InsertUConstrAtL n l_t l), MatchFields (Linearize (UnM1 (Rep t))) l_t, Arity l_t ~ Arity (Linearize (UnM1 (Rep t))))
class PerformLRemoveConstrAt_ c n t l_t lc l => PerformLRemoveConstrAt c n (t :: Type) l_t lc l
data RemoveConstrAt (c :: Symbol) (n :: Nat) (t :: Type) :: MajorSurgery k
data RemoveUConstrAt (n :: Nat) (t :: Type) :: MajorSurgery k
-- | Like RemoveConstr, but without the explicit constructor type.
data RemoveUConstrAt_ (n :: Nat) :: MajorSurgery k
-- | This is polymorphic to allow different ways of specifying the inserted
-- constructor.
--
-- If sym (the kind of the constructor name c) is:
--
--
-- - Symbol: treat it like a regular prefix constructor.
-- - TODO Infix constructors and their fixities.
--
--
-- t must be a single-constructor type, then we reuse its
-- generic representation for the new constructor, only replacing its
-- constructor name with c.
data InsertConstrAt (c :: sym) (n :: Nat) (t :: ty) :: MajorSurgery k
type family ConGraft (c :: sym) (t :: ty) :: k -> Type
type family RenameCon (c :: sym) (t :: k -> Type) :: k -> Type
type family RenameMeta (c :: sym) (m :: Meta) :: Meta
type PerformLInsertConstrAt0 l c n t = PerformLInsertConstrAt c n t (ConGraft c t) l (Eval (InsertUConstrAtL n (ConGraft c t) l))
type PerformLInsertConstrAt_ c n t l_t l lc = (GInsertConstr n t l lc, c ~ MetaConsName (MetaOf l_t), n ~ (ConstrIndex c @@ lc), l_t ~ (ConstrAt n @@ lc), l ~ Eval (RemoveUConstrAt_ n lc), MatchFields (Linearize (UnM1 (Rep t))) l_t)
class PerformLInsertConstrAt_ c n t l_t l lc => PerformLInsertConstrAt c n t l_t l lc
data InsertUConstrAt (n :: Nat) (t :: Type) :: MajorSurgery k
data InsertUConstrAtL (n :: Nat) (t :: k -> Type) :: MajorSurgery k
data ConstrIndex (con :: Symbol) (f :: k -> Type) :: Exp Nat
class GRemoveConstr (n :: Nat) (t :: Type) f g
gRemoveConstr :: GRemoveConstr n t f g => f x -> Either t (g x)
type ConstrArborify t l = (Generic t, Coercible (UnM1 (Rep t)) (Rep t), GArborify (UnM1 (Rep t)), Coercible l (Linearize (UnM1 (Rep t))))
constrArborify' :: forall t l x. ConstrArborify t l => l x -> t
class GInsertConstr (n :: Nat) (t :: Type) f g
gInsertConstr :: GInsertConstr n t f g => Either t (f x) -> g x
type ConstrLinearize t l = (Generic t, Coercible (Rep t) (UnM1 (Rep t)), GLinearize (UnM1 (Rep t)), Coercible (Linearize (UnM1 (Rep t))) l)
constrLinearize' :: forall t l x. ConstrLinearize t l => t -> l x
-- | Equate two generic representations, but ignoring constructor and field
-- metadata.
class MatchFields (f :: k -> Type) (g :: k -> Type)
class IsTuple (n :: Nat) (t :: k)
instance (t Data.Type.Equality.~ ()) => Generic.Data.Surgery.Internal.IsTuple 0 t
instance (t Data.Type.Equality.~ Data.Functor.Identity.Identity a) => Generic.Data.Surgery.Internal.IsTuple 1 t
instance (t Data.Type.Equality.~ (a, b)) => Generic.Data.Surgery.Internal.IsTuple 2 t
instance (t Data.Type.Equality.~ (a, b, c)) => Generic.Data.Surgery.Internal.IsTuple 3 t
instance (t Data.Type.Equality.~ (a, b, c, d)) => Generic.Data.Surgery.Internal.IsTuple 4 t
instance (t Data.Type.Equality.~ (a, b, c, d, e)) => Generic.Data.Surgery.Internal.IsTuple 5 t
instance (t Data.Type.Equality.~ (a, b, c, d, e, f)) => Generic.Data.Surgery.Internal.IsTuple 6 t
instance (t Data.Type.Equality.~ (a, b, c, d, e, f, g)) => Generic.Data.Surgery.Internal.IsTuple 7 t
instance Generic.Data.Surgery.Internal.PerformLRemoveConstrAt_ c n t l_t lc l => Generic.Data.Surgery.Internal.PerformLRemoveConstrAt c n t l_t lc l
instance Generic.Data.Surgery.Internal.PerformLInsertConstrAt_ c n t l_t l lc => Generic.Data.Surgery.Internal.PerformLInsertConstrAt c n t l_t l lc
instance forall k (g :: k -> *) (c :: GHC.Generics.Meta) (g' :: k -> *) (f' :: k -> *). (g Data.Type.Equality.~ GHC.Generics.M1 GHC.Generics.D c g', Generic.Data.Surgery.Internal.MatchFields f' g') => Generic.Data.Surgery.Internal.MatchFields (GHC.Generics.M1 GHC.Generics.D c f') g
instance forall k (g :: k -> *) (_x :: GHC.Types.Symbol) (_y :: GHC.Generics.FixityI) (_z :: GHC.Types.Bool) (g' :: k -> *) (f' :: k -> *) (c :: GHC.Generics.Meta). (g Data.Type.Equality.~ GHC.Generics.M1 GHC.Generics.C ('GHC.Generics.MetaCons _x _y _z) g', Generic.Data.Surgery.Internal.MatchFields f' g') => Generic.Data.Surgery.Internal.MatchFields (GHC.Generics.M1 GHC.Generics.C c f') g
instance forall k (g :: k -> *) (_w :: GHC.Maybe.Maybe GHC.Types.Symbol) (_x :: GHC.Generics.SourceUnpackedness) (_y :: GHC.Generics.SourceStrictness) (_z :: GHC.Generics.DecidedStrictness) (g' :: k -> *) (f' :: k -> *) (c :: GHC.Generics.Meta). (g Data.Type.Equality.~ GHC.Generics.M1 GHC.Generics.S ('GHC.Generics.MetaSel _w _x _y _z) g', Generic.Data.Surgery.Internal.MatchFields f' g') => Generic.Data.Surgery.Internal.MatchFields (GHC.Generics.M1 GHC.Generics.S c f') g
instance forall k (g :: k -> *) (g1 :: k -> *) (g2 :: k -> *) (f1 :: k -> *) (f2 :: k -> *). (g Data.Type.Equality.~ (g1 GHC.Generics.:+: g2), Generic.Data.Surgery.Internal.MatchFields f1 g1, Generic.Data.Surgery.Internal.MatchFields f2 g2) => Generic.Data.Surgery.Internal.MatchFields (f1 GHC.Generics.:+: f2) g
instance forall k (g :: k -> *) (g1 :: k -> *) (g2 :: k -> *) (f1 :: k -> *) (f2 :: k -> *). (g Data.Type.Equality.~ (g1 GHC.Generics.:*: g2), Generic.Data.Surgery.Internal.MatchFields f1 g1, Generic.Data.Surgery.Internal.MatchFields f2 g2) => Generic.Data.Surgery.Internal.MatchFields (f1 GHC.Generics.:*: f2) g
instance forall k (g :: k -> *) i a. (g Data.Type.Equality.~ GHC.Generics.K1 i a) => Generic.Data.Surgery.Internal.MatchFields (GHC.Generics.K1 i a) g
instance forall k (g :: k -> *). (g Data.Type.Equality.~ GHC.Generics.U1) => Generic.Data.Surgery.Internal.MatchFields GHC.Generics.U1 g
instance forall k (g :: k -> *). (g Data.Type.Equality.~ GHC.Generics.V1) => Generic.Data.Surgery.Internal.MatchFields GHC.Generics.V1 g
instance Generic.Data.Surgery.Internal.ConstrLinearize t l => Generic.Data.Surgery.Internal.GInsertConstr 0 t f (l GHC.Generics.:+: f)
instance forall k (n :: GHC.Types.Nat) t (f :: k -> *) (g :: k -> *) i (c :: GHC.Generics.Meta). Generic.Data.Surgery.Internal.GInsertConstr n t f g => Generic.Data.Surgery.Internal.GInsertConstr n t (GHC.Generics.M1 i c f) (GHC.Generics.M1 i c g)
instance forall k (n :: GHC.Types.Nat) t (f :: k -> *) (g :: k -> *) (f0f :: k -> *) (f0 :: k -> *). (Generic.Data.Surgery.Internal.GInsertConstr (n GHC.TypeNats.- 1) t f g, (n Data.Type.Equality.== 0) Data.Type.Equality.~ 'GHC.Types.False, f0f Data.Type.Equality.~ (f0 GHC.Generics.:+: f)) => Generic.Data.Surgery.Internal.GInsertConstr n t f0f (f0 GHC.Generics.:+: g)
instance Generic.Data.Surgery.Internal.ConstrArborify t l => Generic.Data.Surgery.Internal.GRemoveConstr 0 t (l GHC.Generics.:+: f) f
instance forall k (n :: GHC.Types.Nat) t (f :: k -> *) (g :: k -> *) i (c :: GHC.Generics.Meta). Generic.Data.Surgery.Internal.GRemoveConstr n t f g => Generic.Data.Surgery.Internal.GRemoveConstr n t (GHC.Generics.M1 i c f) (GHC.Generics.M1 i c g)
instance forall k (n :: GHC.Types.Nat) t (f :: k -> *) (g :: k -> *) (f0g :: k -> *) (f0 :: k -> *). (Generic.Data.Surgery.Internal.GRemoveConstr (n GHC.TypeNats.- 1) t f g, (n Data.Type.Equality.== 0) Data.Type.Equality.~ 'GHC.Types.False, f0g Data.Type.Equality.~ (f0 GHC.Generics.:+: g)) => Generic.Data.Surgery.Internal.GRemoveConstr n t (f0 GHC.Generics.:+: f) f0g
instance forall k (n :: GHC.Types.Nat) (fd :: GHC.Maybe.Maybe GHC.Types.Symbol) t (l :: k -> *) (tl :: k -> *). Generic.Data.Surgery.Internal.PerformLInsert_ n fd t l tl => Generic.Data.Surgery.Internal.PerformLInsert n fd t l tl
instance forall k (n :: GHC.Types.Nat) a (f :: k -> *) (g :: k -> *) i (c :: GHC.Generics.Meta). Generic.Data.Surgery.Internal.GInsertField n a f g => Generic.Data.Surgery.Internal.GInsertField n a (GHC.Generics.M1 i c f) (GHC.Generics.M1 i c g)
instance forall k (n :: GHC.Types.Nat) a (f :: k -> *) (g :: k -> *). Generic.Data.Surgery.Internal.GInsertField n a f g => Generic.Data.Surgery.Internal.GInsertField n a (f GHC.Generics.:+: GHC.Generics.V1) (g GHC.Generics.:+: GHC.Generics.V1)
instance forall k a (f :: k -> *) s (m :: GHC.Generics.Meta) i. Generic.Data.Surgery.Internal.GInsertField 0 a f (GHC.Generics.M1 s m (GHC.Generics.K1 i a) GHC.Generics.:*: f)
instance forall k (n :: GHC.Types.Nat) (f0f :: k -> *) (f0 :: k -> *) (f :: k -> *) a (g :: k -> *). ((n Data.Type.Equality.== 0) Data.Type.Equality.~ 'GHC.Types.False, f0f Data.Type.Equality.~ (f0 GHC.Generics.:*: f), Generic.Data.Surgery.Internal.GInsertField (n GHC.TypeNats.- 1) a f g) => Generic.Data.Surgery.Internal.GInsertField n a f0f (f0 GHC.Generics.:*: g)
instance forall k (n :: GHC.Types.Nat) (fd :: GHC.Maybe.Maybe GHC.Types.Symbol) t (lt :: k -> *) (l :: k -> *). Generic.Data.Surgery.Internal.PerformLRemoveFieldAt_ n fd t lt l => Generic.Data.Surgery.Internal.PerformLRemoveFieldAt n fd t lt l
instance forall k (n :: GHC.Types.Nat) a (f :: k -> *) (g :: k -> *) i (c :: GHC.Generics.Meta). Generic.Data.Surgery.Internal.GRemoveField n a f g => Generic.Data.Surgery.Internal.GRemoveField n a (GHC.Generics.M1 i c f) (GHC.Generics.M1 i c g)
instance forall k (n :: GHC.Types.Nat) a (f :: k -> *) (g :: k -> *). Generic.Data.Surgery.Internal.GRemoveField n a f g => Generic.Data.Surgery.Internal.GRemoveField n a (f GHC.Generics.:+: GHC.Generics.V1) (g GHC.Generics.:+: GHC.Generics.V1)
instance forall k a s (m :: GHC.Generics.Meta) i (f :: k -> *). Generic.Data.Surgery.Internal.GRemoveField 0 a (GHC.Generics.M1 s m (GHC.Generics.K1 i a) GHC.Generics.:*: f) f
instance forall k (n :: GHC.Types.Nat) (f0g :: k -> *) (f0 :: k -> *) (g :: k -> *) a (f :: k -> *). ((n Data.Type.Equality.== 0) Data.Type.Equality.~ 'GHC.Types.False, f0g Data.Type.Equality.~ (f0 GHC.Generics.:*: g), Generic.Data.Surgery.Internal.GRemoveField (n GHC.TypeNats.- 1) a f g) => Generic.Data.Surgery.Internal.GRemoveField n a (f0 GHC.Generics.:*: f) f0g
instance forall k (r :: k -> *) (s :: Generic.Data.Surgery.Internal.MajorSurgery k). Generic.Data.Surgery.Internal.Perform_ r s => Generic.Data.Surgery.Internal.Perform r s
instance forall k (f :: k -> *) (m :: GHC.Generics.Meta). Generic.Data.Surgery.Internal.GArborifyProduct f GHC.Generics.U1 => Generic.Data.Surgery.Internal.GArborify (GHC.Generics.M1 GHC.Generics.C m f)
instance forall k (f :: k -> *) c (m :: GHC.Generics.Meta) (tl :: k -> *). Generic.Data.Surgery.Internal.GArborifyProduct f GHC.Generics.U1 => Generic.Data.Surgery.Internal.GArborifySum (GHC.Generics.M1 c m f) tl
instance forall k (tl :: k -> *). Generic.Data.Surgery.Internal.GArborifyProduct GHC.Generics.U1 tl
instance forall k (g :: k -> *) (tl :: k -> *) (f :: k -> *). (Generic.Data.Surgery.Internal.GArborifyProduct g tl, Generic.Data.Surgery.Internal.GArborifyProduct f (Generic.Data.Surgery.Internal.LinearizeProduct g tl)) => Generic.Data.Surgery.Internal.GArborifyProduct (f GHC.Generics.:*: g) tl
instance forall k s (m :: GHC.Generics.Meta) (f :: k -> *) (tl :: k -> *). Generic.Data.Surgery.Internal.GArborifyProduct (GHC.Generics.M1 s m f) tl
instance forall k (f :: k -> *) (m :: GHC.Generics.Meta). Generic.Data.Surgery.Internal.GArborifySum f GHC.Generics.V1 => Generic.Data.Surgery.Internal.GArborify (GHC.Generics.M1 GHC.Generics.D m f)
instance forall k (tl :: k -> *). Generic.Data.Surgery.Internal.GArborifySum GHC.Generics.V1 tl
instance forall k (g :: k -> *) (tl :: k -> *) (f :: k -> *). (Generic.Data.Surgery.Internal.GArborifySum g tl, Generic.Data.Surgery.Internal.GArborifySum f (Generic.Data.Surgery.Internal.LinearizeSum g tl)) => Generic.Data.Surgery.Internal.GArborifySum (f GHC.Generics.:+: g) tl
instance forall k (f :: k -> *) (m :: GHC.Generics.Meta). Generic.Data.Surgery.Internal.GLinearizeProduct f GHC.Generics.U1 => Generic.Data.Surgery.Internal.GLinearize (GHC.Generics.M1 GHC.Generics.C m f)
instance forall k (f :: k -> *) c (m :: GHC.Generics.Meta) (tl :: k -> *). Generic.Data.Surgery.Internal.GLinearizeProduct f GHC.Generics.U1 => Generic.Data.Surgery.Internal.GLinearizeSum (GHC.Generics.M1 c m f) tl
instance forall k (tl :: k -> *). Generic.Data.Surgery.Internal.GLinearizeProduct GHC.Generics.U1 tl
instance forall k (g :: k -> *) (tl :: k -> *) (f :: k -> *). (Generic.Data.Surgery.Internal.GLinearizeProduct g tl, Generic.Data.Surgery.Internal.GLinearizeProduct f (Generic.Data.Surgery.Internal.LinearizeProduct g tl)) => Generic.Data.Surgery.Internal.GLinearizeProduct (f GHC.Generics.:*: g) tl
instance forall k s (m :: GHC.Generics.Meta) (f :: k -> *) (tl :: k -> *). Generic.Data.Surgery.Internal.GLinearizeProduct (GHC.Generics.M1 s m f) tl
instance forall k (f :: k -> *) (m :: GHC.Generics.Meta). Generic.Data.Surgery.Internal.GLinearizeSum f GHC.Generics.V1 => Generic.Data.Surgery.Internal.GLinearize (GHC.Generics.M1 GHC.Generics.D m f)
instance forall k (tl :: k -> *). Generic.Data.Surgery.Internal.GLinearizeSum GHC.Generics.V1 tl
instance forall k (g :: k -> *) (tl :: k -> *) (f :: k -> *). (Generic.Data.Surgery.Internal.GLinearizeSum g tl, Generic.Data.Surgery.Internal.GLinearizeSum f (Generic.Data.Surgery.Internal.LinearizeSum g tl)) => Generic.Data.Surgery.Internal.GLinearizeSum (f GHC.Generics.:+: g) tl
-- | Surgery for generic data types: remove and insert constructors and
-- fields.
--
-- Functions in this module are expected to be used with visible type
-- applications. Surgeries have a lot of type parameters, but usually
-- only the first one to three type arguments need to be passed via
-- TypeApplications. Functions are documented with informal
-- "functional dependencies", clarifying which type parameters can be
-- inferred from which others (click on "Details" under each function to
-- see those).
--
-- Remember that not all parameters to the left of a functional
-- dependency arrow need to be annotated explicitly to determine those on
-- the right. Some can also be inferred from the context.
--
-- Note that constructors and fields are indexed from zero.
module Generic.Data.Surgery
-- | Synthetic data type.
--
-- A wrapper to view a generic Rep as the datatype it's supposed
-- to represent, without needing a declaration.
data Data (r :: Type -> Type) p
-- | Conversion between a generic type and the synthetic type made using
-- its representation. Inverse of fromData.
toData :: Generic a => a -> Data (Rep a) p
-- | Inverse of toData.
fromData :: Generic a => Data (Rep a) p -> a
-- | A sterile Operating Room, where generic data comes to be
-- altered.
--
-- Generic representation in a simplified shape l at the type
-- level (reusing the constructors from GHC.Generics for
-- convenience). This representation makes it easy to modify fields and
-- constructors.
--
-- We may also refer to the representation l as a "row" of
-- constructors, if it represents a sum type, otherwise it is a "row" of
-- unnamed fields or record fields for single-constructor types.
--
-- x corresponds to the last parameter of Rep, and is
-- currently ignored by this module (no support for Generic1).
--
-- General sketch
--
--
-- toOR surgeries fromOR'
-- data MyType --------> OR (Rep MyType) ----------> OR alteredRep ---------> Data alteredRep
-- |
-- | myGenericFun :: Generic a => a -> a
-- fromOR surgeries toOR' v
-- data MyType <-------- OR (Rep MyType) <---------- OR alteredRep <--------- Data alteredRep
--
--
-- If instead myGenericFun is only a consumer of a
-- (resp. producer), then you only need the top half of the diagram
-- (resp. bottom half). For example, in aeson: genericToJSON
-- (consumer), genericParseJSON (producer).
data OR (l :: k -> Type) (x :: k)
-- | Move fresh data to the Operating Room, where surgeries can be
-- applied.
--
-- Convert a generic type to a generic representation.
--
-- When inserting or removing fields, there may be a mismatch with
-- strict/unpacked fields. To work around this, you can switch to
-- toORLazy, if your operations don't care about dealing with a
-- normalized Rep (in which all the strictness annotations have
-- been replaced with lazy defaults).
--
-- Details
--
-- Type parameters
--
--
-- a :: Type -- Generic type
-- l :: k -> Type -- Generic representation (simplified)
-- x :: k -- Ignored
--
--
-- Functional dependencies
--
--
-- a -> l
--
toOR :: forall a l x. (Generic a, ToORRep a l) => a -> OR l x
-- | Move altered data out of the Operating Room, to be consumed by
-- some generic function.
--
-- Convert a generic representation to a "synthetic" type that behaves
-- like a generic type.
--
-- Details
--
-- Type parameters
--
--
-- f :: k -> Type -- Generic representation (proper)
-- l :: k -> Type -- Generic representation (simplified)
-- x :: k -- Ignored
--
--
-- Functional dependencies
--
--
-- f -> l
-- l -> f
--
--
-- Implementation details
--
-- The synthesized representation is made of balanced binary trees,
-- corresponding closely to what GHC would generate for an actual data
-- type.
--
-- That structure assumed by at least one piece of code out there
-- (aeson).
fromOR' :: forall f l x. FromOR f l => OR l x -> Data f x
-- | Move altered data, produced by some generic function, to the
-- operating room.
--
-- The inverse of fromOR'.
--
-- Details
--
-- Type parameters
--
--
-- f :: k -> Type -- Generic representation (proper)
-- l :: k -> Type -- Generic representation (simplified)
-- x :: k -- Ignored
--
--
-- Functional dependencies
--
--
-- f -> l
-- l -> f
--
toOR' :: forall f l x. ToOR f l => Data f x -> OR l x
-- | Move restored data out of the Operating Room and back to the
-- real world.
--
-- The inverse of toOR.
--
-- It may be useful to annotate the output type of fromOR, since
-- the rest of the type depends on it and the only way to infer it
-- otherwise is from the context. The following annotations are possible:
--
--
-- fromOR :: OROf a -> a
-- fromOR @a -- with TypeApplications
--
--
-- When inserting or removing fields, there may be a mismatch with
-- strict/unpacked fields. To work around this, you can switch to
-- fromORLazy, if your operations don't care about dealing with a
-- normalized Rep (in which all the strictness annotations have
-- been replaced with lazy defaults).
--
-- Details
--
-- Type parameters
--
--
-- a :: Type -- Generic type
-- l :: k -> Type -- Generic representation (simplified)
-- x :: k -- Ignored
--
--
-- Functional dependencies
--
--
-- a -> l
--
fromOR :: forall a l x. (Generic a, FromORRep a l) => OR l x -> a
-- | The simplified generic representation type of type a, that
-- toOR and fromOR convert to and from.
type OROf a = OR (Linearize (Rep a)) ()
-- | Move normalized data to the Operating Room, where surgeries can be
-- applied.
--
-- Convert a generic type to a generic representation, in which all the
-- strictness annotations have been normalized to lazy defaults.
--
-- This variant is useful when one needs to operate on fields whose
-- Rep has different strictness annotations than the ones used by
-- DefaultMetaSel.
--
-- Details
--
-- Type parameters
--
--
-- a :: Type -- Generic type
-- l :: k -> Type -- Generic representation (simplified and normalized)
-- x :: k -- Ignored
--
--
-- Functional dependencies
--
--
-- a -> l
--
toORLazy :: forall a l x. (Generic a, ToORRepLazy a l) => a -> OR l x
-- | Move normalized data out of the Operating Room and back to the
-- real world.
--
-- The inverse of toORLazy.
--
-- It may be useful to annotate the output type of fromORLazy,
-- since the rest of the type depends on it and the only way to infer it
-- otherwise is from the context. The following annotations are possible:
--
--
-- fromORLazy :: OROfLazy a -> a
-- fromORLazy @a -- with TypeApplications
--
--
-- Details
--
-- Type parameters
--
--
-- a :: Type -- Generic type
-- l :: k -> Type -- Generic representation (simplified and normalized)
-- x :: k -- Ignored
--
--
-- Functional dependencies
--
--
-- a -> l
--
fromORLazy :: forall a l x. (Generic a, FromORRepLazy a l) => OR l x -> a
-- | The simplified and normalized generic representation type of type
-- a, that toORLazy and fromORLazy convert to and
-- from.
type OROfLazy a = OR (Linearize (Lazify (Rep a))) ()
-- | removeCField @n @t: remove the n-th field, of
-- type t, in a non-record single-constructor type.
--
-- Inverse of insertCField.
--
-- Details
--
-- Type parameters
--
--
-- n :: Nat -- Field position
-- t :: Type -- Field type
-- lt :: k -> Type -- Row with field
-- l :: k -> Type -- Row without field
-- x :: k -- Ignored
--
--
-- Signature
--
--
-- OR lt x -- Data with field
-- ->
-- (t, OR l x) -- Field value × Data without field
--
--
-- Functional dependencies
--
--
-- n lt -> t l
-- n t l -> lt
--
removeCField :: forall n t lt l x. RmvCField n t lt l => OR lt x -> (t, OR l x)
-- | insertCField @n @t: insert a field of type t
-- at position n in a non-record single-constructor type.
--
-- Inverse of removeCField.
--
-- Details
--
-- Type parameters
--
--
-- n :: Nat -- Field position
-- t :: Type -- Field type
-- lt :: k -> Type -- Row with field
-- l :: k -> Type -- Row without field
-- x :: k -- Ignored
--
--
-- Signature
--
--
-- (t, OR l x) -- Field value × Data without field
-- ->
-- OR lt x -- Data with field
--
--
-- Functional dependencies
--
--
-- n lt -> t l
-- n t l -> lt
--
insertCField :: forall n t lt l x. InsCField n t lt l => (t, OR l x) -> OR lt x
-- | Curried insertCField.
insertCField' :: forall n t lt l x. InsCField n t lt l => t -> OR l x -> OR lt x
-- | modifyCField @n @t @t': modify the field at position
-- n in a non-record via a function f :: t -> t'
-- (changing the type of the field).
--
-- Details
--
-- Type parameters
--
--
-- n :: Nat -- Field position
-- t :: Type -- Initial field type
-- t' :: Type -- Final field type
-- lt :: k -> Type -- Row with initial field
-- lt' :: k -> Type -- Row with final field
-- l :: k -> Type -- Row without field
-- x :: k -- Ignored
--
--
-- Signature
--
--
-- (t -> t') -- Field modification
-- ->
-- OR lt x -- Data with field t
-- ->
-- OR lt' x -- Data with field t'
--
--
-- Functional dependencies
--
--
-- n lt -> t l
-- n lt' -> t' l
-- n t l -> lt
-- n t' l -> lt'
--
modifyCField :: forall n t t' lt lt' l x. ModCField n t t' lt lt' l => (t -> t') -> OR lt x -> OR lt' x
-- | removeRField @"fdName" @n @t: remove the field
-- fdName at position n of type t in a record
-- type.
--
-- Inverse of insertRField.
--
-- Details
--
-- Type parameters
--
--
-- fd :: Symbol -- Field name
-- n :: Nat -- Field position
-- t :: Type -- Field type
-- lt :: k -> Type -- Row with field
-- l :: k -> Type -- Row without field
-- x :: k -- Ignored
--
--
-- Signature
--
--
-- OR lt x -- Data with field
-- ->
-- (t, OR l x) -- Field value × Data without field
--
--
-- Functional dependencies
--
--
-- fd lt -> n t l
-- n lt -> fd t l
-- fd n t l -> lt
--
removeRField :: forall fd n t lt l x. RmvRField fd n t lt l => OR lt x -> (t, OR l x)
-- | insertRField @"fdName" @n @t: insert a field named
-- fdName of type t at position n in a record
-- type.
--
-- Inverse of removeRField.
--
-- Details
--
-- Type parameters
--
--
-- fd :: Symbol -- Field name
-- n :: Nat -- Field position
-- t :: Type -- Field type
-- lt :: k -> Type -- Row with field
-- l :: k -> Type -- Row without field
-- x :: k -- Ignored
--
--
-- Signature
--
--
-- (t, OR l x) -- Field value × Data without field
-- ->
-- OR lt x -- Data with field
--
--
-- Functional dependencies
--
--
-- fd lt -> n t l
-- n lt -> fd t l
-- fd n t l -> lt
--
insertRField :: forall fd n t lt l x. InsRField fd n t lt l => (t, OR l x) -> OR lt x
-- | Curried insertRField.
insertRField' :: forall fd n t lt l x. InsRField fd n t lt l => t -> OR l x -> OR lt x
-- | modifyRField @"fdName" @n @t @t': modify the field
-- fdName at position n in a record via a function
-- f :: t -> t' (changing the type of the field).
--
-- Details
--
-- Type parameters
--
--
-- fd :: Symbol -- Field name
-- n :: Nat -- Field position
-- t :: Type -- Initial field type
-- t' :: Type -- Final field type
-- lt :: k -> Type -- Row with initial field
-- lt' :: k -> Type -- Row with final field
-- l :: k -> Type -- Row without field
-- x :: k -- Ignored
--
--
-- Signature
--
--
-- (t -> t') -- Field modification
-- ->
-- OR lt x -- Data with field t
-- ->
-- OR lt' x -- Data with field t'
--
--
-- Functional dependencies
--
--
-- fd lt -> n t l
-- fd lt' -> n t' l
-- n lt -> fd t l
-- n lt' -> fd t' l
-- fd n t l -> lt
-- fd n t' l -> lt'
--
modifyRField :: forall fd n t t' lt lt' l x. ModRField fd n t t' lt lt' l => (t -> t') -> OR lt x -> OR lt' x
-- | removeConstr @"C" @n @t: remove the n-th
-- constructor, named C, with contents isomorphic to the tuple
-- t.
--
-- Inverse of insertConstr.
--
-- Details
--
-- Type parameters
--
--
-- c :: Symbol -- Constructor name
-- t :: Type -- Tuple type to hold c's contents
-- n :: Nat -- Constructor position
-- lc :: k -> Type -- Row with constructor
-- l :: k -> Type -- Row without constructor
-- l_t :: k -> Type -- Field row of constructor c
-- x :: k -- Ignored
--
--
-- Signature
--
--
-- OR lc x -- Data with constructor
-- ->
-- Either t (OR l x) -- Constructor (as a tuple) | Data without constructor
--
--
-- Functional dependencies
--
--
-- c lc -> n l l_t
-- n lc -> c l l_t
-- c n l l_t -> lc
--
--
-- Note that there is no dependency to determine t.
removeConstr :: forall c n t lc l x. RmvConstr c n t lc l => OR lc x -> Either t (OR l x)
-- | insertConstr @"C" @n @t: insert a constructor
-- C at position n with contents isomorphic to the
-- tuple t.
--
-- Inverse of removeConstr.
--
-- Details
--
-- Type parameters
--
--
-- c :: Symbol -- Constructor name
-- t :: Type -- Tuple type to hold c's contents
-- n :: Nat -- Constructor position
-- lc :: k -> Type -- Row with constructor
-- l :: k -> Type -- Row without constructor
-- l_t :: k -> Type -- Field row of constructor c
-- x :: k -- Ignored
--
--
-- Signature
--
--
-- Either t (OR l x) -- Constructor (as a tuple) | Data without constructor
-- ->
-- OR lc x -- Data with constructor
--
--
-- Functional dependencies
--
--
-- c lc -> n l l_t
-- n lc -> c l l_t
-- c n l l_t -> lc
--
--
-- Note that there is no dependency to determine t.
insertConstr :: forall c n t lc l x. InsConstr c n t lc l => Either t (OR l x) -> OR lc x
-- | modifyConstr @"C" @n @t @t': modify the n-th
-- constructor, named C, with contents isomorphic to the tuple
-- t, to another tuple t'.
--
-- Details
--
-- Type parameters
--
--
-- c :: Symbol -- Constructor name
-- t :: Type -- Tuple type to hold c's initial contents
-- t' :: Type -- Tuple type to hold c's final contents
-- n :: Nat -- Constructor position
-- lc :: k -> Type -- Row with initial constructor
-- lc' :: k -> Type -- Row with final constructor
-- l :: k -> Type -- Row without constructor
-- l_t :: k -> Type -- Initial field row of constructor c
-- l_t' :: k -> Type -- Final field row of constructor c
-- x :: k -- Ignored
--
--
-- Signature
--
--
-- (t -> t') -- Constructor modification
-- ->
-- OR lc x -- Data with initial constructor
-- ->
-- OR lc' x -- Data with final constructor
--
--
-- Functional dependencies
--
--
-- c lc -> n l l_t
-- c lc' -> n l l_t'
-- n lc -> c l l_t
-- n lc' -> c l l_t'
-- c n l l_t -> lc
-- c n l l_t' -> lc'
--
--
-- Note that there is no dependency to determine t and
-- t'.
modifyConstr :: forall c n t t' lc lc' l x. ModConstr c n t t' lc lc' l => (t -> t') -> OR lc x -> OR lc' x
-- | A variant of removeConstr that can infer the tuple type
-- t to hold the contents of the removed constructor.
--
-- See removeConstr.
--
-- Details
--
-- Extra functional dependency
--
--
-- l_t -> t
--
removeConstrT :: forall c n t lc l x. RmvConstrT c n t lc l => OR lc x -> Either t (OR l x)
-- | A variant of insertConstr that can infer the tuple type
-- t to hold the contents of the inserted constructor.
--
-- See insertConstr.
--
-- Details
--
-- Extra functional dependency
--
--
-- l_t -> t
--
insertConstrT :: forall c n t lc l x. InsConstrT c n t lc l => Either t (OR l x) -> OR lc x
-- | A variant of modifyConstr that can infer the tuple types
-- t and t' to hold the contents of the inserted
-- constructor.
--
-- See modifyConstr.
--
-- Details
--
-- Extra functional dependencies
--
--
-- l_t -> t
-- l_t' -> t'
--
modifyConstrT :: forall c n t t' lc lc' l x. ModConstrT c n t t' lc lc' l => (t -> t') -> OR lc x -> OR lc' x
-- | Kind of surgeries: operations on generic representations of types.
--
-- Treat this as an abstract kind (don't pay attention to its
-- definition).
--
-- Implementation details
--
-- The name Surgery got taken first by generic-data.
--
-- k is the kind of the extra parameter reserved for
-- Generic1, which we just don't use.
type MajorSurgery k = MajorSurgery_ k
-- | A constraint Perform r s means that the surgery s
-- can be applied to the generic representation r.
class Perform_ r s => Perform (r :: k -> Type) (s :: MajorSurgery k)
-- | Operate f s. Apply a surgery s to a generic
-- representation f (e.g., f = Rep a for some
-- Generic type a).
--
-- The first argument is the generic representation; the second argument
-- is the surgery, which typically has the more complex syntax, which is
-- why this reverse application order was chosen.
type Operate (f :: k -> Type) (s :: MajorSurgery k) = Operate_ f s
-- | Composition of surgeries (left-to-right).
--
-- Note
--
-- Surgeries work on normalized representations, so Operate, which
-- applies a surgery to a generic representation, inserts normalization
-- steps before and after the surgery. This means that Operate
-- r (s1 :>> s2) is not quite the same as
-- Operate (Operate r s1) s2. Instead, the latter
-- is equivalent to Operate r (s1 :>>
-- Suture :>> s2), where Suture inserts
-- some intermediate normalization steps.
data (:>>) :: MajorSurgery k -> MajorSurgery k -> MajorSurgery k
infixl 1 :>>
-- | The identity surgery: doesn't do anything.
data IdSurgery :: MajorSurgery k
data InsertField (n :: Nat) (fd :: Maybe Symbol) (t :: Type) :: MajorSurgery k
data RemoveField (n :: Nat) (a :: Type) :: MajorSurgery k
data RemoveRField (fd :: Symbol) (a :: Type) :: MajorSurgery k
-- | This is polymorphic to allow different ways of specifying the inserted
-- constructor.
--
-- If sym (the kind of the constructor name c) is:
--
--
-- - Symbol: treat it like a regular prefix constructor.
-- - TODO Infix constructors and their fixities.
--
--
-- t must be a single-constructor type, then we reuse its
-- generic representation for the new constructor, only replacing its
-- constructor name with c.
data InsertConstrAt (c :: sym) (n :: Nat) (t :: ty) :: MajorSurgery k
data RemoveConstr (c :: Symbol) (t :: Type) :: MajorSurgery k
-- | Use this if a patient ever needs to go out and back into the operating
-- room, when it's not just to undo the surgery up to that point.
data Suture :: MajorSurgery k
-- | This constraint means that a is convertible to its
-- simplified generic representation. Implies OROf a ~
-- OR l ().
type ToORRep a l = ToOR (Rep a) l
-- | Similar to ToORRep, but as a constraint on the standard generic
-- representation of a directly, f ~ Rep a.
type ToOR f l = (GLinearize f, Linearize f ~ l, f ~ Arborify l)
-- | This constraint means that a is convertible to its
-- simplified and normalized generic representation (i.e., with all its
-- strictness annotations normalized to lazy defaults). Implies
-- OROfLazy a ~ OR l ().
type ToORRepLazy a l = ToORLazy (Rep a) l
-- | Similar to ToORRepLazy, but as a constraint on the standard
-- generic representation of a directly, f ~ Rep
-- a.
type ToORLazy f l = (ToOR (Lazify f) l, Coercible f (Arborify l))
-- | This constraint means that a is convertible from its
-- simplified generic representation. Implies OROf a ~
-- OR l ().
type FromORRep a l = FromOR (Rep a) l
-- | Similar to FromORRep, but as a constraint on the standard
-- generic representation of a directly, f ~ Rep
-- a.
type FromOR f l = (GArborify f, Linearize f ~ l, f ~ Arborify l)
-- | This constraint means that a is convertible from its
-- simplified and normalized generic representation (i.e., with all its
-- strictness annotations normalized to lazy defaults). Implies
-- OROfLazy a ~ OR l ().
type FromORRepLazy a l = FromORLazy (Rep a) l
-- | Similar to FromLazyORRep, but as a constraint on the standard
-- generic representation of a directly, f ~ Rep
-- a.
type FromORLazy f l = (FromOR (Lazify f) l, Coercible (Arborify l) f)
-- | This constraint means that the (unnamed) field row lt
-- contains a field of type t at position n, and
-- removing it yields row l.
type RmvCField n t lt l = (GRemoveField n t lt l, CFieldSurgery n t lt l)
-- | This constraint means that inserting a field t at position
-- n in the (unnamed) field row l yields row
-- lt.
type InsCField n t lt l = (GInsertField n t l lt, CFieldSurgery n t lt l)
-- | This constraint means that modifying a field t to t'
-- at position n in the (unnamed) field row lt yields
-- row lt'. l is the row of fields common to
-- lt and lt'.
type ModCField n t t' lt lt' l = (RmvCField n t lt l, InsCField n t' lt' l)
-- | This constraint means that the record field row lt contains a
-- field of type t named fd at position n, and
-- removing it yields row l.
type RmvRField fd n t lt l = (GRemoveField n t lt l, RFieldSurgery fd n t lt l)
-- | This constraint means that inserting a field t named
-- fd at position n in the record field row l
-- yields row lt.
type InsRField fd n t lt l = (GInsertField n t l lt, RFieldSurgery fd n t lt l)
-- | This constraint means that modifying a field t named
-- fd at position n to t' in the record field
-- row lt yields row lt'. l is the row of
-- fields common to lt and lt'.
type ModRField fd n t t' lt lt' l = (RmvRField fd n t lt l, InsRField fd n t' lt' l)
-- | This constraint means that the constructor row lc contains a
-- constructor named c at position n, and removing it
-- from lc yields row l. Furthermore, constructor
-- c contains a field row l_t compatible with the tuple
-- type t.
type RmvConstr c n t lc l = (GRemoveConstr n t lc l, ConstrSurgery c n t lc l (Eval (ConstrAt n lc)))
-- | This constraint means that inserting a constructor c at
-- position n in the constructor row l yields row
-- lc. Furthermore, constructor c contains a field row
-- l_t compatible with the tuple type t.
type InsConstr c n (t :: Type) lc l = (GInsertConstr n t l lc, ConstrSurgery c n t lc l (Eval (ConstrAt n lc)))
-- | This constraint means that the constructor row lc contains a
-- constructor named c at position n of type isomorphic
-- to t, and modifying it to t' yields row
-- lc'.
type ModConstr c n t t' lc lc' l = (RmvConstr c n t lc l, InsConstr c n t' lc' l)
-- | A variant of RmvConstr allowing t to be inferred.
type RmvConstrT c n t lc l = (RmvConstr c n t lc l, IsTuple (Arity (Eval (ConstrAt n lc))) t)
-- | A variant of InsConstr allowing t to be inferred.
type InsConstrT c n t lc l = (InsConstr c n t lc l, IsTuple (Arity (Eval (ConstrAt n lc))) t)
-- | A variant of ModConstr allowing t and t' to
-- be inferred.
type ModConstrT c n t t' lc lc' l = (ModConstr c n t t' lc lc' l, IsTuple (Arity (Eval (ConstrAt n lc))) t, IsTuple (Arity (Eval (ConstrAt n lc'))) t')