generic-data-surgery-0.3.0.0: src/Generic/Data/Surgery/Internal.hs
{-# LANGUAGE
AllowAmbiguousTypes,
BangPatterns,
ConstraintKinds,
DataKinds,
DeriveGeneric,
FlexibleContexts,
FlexibleInstances,
LambdaCase,
MultiParamTypeClasses,
PolyKinds,
ScopedTypeVariables,
TypeApplications,
TypeFamilies,
TypeOperators,
TypeInType,
UndecidableInstances,
UndecidableSuperClasses #-}
-- | Operate on data types: insert\/modify\/delete fields and constructors.
module Generic.Data.Surgery.Internal where
import Control.Monad ((<=<))
import Data.Bifunctor (first, second)
import Data.Coerce
import Data.Functor.Identity (Identity)
import Data.Kind (Constraint, Type)
import Data.Type.Equality (type (==))
import GHC.Generics
import GHC.TypeLits
import Fcf
( Exp, Eval, If, Pure, Pure2, Bimap, Uncurry
, type (@@), type (=<<), type (<=<), type (<$>)
)
import Generic.Data (MetaOf, MetaConsName)
import Generic.Data.Internal.Compat (Div)
import Generic.Data.Internal.Data (Data(Data,unData))
import Generic.Data.Internal.Meta (UnM1)
import Generic.Data.Internal.Utils (coerce', absurd1)
-- | /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 { unOR :: 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
toOR = OR . gLinearize . from
-- | /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
toORLazy = OR . gLinearize @(Arborify l) . coerce' . from
-- | /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
fromOR' = Data . gArborify . unOR
-- | /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
toOR' = OR . gLinearize . unData
-- | /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
fromOR = to . gArborify . unOR
-- | /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
fromORLazy = to . coerce' . gArborify @(Lazify (Rep a)) . unOR
-- | 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)
removeCField (OR a) = OR <$> gRemoveField @n a
-- | @'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)
removeRField (OR a) = OR <$> gRemoveField @n a
-- | @'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
insertCField = uncurry (insertCField' @n)
-- | Curried 'insertCField'.
insertCField'
:: forall n t lt l x
. InsCField n t lt l
=> t -> OR l x -> OR lt x
insertCField' z (OR a) = OR (gInsertField @n z a)
-- | @'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
insertRField = uncurry (insertRField' @fd)
-- | Curried 'insertRField'.
insertRField'
:: forall fd n t lt l x
. InsRField fd n t lt l
=> t -> OR l x -> OR lt x
insertRField' z (OR a) = OR (gInsertField @n z a)
-- | @'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
modifyCField f = insertCField @n @t' . first f . removeCField @n @t
-- | @'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
modifyRField f = insertRField @fd @n @t' . first f . removeRField @fd @n @t
-- | @'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)
removeConstr (OR a) = second OR (gRemoveConstr @n a)
-- | 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)
removeConstrT = removeConstr @c @n @t
-- | @'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
insertConstr z = OR (gInsertConstr @n (second unOR z))
-- | 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
insertConstrT = insertConstr @c @n @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__
--
-- ==== 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
modifyConstr f = insertConstr @c @n @t' . first f . removeConstr @c @n @t
-- | 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
modifyConstrT = modifyConstr @c @n @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@.
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 instance Linearize (M1 D m f) = M1 D m (LinearizeSum f V1)
type instance Linearize (M1 C m f) = M1 C m (LinearizeProduct f U1)
type family LinearizeSum (f :: k -> Type) (tl :: k -> Type) :: k -> Type
type instance LinearizeSum V1 tl = tl
type instance LinearizeSum (f :+: g) tl = LinearizeSum f (LinearizeSum g tl)
type instance LinearizeSum (M1 c m f) tl = M1 c m (LinearizeProduct f U1) :+: tl
type family LinearizeProduct (f :: k -> Type) (tl :: k -> Type) :: k -> Type
type instance LinearizeProduct U1 tl = tl
type instance LinearizeProduct (f :*: g) tl = LinearizeProduct f (LinearizeProduct g tl)
type instance LinearizeProduct (M1 s m f) tl = M1 s m f :*: tl
class GLinearize f where
gLinearize :: f x -> Linearize f x
instance GLinearizeSum f V1 => GLinearize (M1 D m f) where
gLinearize (M1 a) = M1 (gLinearizeSum @_ @V1 (Left a))
instance GLinearizeProduct f U1 => GLinearize (M1 C m f) where
gLinearize (M1 a) = M1 (gLinearizeProduct a U1)
class GLinearizeSum f tl where
gLinearizeSum :: Either (f x) (tl x) -> LinearizeSum f tl x
instance GLinearizeSum V1 tl where
gLinearizeSum (Left v) = absurd1 v
gLinearizeSum (Right c) = c
instance (GLinearizeSum g tl, GLinearizeSum f (LinearizeSum g tl))
=> GLinearizeSum (f :+: g) tl where
gLinearizeSum (Left (L1 a)) = gLinearizeSum @_ @(LinearizeSum g tl) (Left a)
gLinearizeSum (Left (R1 b)) = gLinearizeSum @f (Right (gLinearizeSum @g @tl (Left b)))
gLinearizeSum (Right c) = gLinearizeSum @f (Right (gLinearizeSum @g (Right c)))
instance GLinearizeProduct f U1 => GLinearizeSum (M1 c m f) tl where
gLinearizeSum (Left (M1 a)) = L1 (M1 (gLinearizeProduct a U1))
gLinearizeSum (Right c) = R1 c
class GLinearizeProduct f tl where
gLinearizeProduct :: f x -> tl x -> LinearizeProduct f tl x
instance GLinearizeProduct U1 tl where
gLinearizeProduct _ = id
instance (GLinearizeProduct g tl, GLinearizeProduct f (LinearizeProduct g tl))
=> GLinearizeProduct (f :*: g) tl where
gLinearizeProduct (a :*: b) = gLinearizeProduct a . gLinearizeProduct b
instance GLinearizeProduct (M1 s m f) tl where
gLinearizeProduct = (:*:)
class GArborify f where
gArborify :: Linearize f x -> f x
instance GArborifySum f V1 => GArborify (M1 D m f) where
gArborify (M1 a) = case gArborifySum @_ @V1 a of
Left a' -> M1 a'
Right v -> absurd1 v
instance GArborifyProduct f U1 => GArborify (M1 C m f) where
gArborify (M1 a) = M1 (fst (gArborifyProduct @_ @U1 a))
class GArborifySum f tl where
gArborifySum :: LinearizeSum f tl x -> Either (f x) (tl x)
instance GArborifySum V1 tl where
gArborifySum = Right
instance (GArborifySum g tl, GArborifySum f (LinearizeSum g tl))
=> GArborifySum (f :+: g) tl where
gArborifySum = first R1 . gArborifySum <=< first L1 . gArborifySum
instance GArborifyProduct f U1 => GArborifySum (M1 c m f) tl where
gArborifySum (L1 (M1 a)) = Left (M1 (fst (gArborifyProduct @_ @U1 a)))
gArborifySum (R1 c) = Right c
class GArborifyProduct f tl where
gArborifyProduct :: LinearizeProduct f tl x -> (f x, tl x)
instance GArborifyProduct U1 tl where
gArborifyProduct c = (U1, c)
instance (GArborifyProduct g tl, GArborifyProduct f (LinearizeProduct g tl))
=> GArborifyProduct (f :*: g) tl where
gArborifyProduct abc = (a :*: b, c) where
(a, bc) = gArborifyProduct abc
(b, c) = gArborifyProduct bc
instance GArborifyProduct (M1 s m f) tl where
gArborifyProduct (a :*: c) = (a, c)
type family Arborify (f :: k -> Type) :: k -> Type
type instance Arborify (M1 D m f) = M1 D m (Eval (ArborifySum (CoArity f) f))
type instance Arborify (M1 C m f) = M1 C m (Eval (ArborifyProduct (Arity f) f))
data ArborifySum (n :: Nat) (f :: k -> Type) :: Exp (k -> Type)
type instance Eval (ArborifySum n V1) = V1
type instance Eval (ArborifySum n (f :+: g)) =
Eval (If (n == 1)
(ArborifyProduct (Arity f) f)
(Arborify' ArborifySum (:+:) n (Div n 2) f g))
data ArborifyProduct (n :: Nat) (f :: k -> Type) :: Exp (k -> Type)
type instance Eval (ArborifyProduct n (M1 C s f)) = M1 C s (Eval (ArborifyProduct n f))
type instance Eval (ArborifyProduct n U1) = U1
type instance Eval (ArborifyProduct n (f :*: g)) =
Eval (If (n == 1)
(Pure f)
(Arborify' ArborifyProduct (:*:) n (Div n 2) f g))
-- let nDiv2 = Div n 2 in ...
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 instance Lazify (M1 i m f) = M1 i (LazifyMeta m) (Lazify f)
type instance Lazify (f :*: g) = Lazify f :*: Lazify g
type instance Lazify (f :+: g) = Lazify f :+: Lazify g
type instance Lazify (K1 i c) = K1 i c
type instance Lazify U1 = U1
type instance Lazify V1 = V1
type family LazifyMeta (m :: Meta) :: Meta
type instance LazifyMeta ('MetaData n m p nt) = 'MetaData n m p nt
type instance LazifyMeta ('MetaCons n f s) = 'MetaCons n f s
type instance LazifyMeta ('MetaSel mn su ss ds)
= 'MetaSel mn 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy
data SplitAt :: Nat -> (k -> Type) -> Exp (k -> Type, k -> Type)
type instance Eval (SplitAt n (f :+: g)) =
Eval (If (n == 0)
(Pure '(V1, f :+: g))
(Bimap (Pure2 (:+:) f) Pure =<< SplitAt (n-1) g))
type instance Eval (SplitAt n (f :*: g)) =
Eval (If (n == 0)
(Pure '(U1, f :*: g))
(Bimap (Pure2 (:*:) f) Pure =<< SplitAt (n-1) g))
-- * Surgeries
-- | 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
-- Whenever you see
-- data ... :: MajorSurgery k
-- mentally expand it to
-- data ... (f :: k -> Type) :: Exp (k -> Type)
-- | @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
type instance Eval ((s :>> t) l) = Eval (t (Eval (s l)))
-- Note: This is a specialization of @(>=>)@ in Fcf.
type instance PerformL l (s :>> t) = (PerformL l s, PerformL (Eval (s l)) t)
infixl 1 :>>
-- | The identity surgery: doesn't do anything.
data IdSurgery :: MajorSurgery k
type instance Eval (IdSurgery l) = l
type instance PerformL l IdSurgery = ()
-- | 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 instance Eval (Suture l) = Linearize (Arborify l)
-- Now we can compose surgeries into complex ones, we can relate the input and
-- output of a whole surgery.
--
-- We still need to augment this with run-time information to 'Perform' the
-- surgery at the term level.
--
-- We might also need to interpret surgeries backwards (this is not entirely
-- symmetrical, a "removal" contains less information than an "insertion").
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)
instance 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 instance Eval (FieldTypeAt n (M1 i c f)) = Eval (FieldTypeAt n f)
type instance Eval (FieldTypeAt n (f :+: V1)) = Eval (FieldTypeAt n f)
type instance Eval (FieldTypeAt n (f :*: g)) =
Eval (If (n == 0) (Pure (FieldTypeOf f)) (FieldTypeAt (n-1) g))
type family FieldTypeOf (f :: k -> Type) :: Type
type instance FieldTypeOf (M1 s m (K1 i a)) = a
data FieldNameAt (n :: Nat) (f :: k -> Type) :: Exp (Maybe Symbol)
type instance Eval (FieldNameAt n (M1 i c f)) = Eval (FieldNameAt n f)
type instance Eval (FieldNameAt n (f :+: V1)) = Eval (FieldNameAt n f)
type instance Eval (FieldNameAt n (f :*: g)) =
Eval (If (n == 0) (FieldNameOf f) (FieldNameAt (n-1) g))
data FieldNameOf (f :: k -> Type) :: Exp (Maybe Symbol)
type instance Eval (FieldNameOf (M1 S ('MetaSel mn _ _ _) _)) = mn
data RemoveField (n :: Nat) (a :: Type) :: MajorSurgery k
type instance Eval (RemoveField n a f) = Eval (RemoveField_ n f)
-- | Like 'RemoveField' but without the explicit field type.
data RemoveField_ (n :: Nat) :: MajorSurgery k
type instance Eval (RemoveField_ n (M1 i m f)) = M1 i m (Eval (RemoveField_ n f))
type instance Eval (RemoveField_ n (f :+: V1)) = Eval (RemoveField_ n f) :+: V1
type instance Eval (RemoveField_ n (f :*: g)) =
Eval (If (n == 0) (Pure g) ((:*:) f <$> RemoveField_ (n-1) g))
type instance PerformL lt (RemoveField n a) = PerformL lt (RemoveFieldAt n (FieldNameAt n @@ lt) a)
data RemoveFieldAt (n :: Nat) (fd :: Maybe Symbol) (a :: Type) :: MajorSurgery k
type instance PerformL lt (RemoveFieldAt n fd a) =
PerformLRemoveFieldAt n fd a lt (Eval (RemoveField_ n lt))
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
instance PerformLRemoveFieldAt_ n fd t lt l => PerformLRemoveFieldAt n fd t lt l
data RemoveRField (fd :: Symbol) (a :: Type) :: MajorSurgery k
type instance Eval (RemoveRField fd a f) = Eval (RemoveField_ (Eval (FieldIndex fd f)) f)
type instance PerformL lt (RemoveRField fd a) =
PerformL lt (RemoveFieldAt (FieldIndex fd @@ lt) ('Just fd) a)
type DefaultMetaSel field
= 'MetaSel field 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy
data InsertField (n :: Nat) (fd :: Maybe Symbol) (t :: Type) :: MajorSurgery k
type instance Eval (InsertField n fd t (M1 D m f)) = M1 D m (Eval (InsertField n fd t f))
type instance Eval (InsertField n fd t (M1 C m f)) = M1 C m (Eval (InsertField n fd t f))
type instance Eval (InsertField n fd t (f :+: V1)) = Eval (InsertField n fd t f) :+: V1
type instance Eval (InsertField n fd t (f :*: g)) =
Eval (If (n == 0)
(Pure (M1 S (DefaultMetaSel fd) (K1 R t) :*: (f :*: g)))
((:*:) f <$> InsertField (n-1) fd t g))
type instance Eval (InsertField 0 fd t U1) = M1 S (DefaultMetaSel fd) (K1 R t) :*: U1
type instance PerformL l (InsertField n fd t) = PerformLInsert n fd t l (Eval (InsertField n fd t l))
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
instance PerformLInsert_ n fd t l tl => PerformLInsert n fd t l tl
type family CheckField (n :: Nat) (fd :: Maybe Symbol) (tl :: k -> Type) :: Constraint where
CheckField n 'Nothing tl = ()
CheckField n ('Just fd) tl = (n ~ Eval (FieldIndex fd tl))
data Succ :: Nat -> Exp Nat
type instance Eval (Succ n) = 1 + n
-- | Position of a record field
data FieldIndex (field :: Symbol) (f :: k -> Type) :: Exp Nat
type instance Eval (FieldIndex field (M1 D m f)) = Eval (FieldIndex field f)
type instance Eval (FieldIndex field (M1 C m f)) = Eval (FieldIndex field f)
type instance Eval (FieldIndex field (f :+: V1)) = Eval (FieldIndex field f)
type instance Eval (FieldIndex field (M1 S ('MetaSel ('Just field') su ss ds) f :*: g))
= Eval (If (field == field') (Pure 0) (Succ =<< FieldIndex field g))
-- | Number of fields of a single constructor
type family Arity (f :: k -> Type) :: Nat
type instance Arity (M1 d m f) = Arity f
type instance Arity (f :+: V1) = Arity f
type instance Arity (f :*: g) = Arity f + Arity g
type instance Arity (K1 i c) = 1
type instance Arity U1 = 0
-- | Number of constructors of a data type
type family CoArity (f :: k -> Type) :: Nat
type instance CoArity (M1 D m f) = CoArity f
type instance CoArity (M1 C m f) = 1
type instance CoArity V1 = 0
type instance CoArity (f :+: g) = CoArity f + CoArity g
class GRemoveField (n :: Nat) a f g where
gRemoveField :: f x -> (a, g x)
instance GRemoveField n a f g => GRemoveField n a (M1 i c f) (M1 i c g) where
gRemoveField (M1 a) = M1 <$> gRemoveField @n a
-- Only single-constructor types are supported for the moment.
instance GRemoveField n a f g => GRemoveField n a (f :+: V1) (g :+: V1) where
gRemoveField (L1 a) = L1 <$> gRemoveField @n a
gRemoveField (R1 v) = absurd1 v
instance GRemoveField 0 a (M1 s m (K1 i a) :*: f) f where
gRemoveField (M1 (K1 t) :*: b) = (t, b)
instance {-# OVERLAPPABLE #-}
( (n == 0) ~ 'False
, f0g ~ (f0 :*: g)
, GRemoveField (n-1) a f g
) => GRemoveField n a (f0 :*: f) f0g where
gRemoveField (a :*: b) = (a :*:) <$> gRemoveField @(n-1) b
class GInsertField (n :: Nat) a f g where
gInsertField :: a -> f x -> g x
instance GInsertField n a f g => GInsertField n a (M1 i c f) (M1 i c g) where
gInsertField t (M1 a) = M1 (gInsertField @n t a)
instance GInsertField n a f g => GInsertField n a (f :+: V1) (g :+: V1) where
gInsertField t (L1 a) = L1 (gInsertField @n t a)
gInsertField _ (R1 v) = absurd1 v
instance GInsertField 0 a f (M1 s m (K1 i a) :*: f) where
gInsertField t ab = M1 (K1 t) :*: ab
instance {-# OVERLAPPABLE #-}
( (n == 0) ~ 'False
, f0f ~ (f0 :*: f)
, GInsertField (n-1) a f g
) => GInsertField n a f0f (f0 :*: g) where
gInsertField t (a :*: b) = a :*: gInsertField @(n-1) t b
data ConstrAt (n :: Nat) (f :: k -> Type) :: Exp (k -> Type)
type instance Eval (ConstrAt n (M1 i m f)) = Eval (ConstrAt n f)
type instance Eval (ConstrAt n (f :+: g)) =
Eval (If (n == 0) (Pure f) (ConstrAt (n-1) g))
data RemoveConstr (c :: Symbol) (t :: Type) :: MajorSurgery k
type instance Eval (RemoveConstr c t l) = Eval (RemoveConstrAt c (ConstrIndex c @@ l) t l)
type instance PerformL lc (RemoveConstr c t) = PerformLRemoveConstr lc c (ConstrIndex c @@ lc) t
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
-- , l_t ~ Linearize (Arborify l_t)
, 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
instance 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
type instance Eval (RemoveConstrAt _ n t l) = Eval (RemoveUConstrAt n t l)
data RemoveUConstrAt (n :: Nat) (t :: Type) :: MajorSurgery k
type instance Eval (RemoveUConstrAt n _ l) = Eval (RemoveUConstrAt_ n l)
-- | Like 'RemoveConstr', but without the explicit constructor type.
data RemoveUConstrAt_ (n :: Nat) :: MajorSurgery k
type instance Eval (RemoveUConstrAt_ n (M1 i m f)) = M1 i m (Eval (RemoveUConstrAt_ n f))
type instance Eval (RemoveUConstrAt_ n (f :+: g)) =
Eval (If (n == 0) (Pure g) ((:+:) f <$> RemoveUConstrAt_ (n-1) g))
-- | 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 instance Eval (InsertConstrAt c n t l) = Eval (InsertUConstrAtL n (ConGraft c t) l)
type family ConGraft (c :: sym) (t :: ty) :: k -> Type
type instance ConGraft c (t :: Type) = RenameCon c (Linearize (UnM1 (Rep t)))
type family RenameCon (c :: sym) (t :: k -> Type) :: k -> Type
type instance RenameCon c (M1 C m f) = M1 C (RenameMeta c m) f
type family RenameMeta (c :: sym) (m :: Meta) :: Meta
type instance RenameMeta (s :: Symbol) ('MetaCons _ _ r) = 'MetaCons s 'PrefixI r
type instance PerformL l (InsertConstrAt c n t) = PerformLInsertConstrAt0 l c n t
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
instance PerformLInsertConstrAt_ c n t l_t l lc => PerformLInsertConstrAt c n t l_t l lc
data InsertUConstrAt (n :: Nat) (t :: Type) :: MajorSurgery k
type instance Eval (InsertUConstrAt n t l) = Eval (InsertUConstrAtL n (Linearize (UnM1 (Rep t))) l)
data InsertUConstrAtL (n :: Nat) (t :: k -> Type) :: MajorSurgery k
type instance Eval (InsertUConstrAtL n t (M1 i m f)) = M1 i m (Eval (InsertUConstrAtL n t f))
type instance Eval (InsertUConstrAtL n t (f :+: g)) =
Eval (If (n == 0) (Pure (t :+: (f :+: g))) ((:+:) f <$> InsertUConstrAtL (n-1) t g))
type instance Eval (InsertUConstrAtL 0 t V1) = t :+: V1
data ConstrIndex (con :: Symbol) (f :: k -> Type) :: Exp Nat
type instance Eval (ConstrIndex con (M1 D m f)) = Eval (ConstrIndex con f)
type instance Eval (ConstrIndex con (M1 C ('MetaCons con' fx s) f :+: g)) =
Eval (If (con == con') (Pure 0) (Succ =<< ConstrIndex con g))
class GRemoveConstr (n :: Nat) (t :: Type) f g where
gRemoveConstr :: f x -> Either t (g x)
instance GRemoveConstr n t f g => GRemoveConstr n t (M1 i c f) (M1 i c g) where
gRemoveConstr (M1 a) = M1 <$> gRemoveConstr @n a
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
constrArborify' = to @t @x . coerce (gArborify @(UnM1 (Rep t)) @x)
instance ConstrArborify t l => GRemoveConstr 0 t (l :+: f) f where
gRemoveConstr (L1 a) = Left (constrArborify' a)
gRemoveConstr (R1 b) = Right b
instance {-# OVERLAPPABLE #-}
( GRemoveConstr (n-1) t f g, (n == 0) ~ 'False
, f0g ~ (f0 :+: g)
) => GRemoveConstr n t (f0 :+: f) f0g where
gRemoveConstr (L1 a) = Right (L1 a)
gRemoveConstr (R1 b) = R1 <$> gRemoveConstr @(n-1) b
class GInsertConstr (n :: Nat) (t :: Type) f g where
gInsertConstr :: Either t (f x) -> g x
instance GInsertConstr n t f g => GInsertConstr n t (M1 i c f) (M1 i c g) where
gInsertConstr = M1 . gInsertConstr @n . fmap unM1
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
constrLinearize' = coerce (gLinearize @(UnM1 (Rep t)) @x) . from @t @x
instance ConstrLinearize t l => GInsertConstr 0 t f (l :+: f) where
gInsertConstr (Left a) = L1 (constrLinearize' a)
gInsertConstr (Right b) = R1 b
instance {-# OVERLAPPABLE #-}
( GInsertConstr (n-1) t f g, (n == 0) ~ 'False
, f0f ~ (f0 :+: f)
) => GInsertConstr n t f0f (f0 :+: g) where
gInsertConstr (Left a) = R1 (gInsertConstr @(n-1) @t @f @g (Left a))
gInsertConstr (Right (L1 a)) = L1 a
gInsertConstr (Right (R1 b)) = R1 (gInsertConstr @(n-1) @t @f @g (Right b))
-- | Equate two generic representations, but ignoring constructor and field metadata.
class MatchFields (f :: k -> Type) (g :: k -> Type)
instance (g ~ M1 D c g', MatchFields f' g') => MatchFields (M1 D c f') g
instance (g ~ M1 C ('MetaCons _x _y _z) g', MatchFields f' g') => MatchFields (M1 C c f') g
instance (g ~ M1 S ('MetaSel _w _x _y _z) g', MatchFields f' g') => MatchFields (M1 S c f') g
instance (g ~ (g1 :+: g2), MatchFields f1 g1, MatchFields f2 g2) => MatchFields (f1 :+: f2) g
instance (g ~ (g1 :*: g2), MatchFields f1 g1, MatchFields f2 g2) => MatchFields (f1 :*: f2) g
instance (g ~ K1 i a) => MatchFields (K1 i a) g
instance (g ~ U1) => MatchFields U1 g
instance (g ~ V1) => MatchFields V1 g
class IsTuple (n :: Nat) (t :: k)
instance (t ~ ()) => IsTuple 0 t
instance (t ~ Identity a) => IsTuple 1 t
instance (t ~ (a, b)) => IsTuple 2 t
instance (t ~ (a, b, c)) => IsTuple 3 t
instance (t ~ (a, b, c, d)) => IsTuple 4 t
instance (t ~ (a, b, c, d, e)) => IsTuple 5 t
instance (t ~ (a, b, c, d, e, f)) => IsTuple 6 t
instance (t ~ (a, b, c, d, e, f, g)) => IsTuple 7 t