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

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

a :: Type       -- Generic type
l :: k -> Type  -- Generic representation (simplified)
x :: k          -- Ignored

a -> l

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

a :: Type       -- Generic type
l :: k -> Type  -- Generic representation (simplified and normalized)
x :: k          -- Ignored

a -> l

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

f :: k -> Type  -- Generic representation (proper)
l :: k -> Type  -- Generic representation (simplified)
x :: k          -- Ignored

f -> l
l -> f

Move altered data, produced by some generic function, to the operating room.

The inverse of fromOR'.

Details

f :: k -> Type  -- Generic representation (proper)
l :: k -> Type  -- Generic representation (simplified)
x :: k          -- Ignored

f -> l
l -> f

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

a :: Type       -- Generic type
l :: k -> Type  -- Generic representation (simplified)
x :: k          -- Ignored

a -> l

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

a :: Type       -- Generic type
l :: k -> Type  -- Generic representation (simplified and normalized)
x :: k          -- Ignored

a -> l

The simplified generic representation type of type a, that toOR and fromOR convert to and from.

The simplified and normalized generic representation type of type a, that toORLazy and fromORLazy convert to and from.

This constraint means that a is convertible to its simplified generic representation. Implies OROf a ~ OR l ().

This constraint means that a is convertible from its simplified generic representation. Implies OROf a ~ OR l ().

Similar to ToORRep, but as a constraint on the standard generic representation of a directly, f ~ Rep a.

Similar to FromORRep, but as a constraint on the standard generic representation of a directly, f ~ Rep a.

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 ().

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 ().

Similar to FromLazyORRep, but as a constraint on the standard generic representation of a directly, f ~ Rep a.

Similar to ToORRepLazy, but as a constraint on the standard generic representation of a directly, f ~ Rep a.

removeCField @n @t: remove the n-th field, of type t, in a non-record single-constructor type.

Inverse of insertCField.

Details

n  :: Nat        -- Field position
t  :: Type       -- Field type
lt :: k -> Type  -- Row with    field
l  :: k -> Type  -- Row without field
x  :: k          -- Ignored

OR lt x      -- Data with field
->
(t, OR l x)  -- Field value × Data without field

n lt  -> t l
n t l -> lt

removeRField @"fdName" @n @t: remove the field fdName at position n of type t in a record type.

Inverse of insertRField.

Details

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

OR lt x      -- Data with field
->
(t, OR l x)  -- Field value × Data without field

fd lt    -> n  t l
n  lt    -> fd t l
fd n t l -> lt

insertCField @n @t: insert a field of type t at position n in a non-record single-constructor type.

Inverse of removeCField.

Details

n  :: Nat        -- Field position
t  :: Type       -- Field type
lt :: k -> Type  -- Row with    field
l  :: k -> Type  -- Row without field
x  :: k          -- Ignored

(t, OR l x)  -- Field value × Data without field
->
OR lt x      -- Data with field

n lt  -> t l
n t l -> lt

Curried insertCField.

insertRField @"fdName" @n @t: insert a field named fdName of type t at position n in a record type.

Inverse of removeRField.

Details

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

(t, OR l x)  -- Field value × Data without field
->
OR lt x      -- Data with field

fd lt    -> n  t l
n  lt    -> fd t l
fd n t l -> lt

Curried insertRField.

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

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

(t -> t')  -- Field modification
->
OR lt  x   -- Data with field t
->
OR lt' x   -- Data with field t'

n lt   -> t  l
n lt'  -> t' l
n t  l -> lt
n t' l -> lt'

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

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

(t -> t')  -- Field modification
->
OR lt  x   -- Data with field t
->
OR lt' x   -- Data with field t'

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'

removeConstr @"C" @n @t: remove the n-th constructor, named C, with contents isomorphic to the tuple t.

Inverse of insertConstr.

Details

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

OR lc x            -- Data with constructor
->
Either t (OR l x)  -- Constructor (as a tuple) | Data without constructor

c lc      -> n l l_t
n lc      -> c l l_t
c n l l_t -> lc

A variant of removeConstr that can infer the tuple type t to hold the contents of the removed constructor.

See removeConstr.

Details

l_t -> t

insertConstr @"C" @n @t: insert a constructor C at position n with contents isomorphic to the tuple t.

Inverse of removeConstr.

Details

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

Either t (OR l x)  -- Constructor (as a tuple) | Data without constructor
->
OR lc x            -- Data with constructor

c lc      -> n l l_t
n lc      -> c l l_t
c n l l_t -> lc

A variant of insertConstr that can infer the tuple type t to hold the contents of the inserted constructor.

See insertConstr.

Details

l_t -> t

modifyConstr @"C" @n @t @t': modify the n-th constructor, named C, with contents isomorphic to the tuple t, to another tuple t'.

Details

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

(t -> t')  -- Constructor modification
->
OR lc  x   -- Data with initial constructor
->
OR lc' x   -- Data with final   constructor

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'

A variant of modifyConstr that can infer the tuple types t and t' to hold the contents of the inserted constructor.

See modifyConstr.

Details

l_t  -> t
l_t' -> t'

This constraint means that the (unnamed) field row lt contains a field of type t at position n, and removing it yields row 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.

This constraint means that inserting a field t at position n in the (unnamed) field row l yields row lt.

This constraint means that inserting a field t named fd at position n in the record field row l yields row lt.

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

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

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.

A variant of RmvConstr allowing t to be inferred.

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.

A variant of InsConstr allowing t to be inferred.

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

A variant of ModConstr allowing t and t' to be inferred.

Kind of surgeries: operations on generic representations of types.

Treat this as an abstract kind (don't pay attention to its definition).

Implementation details

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.

Internal definition of MajorSurgery.

Internal definition of Operate.

Apply a surgery s to a linearized generic representation 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.

The identity surgery: doesn't do anything.

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.

A constraint Perform r s means that the surgery s can be applied to the generic representation r.

Like RemoveField but without the explicit field type.

Position of a record field

Number of fields of a single constructor

Number of constructors of a data type

Like RemoveConstr, but without the explicit constructor type.

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.

Equate two generic representations, but ignoring constructor and field metadata.