{-# LANGUAGE ConstraintKinds, DataKinds, FlexibleContexts, FlexibleInstances,
KindSignatures, MultiParamTypeClasses, PolyKinds,
ScopedTypeVariables, TypeFamilies, TypeOperators,
UndecidableInstances, TemplateHaskell, QuasiQuotes,
Rank2Types, TypeApplications, AllowAmbiguousTypes #-}
module Frames.Joins (innerJoin
, outerJoin
, leftJoin
, rightJoin)
where
import Data.Discrimination
import Data.Foldable as F
import Frames.Frame
import Frames.Rec
import Frames.InCore (toFrame)
import Frames.Melt (RDeleteAll)
import Frames.InCore (RecVec)
import Data.Vinyl.TypeLevel
import Data.Vinyl
import Data.Vinyl.Functor
mergeRec :: forall fs rs rs2 rs2'.
(fs ⊆ rs2
, rs2' ⊆ rs2
, rs2' ~ RDeleteAll fs rs2
, rs ⊆ (rs ++ rs2')) =>
Record rs ->
Record rs2 ->
Record (rs ++ rs2')
{-# INLINE mergeRec #-}
mergeRec :: Record rs -> Record rs2 -> Record (rs ++ rs2')
mergeRec Record rs
rec1 Record rs2
rec2 =
Record rs
rec1 Record rs -> Rec ElField rs2' -> Record (rs ++ rs2')
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Rec ElField rs2'
rec2'
where
rec2' :: Rec ElField rs2'
rec2' = Record rs2 -> Rec ElField rs2'
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 @rs2' Record rs2
rec2
innerJoin :: forall fs rs rs2 rs2'.
(fs ⊆ rs
, fs ⊆ rs2
, rs ⊆ (rs ++ rs2')
, rs2' ⊆ rs2
, rs2' ~ RDeleteAll fs rs2
, Grouping (Record fs)
, RecVec rs
, RecVec rs2'
, RecVec (rs ++ rs2')
) =>
Frame (Record rs)
-> Frame (Record rs2)
-> Frame (Record (rs ++ rs2'))
innerJoin :: Frame (Record rs)
-> Frame (Record rs2) -> Frame (Record (rs ++ rs2'))
innerJoin Frame (Record rs)
a Frame (Record rs2)
b =
[Record (rs ++ rs2')] -> Frame (Record (rs ++ rs2'))
forall (f :: * -> *) (rs :: [(Symbol, *)]).
(Foldable f, RecVec rs) =>
f (Record rs) -> Frame (Record rs)
toFrame ([Record (rs ++ rs2')] -> Frame (Record (rs ++ rs2')))
-> [Record (rs ++ rs2')] -> Frame (Record (rs ++ rs2'))
forall a b. (a -> b) -> a -> b
$
[[Record (rs ++ rs2')]] -> [Record (rs ++ rs2')]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
(Group (Rec ElField fs)
-> (Record rs -> Record rs2 -> Record (rs ++ rs2'))
-> (Record rs -> Rec ElField fs)
-> (Record rs2 -> Rec ElField fs)
-> [Record rs]
-> [Record rs2]
-> [[Record (rs ++ rs2')]]
forall (f :: * -> *) d a b c.
Discriminating f =>
f d -> (a -> b -> c) -> (a -> d) -> (b -> d) -> [a] -> [b] -> [[c]]
inner Group (Rec ElField fs)
forall a. Grouping a => Group a
grouping Record rs -> Record rs2 -> Record (rs ++ rs2')
mergeFun Record rs -> Rec ElField fs
proj1 Record rs2 -> Rec ElField fs
proj2 (Frame (Record rs) -> [Record rs]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Frame (Record rs)
a) (Frame (Record rs2) -> [Record rs2]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Frame (Record rs2)
b))
where
{-# INLINE mergeFun #-}
mergeFun :: Record rs -> Record rs2 -> Record (rs ++ rs2')
mergeFun = forall (rs :: [(Symbol, *)]) (rs2 :: [(Symbol, *)])
(rs2' :: [(Symbol, *)]).
(fs ⊆ rs2, rs2' ⊆ rs2, rs2' ~ RDeleteAll fs rs2,
rs ⊆ (rs ++ rs2')) =>
Record rs -> Record rs2 -> Record (rs ++ rs2')
forall (fs :: [(Symbol, *)]) (rs :: [(Symbol, *)])
(rs2 :: [(Symbol, *)]) (rs2' :: [(Symbol, *)]).
(fs ⊆ rs2, rs2' ⊆ rs2, rs2' ~ RDeleteAll fs rs2,
rs ⊆ (rs ++ rs2')) =>
Record rs -> Record rs2 -> Record (rs ++ rs2')
mergeRec @fs
{-# INLINE proj1 #-}
proj1 :: Record rs -> Rec ElField fs
proj1 = forall (ss :: [(Symbol, *)]) (f :: (Symbol, *) -> *)
(record :: ((Symbol, *) -> *) -> [(Symbol, *)] -> *) (is :: [Nat]).
(RecSubset record fs ss is, RecSubsetFCtx record f) =>
record f ss -> record f fs
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 @fs
{-# INLINE proj2 #-}
proj2 :: Record rs2 -> Rec ElField fs
proj2 = forall (ss :: [(Symbol, *)]) (f :: (Symbol, *) -> *)
(record :: ((Symbol, *) -> *) -> [(Symbol, *)] -> *) (is :: [Nat]).
(RecSubset record fs ss is, RecSubsetFCtx record f) =>
record f ss -> record f fs
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 @fs
justsFromRec :: RMap fs => Record fs -> Rec (Maybe :. ElField) fs
{-# INLINE justsFromRec #-}
justsFromRec :: Record fs -> Rec (Maybe :. ElField) fs
justsFromRec = (forall (x :: (Symbol, *)). ElField x -> (:.) Maybe ElField x)
-> Record fs -> Rec (Maybe :. ElField) fs
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap (Maybe (ElField x) -> Compose Maybe ElField x
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose (Maybe (ElField x) -> Compose Maybe ElField x)
-> (ElField x -> Maybe (ElField x))
-> ElField x
-> Compose Maybe ElField x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ElField x -> Maybe (ElField x)
forall a. a -> Maybe a
Just)
mkNothingsRec :: forall fs.
(RecApplicative fs) =>
Rec (Maybe :. ElField) fs
{-# INLINE mkNothingsRec #-}
mkNothingsRec :: Rec (Maybe :. ElField) fs
mkNothingsRec = (forall (x :: (Symbol, *)). (:.) Maybe ElField x)
-> Rec (Maybe :. ElField) fs
forall u (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
(forall (x :: u). f x) -> Rec f rs
rpure @fs (Maybe (ElField x) -> Compose Maybe ElField x
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose Maybe (ElField x)
forall a. Maybe a
Nothing)
outerJoin :: forall fs rs rs' rs2 rs2' ors.
(fs ⊆ rs
, fs ⊆ rs2
, rs ⊆ (rs ++ rs2')
, rs' ⊆ rs
, rs' ~ RDeleteAll fs rs
, rs2' ⊆ rs2
, rs2' ~ RDeleteAll fs rs2
, ors ~ (rs ++ rs2')
, ors :~: (rs' ++ rs2)
, RecApplicative rs2'
, RecApplicative rs
, RecApplicative rs'
, Grouping (Record fs)
, RMap rs
, RMap rs2
, RMap ors
, RecVec rs
, RecVec rs2'
, RecVec ors
) =>
Frame (Record rs)
-> Frame (Record rs2)
-> [Rec (Maybe :. ElField) ors]
outerJoin :: Frame (Record rs)
-> Frame (Record rs2) -> [Rec (Maybe :. ElField) ors]
outerJoin Frame (Record rs)
a Frame (Record rs2)
b =
[[Rec (Maybe :. ElField) ors]] -> [Rec (Maybe :. ElField) ors]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
(Group (Rec ElField fs)
-> (Record rs -> Record rs2 -> Rec (Maybe :. ElField) ors)
-> (Record rs -> Rec (Maybe :. ElField) ors)
-> (Record rs2 -> Rec (Maybe :. ElField) ors)
-> (Record rs -> Rec ElField fs)
-> (Record rs2 -> Rec ElField fs)
-> [Record rs]
-> [Record rs2]
-> [[Rec (Maybe :. ElField) ors]]
forall (f :: * -> *) d a b c.
Discriminating f =>
f d
-> (a -> b -> c)
-> (a -> c)
-> (b -> c)
-> (a -> d)
-> (b -> d)
-> [a]
-> [b]
-> [[c]]
outer Group (Rec ElField fs)
forall a. Grouping a => Group a
grouping Record rs -> Record rs2 -> Rec (Maybe :. ElField) ors
mergeFun Record rs -> Rec (Maybe :. ElField) ors
Record rs -> Rec (Maybe :. ElField) (rs ++ rs2')
mergeLeftEmpty Record rs2 -> Rec (Maybe :. ElField) ors
mergeRightEmpty
Record rs -> Rec ElField fs
proj1 Record rs2 -> Rec ElField fs
proj2 (Frame (Record rs) -> [Record rs]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Frame (Record rs)
a) (Frame (Record rs2) -> [Record rs2]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Frame (Record rs2)
b))
where
{-# INLINE proj1 #-}
proj1 :: Record rs -> Rec ElField fs
proj1 = forall (ss :: [(Symbol, *)]) (f :: (Symbol, *) -> *)
(record :: ((Symbol, *) -> *) -> [(Symbol, *)] -> *) (is :: [Nat]).
(RecSubset record fs ss is, RecSubsetFCtx record f) =>
record f ss -> record f fs
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 @fs
{-# INLINE proj2 #-}
proj2 :: Record rs2 -> Rec ElField fs
proj2 = forall (ss :: [(Symbol, *)]) (f :: (Symbol, *) -> *)
(record :: ((Symbol, *) -> *) -> [(Symbol, *)] -> *) (is :: [Nat]).
(RecSubset record fs ss is, RecSubsetFCtx record f) =>
record f ss -> record f fs
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 @fs
{-# INLINE mergeFun #-}
mergeFun :: Record rs -> Record rs2 -> Rec (Maybe :. ElField) ors
mergeFun Record rs
l Record rs2
r = Record ors -> Rec (Maybe :. ElField) ors
forall (fs :: [(Symbol, *)]).
RMap fs =>
Record fs -> Rec (Maybe :. ElField) fs
justsFromRec (Record ors -> Rec (Maybe :. ElField) ors)
-> Record ors -> Rec (Maybe :. ElField) ors
forall a b. (a -> b) -> a -> b
$ Record rs -> Record rs2 -> Record (rs ++ rs2')
forall (fs :: [(Symbol, *)]) (rs :: [(Symbol, *)])
(rs2 :: [(Symbol, *)]) (rs2' :: [(Symbol, *)]).
(fs ⊆ rs2, rs2' ⊆ rs2, rs2' ~ RDeleteAll fs rs2,
rs ⊆ (rs ++ rs2')) =>
Record rs -> Record rs2 -> Record (rs ++ rs2')
mergeRec @fs Record rs
l Record rs2
r
{-# INLINE mergeLeftEmpty #-}
mergeLeftEmpty :: Record rs -> Rec (Maybe :. ElField) (rs ++ rs2')
mergeLeftEmpty Record rs
l = Record rs -> Rec (Maybe :. ElField) rs
forall (fs :: [(Symbol, *)]).
RMap fs =>
Record fs -> Rec (Maybe :. ElField) fs
justsFromRec Record rs
l Rec (Maybe :. ElField) rs
-> Rec (Maybe :. ElField) rs2'
-> Rec (Maybe :. ElField) (rs ++ rs2')
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> RecApplicative rs2' => Rec (Maybe :. ElField) rs2'
forall (fs :: [(Symbol, *)]).
RecApplicative fs =>
Rec (Maybe :. ElField) fs
mkNothingsRec @rs2'
{-# INLINE mergeRightEmpty #-}
mergeRightEmpty :: Record rs2 -> Rec (Maybe :. ElField) ors
mergeRightEmpty Record rs2
r = Rec (Maybe :. ElField) (rs' ++ rs2) -> Rec (Maybe :. ElField) ors
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 @ors (RecApplicative rs' => Rec (Maybe :. ElField) rs'
forall (fs :: [(Symbol, *)]).
RecApplicative fs =>
Rec (Maybe :. ElField) fs
mkNothingsRec @rs' Rec (Maybe :. ElField) rs'
-> Rec (Maybe :. ElField) rs2
-> Rec (Maybe :. ElField) (rs' ++ rs2)
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Record rs2 -> Rec (Maybe :. ElField) rs2
forall (fs :: [(Symbol, *)]).
RMap fs =>
Record fs -> Rec (Maybe :. ElField) fs
justsFromRec Record rs2
r)
rightJoin :: forall fs rs rs' rs2 rs2' ors.
(fs ⊆ rs
, fs ⊆ rs2
, rs ⊆ (rs ++ rs2')
, rs' ⊆ rs
, rs' ~ RDeleteAll fs rs
, rs2' ⊆ rs2
, rs2' ~ RDeleteAll fs rs2
, ors ~ (rs ++ rs2')
, ors :~: (rs' ++ rs2)
, RecApplicative rs2'
, RecApplicative rs
, RecApplicative rs'
, Grouping (Record fs)
, RMap rs2
, RMap ors
, RecVec rs
, RecVec rs2'
, RecVec ors
) =>
Frame (Record rs)
-> Frame (Record rs2)
-> [Rec (Maybe :. ElField) ors]
rightJoin :: Frame (Record rs)
-> Frame (Record rs2) -> [Rec (Maybe :. ElField) ors]
rightJoin Frame (Record rs)
a Frame (Record rs2)
b =
[[Rec (Maybe :. ElField) ors]] -> [Rec (Maybe :. ElField) ors]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Rec (Maybe :. ElField) ors]] -> [Rec (Maybe :. ElField) ors])
-> [[Rec (Maybe :. ElField) ors]] -> [Rec (Maybe :. ElField) ors]
forall a b. (a -> b) -> a -> b
$
Group (Rec ElField fs)
-> (Record rs -> Record rs2 -> Rec (Maybe :. ElField) ors)
-> (Record rs2 -> Rec (Maybe :. ElField) ors)
-> (Record rs -> Rec ElField fs)
-> (Record rs2 -> Rec ElField fs)
-> [Record rs]
-> [Record rs2]
-> [[Rec (Maybe :. ElField) ors]]
forall (f :: * -> *) d a b c.
Discriminating f =>
f d
-> (a -> b -> c)
-> (b -> c)
-> (a -> d)
-> (b -> d)
-> [a]
-> [b]
-> [[c]]
rightOuter Group (Rec ElField fs)
forall a. Grouping a => Group a
grouping Record rs -> Record rs2 -> Rec (Maybe :. ElField) ors
mergeFun Record rs2 -> Rec (Maybe :. ElField) ors
mergeRightEmpty
Record rs -> Rec ElField fs
proj1 Record rs2 -> Rec ElField fs
proj2 (Frame (Record rs) -> [Record rs]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Frame (Record rs)
a) (Frame (Record rs2) -> [Record rs2]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Frame (Record rs2)
b)
where
{-# INLINE proj1 #-}
proj1 :: Record rs -> Rec ElField fs
proj1 = forall (ss :: [(Symbol, *)]) (f :: (Symbol, *) -> *)
(record :: ((Symbol, *) -> *) -> [(Symbol, *)] -> *) (is :: [Nat]).
(RecSubset record fs ss is, RecSubsetFCtx record f) =>
record f ss -> record f fs
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 @fs
{-# INLINE proj2 #-}
proj2 :: Record rs2 -> Rec ElField fs
proj2 = forall (ss :: [(Symbol, *)]) (f :: (Symbol, *) -> *)
(record :: ((Symbol, *) -> *) -> [(Symbol, *)] -> *) (is :: [Nat]).
(RecSubset record fs ss is, RecSubsetFCtx record f) =>
record f ss -> record f fs
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 @fs
{-# INLINE mergeFun #-}
mergeFun :: Record rs -> Record rs2 -> Rec (Maybe :. ElField) ors
mergeFun Record rs
l Record rs2
r = Record ors -> Rec (Maybe :. ElField) ors
forall (fs :: [(Symbol, *)]).
RMap fs =>
Record fs -> Rec (Maybe :. ElField) fs
justsFromRec (Record ors -> Rec (Maybe :. ElField) ors)
-> Record ors -> Rec (Maybe :. ElField) ors
forall a b. (a -> b) -> a -> b
$ Record rs -> Record rs2 -> Record (rs ++ rs2')
forall (fs :: [(Symbol, *)]) (rs :: [(Symbol, *)])
(rs2 :: [(Symbol, *)]) (rs2' :: [(Symbol, *)]).
(fs ⊆ rs2, rs2' ⊆ rs2, rs2' ~ RDeleteAll fs rs2,
rs ⊆ (rs ++ rs2')) =>
Record rs -> Record rs2 -> Record (rs ++ rs2')
mergeRec @fs Record rs
l Record rs2
r
{-# INLINE mergeRightEmpty #-}
mergeRightEmpty :: Record rs2 -> Rec (Maybe :. ElField) ors
mergeRightEmpty Record rs2
r = Rec (Maybe :. ElField) (rs' ++ rs2) -> Rec (Maybe :. ElField) ors
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 @ors (RecApplicative rs' => Rec (Maybe :. ElField) rs'
forall (fs :: [(Symbol, *)]).
RecApplicative fs =>
Rec (Maybe :. ElField) fs
mkNothingsRec @rs' Rec (Maybe :. ElField) rs'
-> Rec (Maybe :. ElField) rs2
-> Rec (Maybe :. ElField) (rs' ++ rs2)
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Record rs2 -> Rec (Maybe :. ElField) rs2
forall (fs :: [(Symbol, *)]).
RMap fs =>
Record fs -> Rec (Maybe :. ElField) fs
justsFromRec Record rs2
r)
leftJoin :: forall fs rs rs2 rs2'.
(fs ⊆ rs
, fs ⊆ rs2
, rs ⊆ (rs ++ rs2')
, rs2' ⊆ rs2
, rs2' ~ RDeleteAll fs rs2
, RMap rs
, RMap (rs ++ rs2')
, RecApplicative rs2'
, Grouping (Record fs)
, RecVec rs
, RecVec rs2'
, RecVec (rs ++ rs2')
) =>
Frame (Record rs)
-> Frame (Record rs2)
-> [Rec (Maybe :. ElField) (rs ++ rs2')]
leftJoin :: Frame (Record rs)
-> Frame (Record rs2) -> [Rec (Maybe :. ElField) (rs ++ rs2')]
leftJoin Frame (Record rs)
a Frame (Record rs2)
b =
[[Rec (Maybe :. ElField) (rs ++ rs2')]]
-> [Rec (Maybe :. ElField) (rs ++ rs2')]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
(Group (Rec ElField fs)
-> (Record rs -> Record rs2 -> Rec (Maybe :. ElField) (rs ++ rs2'))
-> (Record rs -> Rec (Maybe :. ElField) (rs ++ rs2'))
-> (Record rs -> Rec ElField fs)
-> (Record rs2 -> Rec ElField fs)
-> [Record rs]
-> [Record rs2]
-> [[Rec (Maybe :. ElField) (rs ++ rs2')]]
forall (f :: * -> *) d a b c.
Discriminating f =>
f d
-> (a -> b -> c)
-> (a -> c)
-> (a -> d)
-> (b -> d)
-> [a]
-> [b]
-> [[c]]
leftOuter Group (Rec ElField fs)
forall a. Grouping a => Group a
grouping Record rs -> Record rs2 -> Rec (Maybe :. ElField) (rs ++ rs2')
mergeFun Record rs -> Rec (Maybe :. ElField) (rs ++ rs2')
mergeLeftEmpty
Record rs -> Rec ElField fs
proj1 Record rs2 -> Rec ElField fs
proj2 (Frame (Record rs) -> [Record rs]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Frame (Record rs)
a) (Frame (Record rs2) -> [Record rs2]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Frame (Record rs2)
b))
where
proj1 :: Record rs -> Rec ElField fs
proj1 = forall (ss :: [(Symbol, *)]) (f :: (Symbol, *) -> *)
(record :: ((Symbol, *) -> *) -> [(Symbol, *)] -> *) (is :: [Nat]).
(RecSubset record fs ss is, RecSubsetFCtx record f) =>
record f ss -> record f fs
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 @fs
proj2 :: Record rs2 -> Rec ElField fs
proj2 = forall (ss :: [(Symbol, *)]) (f :: (Symbol, *) -> *)
(record :: ((Symbol, *) -> *) -> [(Symbol, *)] -> *) (is :: [Nat]).
(RecSubset record fs ss is, RecSubsetFCtx record f) =>
record f ss -> record f fs
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 @fs
mergeFun :: Record rs -> Record rs2 -> Rec (Maybe :. ElField) (rs ++ rs2')
mergeFun Record rs
l Record rs2
r = Record (rs ++ rs2') -> Rec (Maybe :. ElField) (rs ++ rs2')
forall (fs :: [(Symbol, *)]).
RMap fs =>
Record fs -> Rec (Maybe :. ElField) fs
justsFromRec (Record (rs ++ rs2') -> Rec (Maybe :. ElField) (rs ++ rs2'))
-> Record (rs ++ rs2') -> Rec (Maybe :. ElField) (rs ++ rs2')
forall a b. (a -> b) -> a -> b
$ Record rs -> Record rs2 -> Record (rs ++ rs2')
forall (fs :: [(Symbol, *)]) (rs :: [(Symbol, *)])
(rs2 :: [(Symbol, *)]) (rs2' :: [(Symbol, *)]).
(fs ⊆ rs2, rs2' ⊆ rs2, rs2' ~ RDeleteAll fs rs2,
rs ⊆ (rs ++ rs2')) =>
Record rs -> Record rs2 -> Record (rs ++ rs2')
mergeRec @fs Record rs
l Record rs2
r
mergeLeftEmpty :: Record rs -> Rec (Maybe :. ElField) (rs ++ rs2')
mergeLeftEmpty Record rs
l = Record rs -> Rec (Maybe :. ElField) rs
forall (fs :: [(Symbol, *)]).
RMap fs =>
Record fs -> Rec (Maybe :. ElField) fs
justsFromRec Record rs
l Rec (Maybe :. ElField) rs
-> Rec (Maybe :. ElField) rs2'
-> Rec (Maybe :. ElField) (rs ++ rs2')
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> RecApplicative rs2' => Rec (Maybe :. ElField) rs2'
forall (fs :: [(Symbol, *)]).
RecApplicative fs =>
Rec (Maybe :. ElField) fs
mkNothingsRec @rs2'