Safe Haskell	None
Language	Haskell2010

Generic.Data.Surgery

Contents

Getting into the operating room
Surgeries
Constraint synonyms
- Conversions
- Surgeries

Description

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 annotated with "functional dependencies", with a meaning similar to the homonymous GHC extension for type classes (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.

Synopsis

data Data (r :: Type -> Type) p
toData :: Generic a => a -> Data (Rep a) p
fromData :: Generic a => Data (Rep a) p -> a
onData :: (UnifyRep (Rep a) (Rep b), UnifyRep (Rep a) (Rep b)) => p a b -> p a b
data OR (l :: k -> Type) (x :: k)
toOR :: forall a l x. (Generic a, ToORRep a l) => a -> OR l x
fromOR' :: forall f l x. FromOR f l => OR l x -> Data f x
toOR' :: forall f l x. ToOR f l => Data f x -> OR l x
fromOR :: forall a l x. (Generic a, FromORRep a l) => OR l x -> a
type OROf a = OR (Linearize (Rep a)) ()
removeCField :: forall n t lt l x. RmvCField n t lt l => OR lt x -> (t, OR l x)
insertCField :: forall n t lt l x. InsCField n t lt l => (t, OR l x) -> OR lt x
insertCField' :: forall n t lt l x. InsCField n t lt l => t -> OR l x -> OR lt x
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 :: forall fd n t lt l x. RmvRField fd n t lt l => OR lt x -> (t, OR l x)
insertRField :: forall fd n t lt l x. InsRField fd n t lt l => (t, OR l x) -> OR lt x
insertRField' :: forall fd n t lt l x. InsRField fd n t lt l => t -> OR l x -> OR lt x
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 :: forall c n t lc l l_t x. RmvConstr c n t lc l l_t => OR lc x -> Either t (OR l x)
insertConstr :: forall c n t lc l l_t x. InsConstr c n t lc l l_t => Either t (OR l x) -> OR lc x
modifyConstr :: forall c n t t' lc lc' l l_t l_t' x. ModConstr c n t t' lc lc' l l_t l_t' => (t -> t') -> OR lc x -> OR lc' x
removeConstrT :: forall c n t lc l l_t x. RmvConstrT c n t lc l l_t => OR lc x -> Either t (OR l x)
insertConstrT :: forall c n t lc l l_t x. InsConstrT c n t lc l l_t => Either t (OR l x) -> OR lc x
modifyConstrT :: forall c n t t' lc lc' l l_t l_t' x. ModConstrT c n t t' lc lc' l l_t l_t' => (t -> t') -> OR lc x -> OR lc' x
type ToORRep a l = ToOR (Rep a) l
type ToOR f l = (GLinearize f, Linearize f ~ l, f ~ Arborify l)
type FromORRep a l = FromOR (Rep a) l
type FromOR f l = (GArborify f, Linearize f ~ l, f ~ Arborify l)
type RmvCField n t lt l = (GRemoveField n lt, CFieldSurgery n t lt l)
type InsCField n t lt l = (GInsertField n lt, CFieldSurgery n t lt l)
type ModCField n t t' lt lt' l = (RmvCField n t lt l, InsCField n t' lt' l)
type RmvRField fd n t lt l = (GRemoveField n lt, RFieldSurgery fd n t lt l)
type InsRField fd n t lt l = (GInsertField n lt, RFieldSurgery fd n t lt l)
type ModRField fd n t t' lt lt' l = (RmvRField fd n t lt l, InsRField fd n t' lt' l)
type RmvConstr c n t lc l l_t = (GRemoveConstr n lc, GArborify (Arborify l_t), ConstrSurgery c n t lc l l_t)
type InsConstr c n t lc l l_t = (GInsertConstr n lc, GLinearize (Arborify l_t), ConstrSurgery c n t lc l l_t)
type ModConstr c n t t' lc lc' l l_t l_t' = (RmvConstr c n t lc l l_t, InsConstr c n t' lc' l l_t')
type RmvConstrT c n t lc l l_t = (RmvConstr c n t lc l l_t, IsTuple (Arity l_t) t)
type InsConstrT c n t lc l l_t = (InsConstr c n t lc l l_t, IsTuple (Arity l_t) t)
type ModConstrT c n t t' lc lc' l l_t l_t' = (ModConstr c n t t' lc lc' l l_t l_t', IsTuple (Arity l_t) t, IsTuple (Arity l_t') t')

Documentation

data Data (r :: Type -> Type) p #

Synthetic data type.

A wrapper to view a generic Rep as the datatype it's supposed to represent, without needing a declaration.

Instances

Monad r => Monad (Data r)
Instance details Defined in Generic.Data.Internal.Data Methods (>>=) :: Data r a -> (a -> Data r b) -> Data r b # (>>) :: Data r a -> Data r b -> Data r b # return :: a -> Data r a # fail :: String -> Data r a #
Functor r => Functor (Data r)
Instance details Defined in Generic.Data.Internal.Data Methods fmap :: (a -> b) -> Data r a -> Data r b # (<$) :: a -> Data r b -> Data r a #
Applicative r => Applicative (Data r)
Instance details Defined in Generic.Data.Internal.Data Methods pure :: a -> Data r a # (<>) :: Data r (a -> b) -> Data r a -> Data r b # liftA2 :: (a -> b -> c) -> Data r a -> Data r b -> Data r c # (>) :: Data r a -> Data r b -> Data r b # (<*) :: Data r a -> Data r b -> Data r a #
Foldable r => Foldable (Data r)
Instance details Defined in Generic.Data.Internal.Data Methods fold :: Monoid m => Data r m -> m # foldMap :: Monoid m => (a -> m) -> Data r a -> m # foldr :: (a -> b -> b) -> b -> Data r a -> b # foldr' :: (a -> b -> b) -> b -> Data r a -> b # foldl :: (b -> a -> b) -> b -> Data r a -> b # foldl' :: (b -> a -> b) -> b -> Data r a -> b # foldr1 :: (a -> a -> a) -> Data r a -> a # foldl1 :: (a -> a -> a) -> Data r a -> a # toList :: Data r a -> [a] # null :: Data r a -> Bool # length :: Data r a -> Int # elem :: Eq a => a -> Data r a -> Bool # maximum :: Ord a => Data r a -> a # minimum :: Ord a => Data r a -> a # sum :: Num a => Data r a -> a # product :: Num a => Data r a -> a #
Traversable r => Traversable (Data r)
Instance details Defined in Generic.Data.Internal.Data Methods traverse :: Applicative f => (a -> f b) -> Data r a -> f (Data r b) # sequenceA :: Applicative f => Data r (f a) -> f (Data r a) # mapM :: Monad m => (a -> m b) -> Data r a -> m (Data r b) # sequence :: Monad m => Data r (m a) -> m (Data r a) #
Contravariant r => Contravariant (Data r)
Instance details Defined in Generic.Data.Internal.Data Methods contramap :: (a -> b) -> Data r b -> Data r a # (>$) :: b -> Data r b -> Data r a #
Eq1 r => Eq1 (Data r)
Instance details Defined in Generic.Data.Internal.Data Methods liftEq :: (a -> b -> Bool) -> Data r a -> Data r b -> Bool #
Ord1 r => Ord1 (Data r)
Instance details Defined in Generic.Data.Internal.Data Methods liftCompare :: (a -> b -> Ordering) -> Data r a -> Data r b -> Ordering #
GShow1 r => Show1 (Data r)
Instance details Defined in Generic.Data.Internal.Data Methods liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Data r a -> ShowS # liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Data r a] -> ShowS #
Alternative r => Alternative (Data r)
Instance details Defined in Generic.Data.Internal.Data Methods empty :: Data r a # (<\|>) :: Data r a -> Data r a -> Data r a # some :: Data r a -> Data r [a] # many :: Data r a -> Data r [a] #
MonadPlus r => MonadPlus (Data r)
Instance details Defined in Generic.Data.Internal.Data Methods mzero :: Data r a # mplus :: Data r a -> Data r a -> Data r a #
Generic1 (Data r :: Type -> Type)
Instance details Defined in Generic.Data.Internal.Data Associated Types type Rep1 (Data r) :: k -> Type # Methods from1 :: Data r a -> Rep1 (Data r) a # to1 :: Rep1 (Data r) a -> Data r a #
GBounded r => Bounded (Data r p)
Instance details Defined in Generic.Data.Internal.Data Methods minBound :: Data r p # maxBound :: Data r p #
GEnum StandardEnum r => Enum (Data r p)
Instance details Defined in Generic.Data.Internal.Data Methods succ :: Data r p -> Data r p # pred :: Data r p -> Data r p # toEnum :: Int -> Data r p # fromEnum :: Data r p -> Int # enumFrom :: Data r p -> [Data r p] # enumFromThen :: Data r p -> Data r p -> [Data r p] # enumFromTo :: Data r p -> Data r p -> [Data r p] # enumFromThenTo :: Data r p -> Data r p -> Data r p -> [Data r p] #
Eq (r p) => Eq (Data r p)
Instance details Defined in Generic.Data.Internal.Data Methods (==) :: Data r p -> Data r p -> Bool # (/=) :: Data r p -> Data r p -> Bool #
Ord (r p) => Ord (Data r p)
Instance details Defined in Generic.Data.Internal.Data Methods compare :: Data r p -> Data r p -> Ordering # (<) :: Data r p -> Data r p -> Bool # (<=) :: Data r p -> Data r p -> Bool # (>) :: Data r p -> Data r p -> Bool # (>=) :: Data r p -> Data r p -> Bool # max :: Data r p -> Data r p -> Data r p # min :: Data r p -> Data r p -> Data r p #
(GShow1 r, Show p) => Show (Data r p)
Instance details Defined in Generic.Data.Internal.Data Methods showsPrec :: Int -> Data r p -> ShowS # show :: Data r p -> String # showList :: [Data r p] -> ShowS #
(Functor r, Contravariant r) => Generic (Data r p)
Instance details Defined in Generic.Data.Internal.Data Associated Types type Rep (Data r p) :: Type -> Type # Methods from :: Data r p -> Rep (Data r p) x # to :: Rep (Data r p) x -> Data r p #
Semigroup (r p) => Semigroup (Data r p)
Instance details Defined in Generic.Data.Internal.Data Methods (<>) :: Data r p -> Data r p -> Data r p # sconcat :: NonEmpty (Data r p) -> Data r p # stimes :: Integral b => b -> Data r p -> Data r p #
Monoid (r p) => Monoid (Data r p)
Instance details Defined in Generic.Data.Internal.Data Methods mempty :: Data r p # mappend :: Data r p -> Data r p -> Data r p # mconcat :: [Data r p] -> Data r p #
type Rep1 (Data r :: Type -> Type)
Instance details Defined in Generic.Data.Internal.Data type Rep1 (Data r :: Type -> Type) = r
type Rep (Data r p)
Instance details Defined in Generic.Data.Internal.Data type Rep (Data r p) = r

toData :: Generic a => a -> Data (Rep a) p #

Conversion between a generic type and the synthetic type made using its representation.

fromData :: Generic a => Data (Rep a) p -> a #

Inverse of fromData.

onData :: (UnifyRep (Rep a) (Rep b), UnifyRep (Rep a) (Rep b)) => p a b -> p a b Source #

Can be used with generic-lens for type-changing field updates.

A specialization of the identity function to be used to fix types of functions using Data as input or output, unifying the "spines" of input and output generic representations (the "spine" is everything except field types, which may thus change).

Getting into the operating room

data OR (l :: k -> Type) (x :: k) Source #

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

toOR :: forall a l x. (Generic a, ToORRep a l) => a -> OR l x Source #

Move fresh data to the Operating Room, where surgeries can be applied.

Convert a generic type to a generic representation.

Details

Expand

Type parameters

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

Functional dependencies

a -> l

fromOR' :: forall f l x. FromOR f l => OR l x -> Data f x Source #

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

Expand

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

toOR' :: forall f l x. ToOR f l => Data f x -> OR l x Source #

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

The inverse of fromOR'.

Details

Expand

Type parameters

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

Functional dependencies

f -> l
l -> f

fromOR :: forall a l x. (Generic a, FromORRep a l) => OR l x -> a Source #

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

Details

Expand

Type parameters

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

Functional dependencies

a -> l

type OROf a = OR (Linearize (Rep a)) () Source #

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

Surgeries

Unnamed fields

removeCField :: forall n t lt l x. RmvCField n t lt l => OR lt x -> (t, OR l x) Source #

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

Inverse of insertCField.

Details

Expand

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

insertCField :: forall n t lt l x. InsCField n t lt l => (t, OR l x) -> OR lt x Source #

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

Inverse of removeCField.

Details

Expand

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 Source #

Curried insertCField.

modifyCField :: forall n t t' lt lt' l x. ModCField n t t' lt lt' l => (t -> t') -> OR lt x -> OR lt' x Source #

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

Expand

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'

Named fields (records)

removeRField :: forall fd n t lt l x. RmvRField fd n t lt l => OR lt x -> (t, OR l x) Source #

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

Inverse of insertRField.

Details

Expand

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

insertRField :: forall fd n t lt l x. InsRField fd n t lt l => (t, OR l x) -> OR lt x Source #

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

Inverse of removeRField.

Details

Expand

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 Source #

Curried insertRField.

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 Source #

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

Expand

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'

Constructors

A constructor is extracted to a "tuple", which can be any Generic single-constructor type with the same number of fields.

Note that () and Identity can be used as an empty and a singleton tuple type respectively.

When the tuple type can't be inferred and doesn't really matter, an alternative to explicit type annotations is to use the ...ConstrT variants of these surgeries, which are specialized to actual tuples ((), Identity, (,), (,,), up to 7 --- because that's where Generic instances currently stop).

removeConstr :: forall c n t lc l l_t x. RmvConstr c n t lc l l_t => OR lc x -> Either t (OR l x) Source #

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

Inverse of insertConstr.

Details

Expand

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.

insertConstr :: forall c n t lc l l_t x. InsConstr c n t lc l l_t => Either t (OR l x) -> OR lc x Source #

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

Inverse of removeConstr.

Details

Expand

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.

modifyConstr :: forall c n t t' lc lc' l l_t l_t' x. ModConstr c n t t' lc lc' l l_t l_t' => (t -> t') -> OR lc x -> OR lc' x Source #

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

Details

Expand

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

removeConstrT :: forall c n t lc l l_t x. RmvConstrT c n t lc l l_t => OR lc x -> Either t (OR l x) Source #

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

See removeConstr.

Details

Expand

Extra functional dependency

l_t -> t

insertConstrT :: forall c n t lc l l_t x. InsConstrT c n t lc l l_t => Either t (OR l x) -> OR lc x Source #

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

See insertConstr.

Details

Expand

Extra functional dependency

l_t -> t

modifyConstrT :: forall c n t t' lc lc' l l_t l_t' x. ModConstrT c n t t' lc lc' l l_t l_t' => (t -> t') -> OR lc x -> OR lc' x Source #

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

See modifyConstr.

Details

Expand

Extra functional dependencies

l_t  -> t
l_t' -> t'

Constraint synonyms

Hiding implementation details from the signatures above. Useful to compose surgeries in a reusable way.

Conversions

type ToORRep a l = ToOR (Rep a) l Source #

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

type ToOR f l = (GLinearize f, Linearize f ~ l, f ~ Arborify l) Source #

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

type FromORRep a l = FromOR (Rep a) l Source #

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

type FromOR f l = (GArborify f, Linearize f ~ l, f ~ Arborify l) Source #

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

Surgeries

type RmvCField n t lt l = (GRemoveField n lt, CFieldSurgery n t lt l) Source #

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 InsCField n t lt l = (GInsertField n lt, CFieldSurgery n t lt l) Source #

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

type ModCField n t t' lt lt' l = (RmvCField n t lt l, InsCField n t' lt' l) Source #

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 RmvRField fd n t lt l = (GRemoveField n lt, RFieldSurgery fd n t lt l) Source #

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 InsRField fd n t lt l = (GInsertField n lt, RFieldSurgery fd n t lt l) Source #

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

type ModRField fd n t t' lt lt' l = (RmvRField fd n t lt l, InsRField fd n t' lt' l) Source #

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 RmvConstr c n t lc l l_t = (GRemoveConstr n lc, GArborify (Arborify l_t), ConstrSurgery c n t lc l l_t) Source #

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 InsConstr c n t lc l l_t = (GInsertConstr n lc, GLinearize (Arborify l_t), ConstrSurgery c n t lc l l_t) Source #

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 ModConstr c n t t' lc lc' l l_t l_t' = (RmvConstr c n t lc l l_t, InsConstr c n t' lc' l l_t') Source #

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 RmvConstrT c n t lc l l_t = (RmvConstr c n t lc l l_t, IsTuple (Arity l_t) t) Source #

A variant of RmvConstr allowing t to be inferred.

type InsConstrT c n t lc l l_t = (InsConstr c n t lc l l_t, IsTuple (Arity l_t) t) Source #

A variant of InsConstr allowing t to be inferred.

type ModConstrT c n t t' lc lc' l l_t l_t' = (ModConstr c n t t' lc lc' l l_t l_t', IsTuple (Arity l_t) t, IsTuple (Arity l_t') t') Source #

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