{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Composite.Record
( Rec((:&), RNil), Record
, pattern (:*:), pattern (:^:), pattern (:!:)
, (:->)(Val, getVal), _Val, val, valName, valWithName
, RElem, rlens, rlens', rlensCo, rlensContra
, AllHave, HasInstances, ValuesAllHave
, zipRecsWith, reifyDicts, reifyVal, recordToNonEmpty
, ReifyNames(reifyNames)
, RecWithContext(rmapWithContext)
, RDelete, RDeletable, rdelete
) where
import Control.DeepSeq(NFData(rnf))
import Control.Lens (Iso, iso)
import Control.Lens.TH (makeWrapped)
import Data.Functor.Identity (Identity(Identity))
import Data.Functor.Contravariant (Contravariant(contramap))
import Data.Kind (Constraint, Type)
import Data.List.NonEmpty (NonEmpty((:|)))
import Data.Proxy (Proxy(Proxy))
import Data.String (IsString)
import Data.Text (Text, pack)
import Data.Vinyl (Rec((:&), RNil), RecApplicative, rcast, recordToList, rpure)
import qualified Data.Vinyl as Vinyl
import Data.Vinyl.Functor (Compose(Compose), Const(Const), (:.))
import Data.Vinyl.Lens (type (∈), type (⊆))
import qualified Data.Vinyl.TypeLevel as Vinyl
import Data.Vinyl.XRec(IsoHKD(HKD, toHKD, unHKD))
import Foreign.Storable (Storable)
import GHC.TypeLits (KnownSymbol, Symbol, symbolVal)
type Record = Rec Identity
type RElem r rs = Vinyl.RElem r rs (Vinyl.RIndex r rs)
newtype (:->) (s :: Symbol) a = Val { forall (s :: Symbol) a. (s :-> a) -> a
getVal :: a }
_Val :: Iso (s :-> a) (s :-> b) a b
_Val :: forall (s :: Symbol) a b. Iso (s :-> a) (s :-> b) a b
_Val = forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso forall (s :: Symbol) a. (s :-> a) -> a
getVal forall (s :: Symbol) a. a -> s :-> a
Val
makeWrapped ''(:->)
deriving instance Bounded a => Bounded (s :-> a)
deriving instance Enum a => Enum (s :-> a)
deriving instance Eq a => Eq (s :-> a)
deriving instance Floating a => Floating (s :-> a)
deriving instance Fractional a => Fractional (s :-> a)
deriving instance Integral a => Integral (s :-> a)
deriving instance IsString a => IsString (s :-> a)
deriving instance Monoid a => Monoid (s :-> a)
deriving instance Num a => Num (s :-> a)
deriving instance Ord a => Ord (s :-> a)
deriving instance Real a => Real (s :-> a)
deriving instance RealFloat a => RealFloat (s :-> a)
deriving instance RealFrac a => RealFrac (s :-> a)
deriving instance Semigroup a => Semigroup (s :-> a)
deriving instance Storable a => Storable (s :-> a)
instance Functor ((:->) s) where
fmap :: forall a b. (a -> b) -> (s :-> a) -> s :-> b
fmap a -> b
f = forall (s :: Symbol) a. a -> s :-> a
Val forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: Symbol) a. (s :-> a) -> a
getVal
{-# INLINE fmap #-}
instance Applicative ((:->) s) where
pure :: forall a. a -> s :-> a
pure = forall (s :: Symbol) a. a -> s :-> a
Val
{-# INLINE pure #-}
Val a -> b
f <*> :: forall a b. (s :-> (a -> b)) -> (s :-> a) -> s :-> b
<*> Val a
a = forall (s :: Symbol) a. a -> s :-> a
Val (a -> b
f a
a)
{-# INLINE (<*>) #-}
instance Foldable ((:->) s) where
foldr :: forall a b. (a -> b -> b) -> b -> (s :-> a) -> b
foldr a -> b -> b
f b
z (Val a
a) = a -> b -> b
f a
a b
z
{-# INLINE foldr #-}
instance Traversable ((:->) s) where
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (s :-> a) -> f (s :-> b)
traverse a -> f b
k (Val a
a) = forall (s :: Symbol) a. a -> s :-> a
Val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
k a
a
{-# INLINE traverse #-}
instance Monad ((:->) s) where
return :: forall a. a -> s :-> a
return = forall (f :: * -> *) a. Applicative f => a -> f a
pure
{-# INLINE return #-}
Val a
a >>= :: forall a b. (s :-> a) -> (a -> s :-> b) -> s :-> b
>>= a -> s :-> b
k = a -> s :-> b
k a
a
{-# INLINE (>>=) #-}
instance NFData a => NFData (s :-> a) where
rnf :: (s :-> a) -> ()
rnf (Val a
x) = forall a. NFData a => a -> ()
rnf a
x
instance NFData (Record '[]) where
rnf :: Record '[] -> ()
rnf Record '[]
RNil = ()
instance (NFData x, NFData (Record xs)) => NFData (Record (x : xs)) where
rnf :: Record (x : xs) -> ()
rnf (Identity r
x :& Rec Identity rs
xs) = forall a. NFData a => a -> ()
rnf Identity r
x seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf Rec Identity rs
xs
instance forall (s :: Symbol) a. (KnownSymbol s, Show a) => Show (s :-> a) where
showsPrec :: Int -> (s :-> a) -> ShowS
showsPrec Int
p (Val a
a) = ((forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy s) forall a. [a] -> [a] -> [a]
++ String
" :-> ") forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
p a
a
instance KnownSymbol s => IsoHKD Identity (s :-> a) where
type HKD Identity (s :-> a) = a
unHKD :: HKD Identity (s :-> a) -> Identity (s :-> a)
unHKD = forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: Symbol) a. a -> s :-> a
Val
toHKD :: Identity (s :-> a) -> HKD Identity (s :-> a)
toHKD (Identity (Val a
x)) = a
x
val :: forall (s :: Symbol) a. a -> Identity (s :-> a)
val :: forall (s :: Symbol) a. a -> Identity (s :-> a)
val = forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: Symbol) a. a -> s :-> a
Val @s
valName :: forall s a. KnownSymbol s => s :-> a -> Text
valName :: forall (s :: Symbol) a. KnownSymbol s => (s :-> a) -> Text
valName s :-> a
_ = String -> Text
pack (forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy s))
{-# INLINE valName #-}
valWithName :: forall s a. KnownSymbol s => s :-> a -> (Text, a)
valWithName :: forall (s :: Symbol) a. KnownSymbol s => (s :-> a) -> (Text, a)
valWithName s :-> a
v = (forall (s :: Symbol) a. KnownSymbol s => (s :-> a) -> Text
valName s :-> a
v, forall (s :: Symbol) a. (s :-> a) -> a
getVal s :-> a
v)
{-# INLINE valWithName #-}
pattern (:*:) :: () => () => a -> Rec Identity rs -> Rec Identity (s :-> a ': rs)
pattern $b:*: :: forall a (rs :: [*]) (s :: Symbol).
a -> Rec Identity rs -> Rec Identity ((s :-> a) : rs)
$m:*: :: forall {r} {a} {rs :: [*]} {s :: Symbol}.
Rec Identity ((s :-> a) : rs)
-> (a -> Rec Identity rs -> r) -> ((# #) -> r) -> r
(:*:) a rs = Identity (Val a) :& rs
infixr 5 :*:
pattern (:^:) :: Functor f => () => f a -> Rec f rs -> Rec f (s :-> a ': rs)
pattern $b:^: :: forall (f :: * -> *) a (rs :: [*]) (s :: Symbol).
Functor f =>
f a -> Rec f rs -> Rec f ((s :-> a) : rs)
$m:^: :: forall {r} {f :: * -> *} {a} {rs :: [*]} {s :: Symbol}.
Functor f =>
Rec f ((s :-> a) : rs)
-> (f a -> Rec f rs -> r) -> ((# #) -> r) -> r
(:^:) fa rs <- (fmap getVal -> fa) :& rs where
(:^:) f a
fa Rec f rs
rs = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (s :: Symbol) a. a -> s :-> a
Val f a
fa forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec f rs
rs
infixr 5 :^:
pattern (:!:) :: Contravariant f => () => f a -> Rec f rs -> Rec f (s :-> a ': rs)
pattern $b:!: :: forall (f :: * -> *) a (rs :: [*]) (s :: Symbol).
Contravariant f =>
f a -> Rec f rs -> Rec f ((s :-> a) : rs)
$m:!: :: forall {r} {f :: * -> *} {a} {rs :: [*]} {s :: Symbol}.
Contravariant f =>
Rec f ((s :-> a) : rs)
-> (f a -> Rec f rs -> r) -> ((# #) -> r) -> r
(:!:) fa rs <- (contramap Val -> fa) :& rs where
(:!:) f a
fa Rec f rs
rs = forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap forall (s :: Symbol) a. (s :-> a) -> a
getVal f a
fa forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec f rs
rs
infixr 5 :!:
reifyVal :: proxy (s :-> a) -> (s :-> a) -> (s :-> a)
reifyVal :: forall (proxy :: * -> *) (s :: Symbol) a.
proxy (s :-> a) -> (s :-> a) -> s :-> a
reifyVal proxy (s :-> a)
_ = forall a. a -> a
id
rlens :: (Functor g, RElem (s :-> a) rs, Functor g) => proxy (s :-> a) -> (a -> g a) -> Rec Identity rs -> g (Rec Identity rs)
rlens :: forall (g :: * -> *) (s :: Symbol) a (rs :: [*]) (proxy :: * -> *).
(Functor g, RElem (s :-> a) rs, Functor g) =>
proxy (s :-> a)
-> (a -> g a) -> Rec Identity rs -> g (Rec Identity rs)
rlens proxy (s :-> a)
proxy a -> g a
f =
forall {k} (r :: k) (record :: (k -> *) -> [k] -> *) (rs :: [k])
(f :: k -> *) (g :: * -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f,
Functor g) =>
(f r -> g (f r)) -> record f rs -> g (record f rs)
Vinyl.rlens forall a b. (a -> b) -> a -> b
$ \ (Identity (forall (s :: Symbol) a. (s :-> a) -> a
getVal forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (proxy :: * -> *) (s :: Symbol) a.
proxy (s :-> a) -> (s :-> a) -> s :-> a
reifyVal proxy (s :-> a)
proxy -> a
a)) ->
forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: Symbol) a. a -> s :-> a
Val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> g a
f a
a
{-# INLINE rlens #-}
rlensCo :: (Functor f, Functor g, RElem (s :-> a) rs) => proxy (s :-> a) -> (f a -> g (f a)) -> Rec f rs -> g (Rec f rs)
rlensCo :: forall (f :: * -> *) (g :: * -> *) (s :: Symbol) a (rs :: [*])
(proxy :: * -> *).
(Functor f, Functor g, RElem (s :-> a) rs) =>
proxy (s :-> a) -> (f a -> g (f a)) -> Rec f rs -> g (Rec f rs)
rlensCo proxy (s :-> a)
proxy f a -> g (f a)
f =
forall {k} (r :: k) (record :: (k -> *) -> [k] -> *) (rs :: [k])
(f :: k -> *) (g :: * -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f,
Functor g) =>
(f r -> g (f r)) -> record f rs -> g (record f rs)
Vinyl.rlens forall a b. (a -> b) -> a -> b
$ \ (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (s :: Symbol) a. (s :-> a) -> a
getVal forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (proxy :: * -> *) (s :: Symbol) a.
proxy (s :-> a) -> (s :-> a) -> s :-> a
reifyVal proxy (s :-> a)
proxy) -> f a
fa) ->
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (s :: Symbol) a. a -> s :-> a
Val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a -> g (f a)
f f a
fa
{-# INLINE rlensCo #-}
rlens' :: (Functor f, Functor g, RElem (s :-> a) rs) => proxy (s :-> a) -> (f a -> g (f a)) -> Rec f rs -> g (Rec f rs)
rlens' :: forall (f :: * -> *) (g :: * -> *) (s :: Symbol) a (rs :: [*])
(proxy :: * -> *).
(Functor f, Functor g, RElem (s :-> a) rs) =>
proxy (s :-> a) -> (f a -> g (f a)) -> Rec f rs -> g (Rec f rs)
rlens' = forall (f :: * -> *) (g :: * -> *) (s :: Symbol) a (rs :: [*])
(proxy :: * -> *).
(Functor f, Functor g, RElem (s :-> a) rs) =>
proxy (s :-> a) -> (f a -> g (f a)) -> Rec f rs -> g (Rec f rs)
rlensCo
{-# INLINE rlens' #-}
rlensContra :: (Contravariant f, Functor g, RElem (s :-> a) rs) => proxy (s :-> a) -> (f a -> g (f a)) -> Rec f rs -> g (Rec f rs)
rlensContra :: forall (f :: * -> *) (g :: * -> *) (s :: Symbol) a (rs :: [*])
(proxy :: * -> *).
(Contravariant f, Functor g, RElem (s :-> a) rs) =>
proxy (s :-> a) -> (f a -> g (f a)) -> Rec f rs -> g (Rec f rs)
rlensContra proxy (s :-> a)
proxy f a -> g (f a)
f =
forall {k} (r :: k) (record :: (k -> *) -> [k] -> *) (rs :: [k])
(f :: k -> *) (g :: * -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f,
Functor g) =>
(f r -> g (f r)) -> record f rs -> g (record f rs)
Vinyl.rlens forall a b. (a -> b) -> a -> b
$ \(forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap (forall (proxy :: * -> *) (s :: Symbol) a.
proxy (s :-> a) -> (s :-> a) -> s :-> a
reifyVal proxy (s :-> a)
proxy forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: Symbol) a. a -> s :-> a
Val) -> f a
fa) ->
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap forall (s :: Symbol) a. (s :-> a) -> a
getVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a -> g (f a)
f f a
fa
{-# INLINE rlensContra #-}
zipRecsWith :: (forall a. f a -> g a -> h a) -> Rec f as -> Rec g as -> Rec h as
zipRecsWith :: forall {u} (f :: u -> *) (g :: u -> *) (h :: u -> *) (as :: [u]).
(forall (a :: u). f a -> g a -> h a)
-> Rec f as -> Rec g as -> Rec h as
zipRecsWith forall (a :: u). f a -> g a -> h a
_ Rec f as
RNil Rec g as
_ = forall {u} (a :: u -> *). Rec a '[]
RNil
zipRecsWith forall (a :: u). f a -> g a -> h a
f (f r
r :& Rec f rs
rs) (g r
s :& Rec g rs
ss) = forall (a :: u). f a -> g a -> h a
f f r
r g r
s forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& forall {u} (f :: u -> *) (g :: u -> *) (h :: u -> *) (as :: [u]).
(forall (a :: u). f a -> g a -> h a)
-> Rec f as -> Rec g as -> Rec h as
zipRecsWith forall (a :: u). f a -> g a -> h a
f Rec f rs
rs Rec g rs
ss
recordToNonEmpty :: Vinyl.RecordToList rs => Rec (Const a) (r ': rs) -> NonEmpty a
recordToNonEmpty :: forall {u} (rs :: [u]) a (r :: u).
RecordToList rs =>
Rec (Const a) (r : rs) -> NonEmpty a
recordToNonEmpty (Const a
a :& Rec (Const a) rs
rs) = a
a forall a. a -> [a] -> NonEmpty a
:| forall {u} (rs :: [u]) a.
RecordToList rs =>
Rec (Const a) rs -> [a]
recordToList Rec (Const a) rs
rs
type family HasInstances (a :: u) (cs :: [u -> Constraint]) :: Constraint where
HasInstances a '[] = ()
HasInstances a (c ': cs) = (c a, HasInstances a cs)
type family AllHave (cs :: [u -> Constraint]) (as :: [u]) :: Constraint where
AllHave cs '[] = ()
AllHave cs (a ': as) = (HasInstances a cs, AllHave cs as)
type family ValuesAllHave (cs :: [u -> Constraint]) (as :: [u]) :: Constraint where
ValuesAllHave cs '[] = ()
ValuesAllHave cs (s :-> a ': as) = (HasInstances a cs, ValuesAllHave cs as)
reifyDicts
:: forall u. forall (cs :: [u -> Constraint]) (f :: u -> Type) (rs :: [u]) (proxy :: [u -> Constraint] -> Type).
(AllHave cs rs, RecApplicative rs)
=> proxy cs
-> (forall proxy' (a :: u). HasInstances a cs => proxy' a -> f a)
-> Rec f rs
reifyDicts :: forall u (cs :: [u -> Constraint]) (f :: u -> *) (rs :: [u])
(proxy :: [u -> Constraint] -> *).
(AllHave cs rs, RecApplicative rs) =>
proxy cs
-> (forall (proxy' :: u -> *) (a :: u).
HasInstances a cs =>
proxy' a -> f a)
-> Rec f rs
reifyDicts proxy cs
x forall (proxy' :: u -> *) (a :: u).
HasInstances a cs =>
proxy' a -> f a
f = forall (f :: u -> *) (cs :: [u -> Constraint]) (rs' :: [u])
(proxy :: [u -> Constraint] -> *).
AllHave cs rs' =>
proxy cs
-> Rec (Const ()) rs'
-> (forall (proxy' :: u -> *) (a :: u).
HasInstances a cs =>
proxy' a -> f a)
-> Rec f rs'
go proxy cs
x (forall {u} (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
(forall (x :: u). f x) -> Rec f rs
rpure (forall k a (b :: k). a -> Const a b
Const ())) forall (proxy' :: u -> *) (a :: u).
HasInstances a cs =>
proxy' a -> f a
f
where
go :: forall (f :: u -> Type) (cs :: [u -> Constraint]) (rs' :: [u]) (proxy :: [u -> Constraint] -> Type). AllHave cs rs'
=> proxy cs
-> Rec (Const ()) rs'
-> (forall proxy' (a :: u). HasInstances a cs => proxy' a -> f a)
-> Rec f rs'
go :: forall (f :: u -> *) (cs :: [u -> Constraint]) (rs' :: [u])
(proxy :: [u -> Constraint] -> *).
AllHave cs rs' =>
proxy cs
-> Rec (Const ()) rs'
-> (forall (proxy' :: u -> *) (a :: u).
HasInstances a cs =>
proxy' a -> f a)
-> Rec f rs'
go proxy cs
_ Rec (Const ()) rs'
RNil forall (proxy' :: u -> *) (a :: u).
HasInstances a cs =>
proxy' a -> f a
_ = forall {u} (a :: u -> *). Rec a '[]
RNil
go proxy cs
y ((Const () r
_ :: Const () a) :& Rec (Const ()) rs
ys) forall (proxy' :: u -> *) (a :: u).
HasInstances a cs =>
proxy' a -> f a
g = forall (proxy' :: u -> *) (a :: u).
HasInstances a cs =>
proxy' a -> f a
g (forall {k} (t :: k). Proxy t
Proxy @a) forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& forall (f :: u -> *) (cs :: [u -> Constraint]) (rs' :: [u])
(proxy :: [u -> Constraint] -> *).
AllHave cs rs' =>
proxy cs
-> Rec (Const ()) rs'
-> (forall (proxy' :: u -> *) (a :: u).
HasInstances a cs =>
proxy' a -> f a)
-> Rec f rs'
go proxy cs
y Rec (Const ()) rs
ys forall (proxy' :: u -> *) (a :: u).
HasInstances a cs =>
proxy' a -> f a
g
{-# INLINE reifyDicts #-}
class ReifyNames (rs :: [Type]) where
reifyNames :: Rec f rs -> Rec ((,) Text :. f) rs
instance ReifyNames '[] where
reifyNames :: forall (f :: * -> *). Rec f '[] -> Rec ((,) Text :. f) '[]
reifyNames Rec f '[]
_ = forall {u} (a :: u -> *). Rec a '[]
RNil
instance forall (s :: Symbol) a (rs :: [Type]). (KnownSymbol s, ReifyNames rs) => ReifyNames (s :-> a ': rs) where
reifyNames :: forall (f :: * -> *).
Rec f ((s :-> a) : rs) -> Rec ((,) Text :. f) ((s :-> a) : rs)
reifyNames (f r
fa :& Rec f rs
rs) = forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose ((,) (String -> Text
pack forall a b. (a -> b) -> a -> b
$ forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
Proxy @s)) f r
fa) forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& forall (rs :: [*]) (f :: * -> *).
ReifyNames rs =>
Rec f rs -> Rec ((,) Text :. f) rs
reifyNames Rec f rs
rs
class RecWithContext (ss :: [Type]) (ts :: [Type]) where
rmapWithContext :: proxy ss -> (forall r. r ∈ ss => f r -> g r) -> Rec f ts -> Rec g ts
instance RecWithContext ss '[] where
rmapWithContext :: forall (proxy :: [*] -> *) (f :: * -> *) (g :: * -> *).
proxy ss
-> (forall r. (r ∈ ss) => f r -> g r) -> Rec f '[] -> Rec g '[]
rmapWithContext proxy ss
_ forall r. (r ∈ ss) => f r -> g r
_ Rec f '[]
_ = forall {u} (a :: u -> *). Rec a '[]
RNil
instance forall r (ss :: [Type]) (ts :: [Type]). (r ∈ ss, RecWithContext ss ts) => RecWithContext ss (r ': ts) where
rmapWithContext :: forall (proxy :: [*] -> *) (f :: * -> *) (g :: * -> *).
proxy ss
-> (forall r. (r ∈ ss) => f r -> g r)
-> Rec f (r : ts)
-> Rec g (r : ts)
rmapWithContext proxy ss
proxy forall r. (r ∈ ss) => f r -> g r
n (f r
r :& Rec f rs
rs) = forall r. (r ∈ ss) => f r -> g r
n f r
r forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& forall (ss :: [*]) (ts :: [*]) (proxy :: [*] -> *) (f :: * -> *)
(g :: * -> *).
RecWithContext ss ts =>
proxy ss
-> (forall r. (r ∈ ss) => f r -> g r) -> Rec f ts -> Rec g ts
rmapWithContext proxy ss
proxy forall r. (r ∈ ss) => f r -> g r
n Rec f rs
rs
type family RDelete (r :: u) (rs :: [u]) where
RDelete r (r ': rs) = rs
RDelete r (s ': rs) = s ': RDelete r rs
type RDeletable r rs = (r ∈ rs, RDelete r rs ⊆ rs)
rdelete :: RDeletable r rs => proxy r -> Rec f rs -> Rec f (RDelete r rs)
rdelete :: forall {u} (r :: u) (rs :: [u]) (proxy :: u -> *) (f :: u -> *).
RDeletable r rs =>
proxy r -> Rec f rs -> Rec f (RDelete r rs)
rdelete proxy r
_ = forall {k1} {k2} (rs :: [k1]) (ss :: [k1]) (f :: k2 -> *)
(record :: (k2 -> *) -> [k1] -> *) (is :: [Nat]).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f ss -> record f rs
rcast