{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE UndecidableInstances #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Row.Records
--
-- This module implements extensible records using closed type famillies.
--
-- See Examples.lhs for examples.
--
-- Lists of (label,type) pairs are kept sorted thereby ensuring
-- that { x = 0, y = 0 } and { y = 0, x = 0 } have the same type.
--
-- In this way we can implement standard type classes such as Show, Eq, Ord and Bounded
-- for open records, given that all the elements of the open record satify the constraint.
--
-----------------------------------------------------------------------------


module Data.Row.Records
  (
  -- * Types and constraints
    Label(..)
  , KnownSymbol, AllUniqueLabels, WellBehaved
  , Rec, Row, Empty, type (≈)
  -- * Construction
  , empty
  , type (.==), (.==), pattern (:==), unSingleton
  , default', defaultA
  , fromLabels, fromLabelsA, fromLabelsMapA
  -- ** Extension
  , extend, Extend, Lacks, type (.\)
  -- ** Restriction
  , type (.-), (.-)
  , lazyRemove
  , Subset
  , restrict, split
  -- ** Modification
  , update, focus, multifocus, Modify, rename, Rename
  -- * Query
  , HasType, type (.!), (.!)
  -- * Combine
  -- ** Disjoint union
  , type (.+), (.+), Disjoint, pattern (:+)
  -- ** Overwrite
  , type (.//), (.//)
  -- * Application with functions
  , curryRec
  , (.$)
  -- * Native Conversion
  -- $native
  , fromNative, toNative, toNativeGeneral
  , FromNative, ToNative, ToNativeGeneral
  , NativeRow
  -- * Dynamic Conversion
  , toDynamicMap, fromDynamicMap
  -- * Row operations
  -- ** Map
  , Map, map, map', mapF
  , transform, transform'
  , zipTransform, zipTransform'
  -- ** Fold
  , BiForall, Forall, erase, eraseWithLabels, eraseZip, eraseToHashMap
  -- ** Zip
  , Zip, zip
  -- ** Applicative-like functions
  , traverse, traverseMap
  , sequence, sequence'
  , distribute
  -- ** Compose
  -- $compose
  , compose, uncompose
  , compose', uncompose'
  -- ** Labels
  , labels, labels'
  -- ** Coerce
  , coerceRec
  )
where

import Prelude hiding (map, sequence, traverse, zip)

import Control.DeepSeq (NFData(..), deepseq)

import           Data.Bifunctor               (Bifunctor(..))
import           Data.Coerce
import           Data.Dynamic
import           Data.Functor.Compose
import           Data.Functor.Const
import           Data.Functor.Identity
import           Data.Functor.Product
import           Data.Generics.Product.Fields (HasField(..), HasField'(..))
import           Data.Hashable
import           Data.HashMap.Lazy            (HashMap)
import qualified Data.HashMap.Lazy            as M
import qualified Data.List                    as L
import           Data.Monoid                  (Endo(..), appEndo)
import           Data.Proxy
import           Data.String                  (IsString)
import           Data.Text                    (Text)

import qualified GHC.Generics as G
import           GHC.TypeLits
import Unsafe.Coerce

import Data.Row.Dictionaries
import Data.Row.Internal


{--------------------------------------------------------------------
  Open records
--------------------------------------------------------------------}
-- | A record with row r.
newtype Rec (r :: Row *) where
  OR :: HashMap Text HideType -> Rec r

instance Forall r Show => Show (Rec r) where
  showsPrec :: Int -> Rec r -> ShowS
showsPrec Int
p Rec r
r =
    case (forall a. Show a => a -> ShowS) -> Rec r -> [(String, ShowS)]
forall (c :: * -> Constraint) (ρ :: Row *) s b.
(Forall ρ c, IsString s) =>
(forall a. c a => a -> b) -> Rec ρ -> [(s, b)]
eraseWithLabels @Show (Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
7) Rec r
r of
      [] ->
        String -> ShowS
showString String
"empty"
      [(String, ShowS)]
xs ->
        Bool -> ShowS -> ShowS
showParen
          (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
6)
          (Endo String -> ShowS
forall a. Endo a -> a -> a
appEndo (Endo String -> ShowS) -> Endo String -> ShowS
forall a b. (a -> b) -> a -> b
$ (ShowS -> Endo String) -> [ShowS] -> Endo String
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ShowS -> Endo String
forall a. (a -> a) -> Endo a
Endo (ShowS -> [ShowS] -> [ShowS]
forall a. a -> [a] -> [a]
L.intersperse (String -> ShowS
showString String
" .+ ") (((String, ShowS) -> ShowS) -> [(String, ShowS)] -> [ShowS]
forall a b. (a -> b) -> [a] -> [b]
L.map (String, ShowS) -> ShowS
forall a. (String, a -> String) -> a -> String
binds [(String, ShowS)]
xs)))
    where
      binds :: (String, a -> String) -> a -> String
binds (String
label, a -> String
value) =
        Char -> ShowS
showChar Char
'#' ShowS -> (a -> String) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        String -> ShowS
showString String
label ShowS -> (a -> String) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        String -> ShowS
showString String
" .== " ShowS -> (a -> String) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        a -> String
value

instance Forall r Eq => Eq (Rec r) where
  Rec r
r == :: Rec r -> Rec r -> Bool
== Rec r
r' = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (forall a. Eq a => a -> a -> Bool) -> Rec r -> Rec r -> [Bool]
forall (c :: * -> Constraint) (ρ :: Row *) b.
Forall ρ c =>
(forall a. c a => a -> a -> b) -> Rec ρ -> Rec ρ -> [b]
eraseZip @Eq forall a. Eq a => a -> a -> Bool
(==) Rec r
r Rec r
r'

instance (Forall r Eq, Forall r Ord) => Ord (Rec r) where
  compare :: Rec r -> Rec r -> Ordering
compare Rec r
m Rec r
m' = [Ordering] -> Ordering
cmp ([Ordering] -> Ordering) -> [Ordering] -> Ordering
forall a b. (a -> b) -> a -> b
$ (forall a. Ord a => a -> a -> Ordering)
-> Rec r -> Rec r -> [Ordering]
forall (c :: * -> Constraint) (ρ :: Row *) b.
Forall ρ c =>
(forall a. c a => a -> a -> b) -> Rec ρ -> Rec ρ -> [b]
eraseZip @Ord forall a. Ord a => a -> a -> Ordering
compare Rec r
m Rec r
m'
      where cmp :: [Ordering] -> Ordering
cmp [Ordering]
l | [] <- [Ordering]
l' = Ordering
EQ
                  | Ordering
a : [Ordering]
_ <- [Ordering]
l' = Ordering
a
                  where l' :: [Ordering]
l' = (Ordering -> Bool) -> [Ordering] -> [Ordering]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ) [Ordering]
l

instance (Forall r Bounded, AllUniqueLabels r) => Bounded (Rec r) where
  minBound :: Rec r
minBound = (forall a. Bounded a => a) -> Rec r
forall (c :: * -> Constraint) (ρ :: Row *).
(Forall ρ c, AllUniqueLabels ρ) =>
(forall a. c a => a) -> Rec ρ
default' @Bounded forall a. Bounded a => a
minBound
  maxBound :: Rec r
maxBound = (forall a. Bounded a => a) -> Rec r
forall (c :: * -> Constraint) (ρ :: Row *).
(Forall ρ c, AllUniqueLabels ρ) =>
(forall a. c a => a) -> Rec ρ
default' @Bounded forall a. Bounded a => a
maxBound

instance Forall r NFData => NFData (Rec r) where
  rnf :: Rec r -> ()
rnf Rec r
r = Const () r -> ()
forall a k (b :: k). Const a b -> a
getConst (Const () r -> ()) -> Const () r -> ()
forall a b. (a -> b) -> a -> b
$ Proxy (Proxy Identity, Proxy (,))
-> (Rec Empty -> Const () Empty)
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, NFData τ, HasType ℓ τ ρ) =>
    Label ℓ -> Rec ρ -> (Rec (ρ .- ℓ), Identity τ))
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, NFData τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> (Const () ρ, Identity τ) -> Const () (Extend ℓ τ ρ))
-> Rec r
-> Const () r
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @r @NFData @(,) @Rec @(Const ()) @Identity Proxy (Proxy Identity, Proxy (,))
forall k (t :: k). Proxy t
Proxy Rec Empty -> Const () Empty
forall k b (b :: k). b -> Const () b
empty forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, NFData τ, HasType ℓ τ ρ) =>
Label ℓ -> Rec ρ -> (Rec (ρ .- ℓ), Identity τ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Rec r -> (Rec (r .- l), Identity (r .! l))
doUncons forall k a a p (b :: k).
(NFData a, NFData a) =>
p -> (a, a) -> Const () b
forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, NFData τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ -> (Const () ρ, Identity τ) -> Const () (Extend ℓ τ ρ)
doCons Rec r
r
    where empty :: b -> Const () b
empty = Const () b -> b -> Const () b
forall a b. a -> b -> a
const (Const () b -> b -> Const () b) -> Const () b -> b -> Const () b
forall a b. (a -> b) -> a -> b
$ () -> Const () b
forall k a (b :: k). a -> Const a b
Const ()
          doUncons :: Label l -> Rec r -> (Rec (r .- l), Identity (r .! l))
doUncons Label l
l = ((r .! l) -> Identity (r .! l))
-> (Rec (r .- l), r .! l) -> (Rec (r .- l), Identity (r .! l))
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (r .! l) -> Identity (r .! l)
forall a. a -> Identity a
Identity ((Rec (r .- l), r .! l) -> (Rec (r .- l), Identity (r .! l)))
-> (Rec r -> (Rec (r .- l), r .! l))
-> Rec r
-> (Rec (r .- l), Identity (r .! l))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label l -> Rec r -> (Rec (r .- l), r .! l)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Rec r -> (Rec (r .- l), r .! l)
lazyUncons Label l
l
          doCons :: p -> (a, a) -> Const () b
doCons p
_ (a
r, a
x) = a -> Const () b -> Const () b
forall a b. NFData a => a -> b -> b
deepseq a
x (Const () b -> Const () b) -> Const () b -> Const () b
forall a b. (a -> b) -> a -> b
$ a -> Const () b -> Const () b
forall a b. NFData a => a -> b -> b
deepseq a
r (Const () b -> Const () b) -> Const () b -> Const () b
forall a b. (a -> b) -> a -> b
$ () -> Const () b
forall k a (b :: k). a -> Const a b
Const ()

-- | The empty record
empty :: Rec Empty
empty :: Rec Empty
empty = HashMap Text HideType -> Rec Empty
forall (r :: Row *). HashMap Text HideType -> Rec r
OR HashMap Text HideType
forall k v. HashMap k v
M.empty

-- | The singleton record
infix 7 .==
(.==) :: KnownSymbol l => Label l -> a -> Rec (l .== a)
Label l
l .== :: Label l -> a -> Rec (l .== a)
.== a
a = Label l -> a -> Rec Empty -> Rec (l .== a)
forall a (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> a -> Rec r -> Rec (Extend l a r)
extend Label l
l a
a Rec Empty
empty

-- | A pattern for the singleton record; can be used to both destruct a record
-- when in a pattern position or construct one in an expression position.
{-# COMPLETE (:==) #-}
infix 7 :==
pattern (:==) :: forall l a. KnownSymbol l => Label l -> a -> Rec (l .== a)
pattern l $b:== :: Label l -> a -> Rec (l .== a)
$m:== :: forall r (l :: Symbol) a.
KnownSymbol l =>
Rec (l .== a) -> (Label l -> a -> r) -> (Void# -> r) -> r
:== a <- (unSingleton @l @a -> (l, a)) where
        (:==) Label l
l a
a = Label l
l Label l -> a -> Rec (l .== a)
forall (l :: Symbol) a.
KnownSymbol l =>
Label l -> a -> Rec (l .== a)
.== a
a

-- | Turns a singleton record into a pair of the label and value.
unSingleton :: forall l a. KnownSymbol l => Rec (l .== a) -> (Label l, a)
unSingleton :: Rec (l .== a) -> (Label l, a)
unSingleton Rec (l .== a)
r = (Label l
l, Rec (l .== a)
Rec ('R '[ l ':-> a])
r Rec ('R '[ l ':-> a]) -> Label l -> 'R '[ l ':-> a] .! l
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Rec r -> Label l -> r .! l
.! Label l
l) where l :: Label l
l = Label l
forall (s :: Symbol). Label s
Label @l

{--------------------------------------------------------------------
  Basic record operations
--------------------------------------------------------------------}


-- | Record extension. The row may already contain the label,
--   in which case the origin value can be obtained after restriction ('.-') with
--   the label.
extend :: forall a l r. KnownSymbol l => Label l -> a -> Rec r -> Rec (Extend l a r)
extend :: Label l -> a -> Rec r -> Rec (Extend l a r)
extend (Label l -> Text
forall (s :: Symbol). KnownSymbol s => Label s -> Text
toKey -> Text
l) a
a (OR HashMap Text HideType
m) = HashMap Text HideType -> Rec (Extend l a r)
forall (r :: Row *). HashMap Text HideType -> Rec r
OR (HashMap Text HideType -> Rec (Extend l a r))
-> HashMap Text HideType -> Rec (Extend l a r)
forall a b. (a -> b) -> a -> b
$ Text -> HideType -> HashMap Text HideType -> HashMap Text HideType
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Text
l (a -> HideType
forall a. a -> HideType
HideType a
a) HashMap Text HideType
m

-- | Update the value associated with the label.
update :: (KnownSymbol l, r .! l ≈ a) => Label l -> a -> Rec r -> Rec r
update :: Label l -> a -> Rec r -> Rec r
update (Label l -> Text
forall (s :: Symbol). KnownSymbol s => Label s -> Text
toKey -> Text
l) a
a (OR HashMap Text HideType
m) = HashMap Text HideType -> Rec r
forall (r :: Row *). HashMap Text HideType -> Rec r
OR (HashMap Text HideType -> Rec r) -> HashMap Text HideType -> Rec r
forall a b. (a -> b) -> a -> b
$ (HideType -> HideType)
-> Text -> HashMap Text HideType -> HashMap Text HideType
forall k v.
(Eq k, Hashable k) =>
(v -> v) -> k -> HashMap k v -> HashMap k v
M.adjust HideType -> HideType
f Text
l HashMap Text HideType
m where f :: HideType -> HideType
f = HideType -> HideType -> HideType
forall a b. a -> b -> a
const (a -> HideType
forall a. a -> HideType
HideType a
a)

-- | Focus on the value associated with the label.
focus ::
  ( KnownSymbol l
  , r' .! l ≈ b
  , r  .! l ≈ a
  , r' ~ Modify l b r
  , r  ~ Modify l a r'
  , Functor f)
  => Label l -> (a -> f b) -> Rec r -> f (Rec r')
focus :: Label l -> (a -> f b) -> Rec r -> f (Rec r')
focus (Label l -> Text
forall (s :: Symbol). KnownSymbol s => Label s -> Text
toKey -> Text
l) a -> f b
f (OR HashMap Text HideType
m) = case HashMap Text HideType
m HashMap Text HideType -> Text -> HideType
forall k v.
(Eq k, Hashable k, HasCallStack) =>
HashMap k v -> k -> v
M.! Text
l of
  HideType a
x -> HashMap Text HideType -> Rec r'
forall (r :: Row *). HashMap Text HideType -> Rec r
OR (HashMap Text HideType -> Rec r')
-> (b -> HashMap Text HideType) -> b -> Rec r'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HideType -> HashMap Text HideType -> HashMap Text HideType)
-> HashMap Text HideType -> HideType -> HashMap Text HideType
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Text -> HideType -> HashMap Text HideType -> HashMap Text HideType
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Text
l) HashMap Text HideType
m (HideType -> HashMap Text HideType)
-> (b -> HideType) -> b -> HashMap Text HideType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> HideType
forall a. a -> HideType
HideType (b -> Rec r') -> f b -> f (Rec r')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f (a -> a
forall a b. a -> b
unsafeCoerce a
x)

-- | Focus on a sub-record
multifocus :: forall u v r f.
  ( Functor f
  , Disjoint u r
  , Disjoint v r)
  => (Rec u -> f (Rec v)) -> Rec (u .+ r) -> f (Rec (v .+ r))
multifocus :: (Rec u -> f (Rec v)) -> Rec (u .+ r) -> f (Rec (v .+ r))
multifocus Rec u -> f (Rec v)
f (u :+ r) = (Rec v -> Rec r -> Rec (v .+ r)
forall (l :: Row *) (r :: Row *).
FreeForall l =>
Rec l -> Rec r -> Rec (l .+ r)
.+ Rec r
r) (Rec v -> Rec (v .+ r)) -> f (Rec v) -> f (Rec (v .+ r))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Rec u -> f (Rec v)
f Rec u
u

-- | Rename a label.
rename :: (KnownSymbol l, KnownSymbol l') => Label l -> Label l' -> Rec r -> Rec (Rename l l' r)
rename :: Label l -> Label l' -> Rec r -> Rec (Rename l l' r)
rename (Label l -> Text
forall (s :: Symbol). KnownSymbol s => Label s -> Text
toKey -> Text
l) (Label l' -> Text
forall (s :: Symbol). KnownSymbol s => Label s -> Text
toKey -> Text
l') (OR HashMap Text HideType
m) = HashMap Text HideType -> Rec (Extend l' (r .! l) (r .- l))
forall (r :: Row *). HashMap Text HideType -> Rec r
OR (HashMap Text HideType -> Rec (Extend l' (r .! l) (r .- l)))
-> HashMap Text HideType -> Rec (Extend l' (r .! l) (r .- l))
forall a b. (a -> b) -> a -> b
$ Text -> HideType -> HashMap Text HideType -> HashMap Text HideType
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Text
l' (HashMap Text HideType
m HashMap Text HideType -> Text -> HideType
forall k v.
(Eq k, Hashable k, HasCallStack) =>
HashMap k v -> k -> v
M.! Text
l) (HashMap Text HideType -> HashMap Text HideType)
-> HashMap Text HideType -> HashMap Text HideType
forall a b. (a -> b) -> a -> b
$ Text -> HashMap Text HideType -> HashMap Text HideType
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
M.delete Text
l HashMap Text HideType
m

-- | Record selection
(.!) :: KnownSymbol l => Rec r -> Label l -> r .! l
OR HashMap Text HideType
m .! :: Rec r -> Label l -> r .! l
.! (Label l -> Text
forall (s :: Symbol). KnownSymbol s => Label s -> Text
toKey -> Text
a) = case HashMap Text HideType
m HashMap Text HideType -> Text -> HideType
forall k v.
(Eq k, Hashable k, HasCallStack) =>
HashMap k v -> k -> v
M.! Text
a of
  HideType a
x -> a -> r .! l
forall a b. a -> b
unsafeCoerce a
x

infixl 6 .-
-- | Record restriction. Remove the label l from the record.
(.-) :: KnownSymbol l => Rec r -> Label l -> Rec (r .- l)
-- OR m .- _ = OR m
OR HashMap Text HideType
m .- :: Rec r -> Label l -> Rec (r .- l)
.- (Label l -> Text
forall (s :: Symbol). KnownSymbol s => Label s -> Text
toKey -> Text
a) = HashMap Text HideType -> Rec (r .- l)
forall (r :: Row *). HashMap Text HideType -> Rec r
OR (HashMap Text HideType -> Rec (r .- l))
-> HashMap Text HideType -> Rec (r .- l)
forall a b. (a -> b) -> a -> b
$ Text -> HashMap Text HideType -> HashMap Text HideType
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
M.delete Text
a HashMap Text HideType
m

-- | Record disjoint union (commutative)
infixl 6 .+
(.+) :: forall l r. FreeForall l => Rec l -> Rec r -> Rec (l .+ r)
OR HashMap Text HideType
l .+ :: Rec l -> Rec r -> Rec (l .+ r)
.+ OR HashMap Text HideType
r = HashMap Text HideType -> Rec (l .+ r)
forall (r :: Row *). HashMap Text HideType -> Rec r
OR (HashMap Text HideType -> Rec (l .+ r))
-> HashMap Text HideType -> Rec (l .+ r)
forall a b. (a -> b) -> a -> b
$ (Text -> HideType -> HideType -> HideType)
-> HashMap Text HideType
-> HashMap Text HideType
-> HashMap Text HideType
forall k v.
(Eq k, Hashable k) =>
(k -> v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
M.unionWithKey Text -> HideType -> HideType -> HideType
choose HashMap Text HideType
l HashMap Text HideType
r
  where
    choose :: Text -> HideType -> HideType -> HideType
choose Text
k HideType
lv HideType
rv = if Text
k Text -> [Text] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (IsString Text, Forall l Unconstrained1) => [Text]
forall k (ρ :: Row k) s.
(IsString s, Forall ρ Unconstrained1) =>
[s]
labels' @l @Text then HideType
lv else HideType
rv

-- | Record overwrite.
--
-- The operation @r .// r'@ creates a new record such that:
--
-- - Any label that is in both @r@ and @r'@ is in the resulting record with the
--   type and value given by the fields in @r@,
--
-- - Any label that is only found in @r@ is in the resulting record.
--
-- - Any label that is only found in @r'@ is in the resulting record.
--
-- This can be thought of as @r@ "overwriting" @r'@.
infixl 6 .//
(.//) :: Rec r -> Rec r' -> Rec (r .// r')
OR HashMap Text HideType
l .// :: Rec r -> Rec r' -> Rec (r .// r')
.// OR HashMap Text HideType
r = HashMap Text HideType -> Rec (r .// r')
forall (r :: Row *). HashMap Text HideType -> Rec r
OR (HashMap Text HideType -> Rec (r .// r'))
-> HashMap Text HideType -> Rec (r .// r')
forall a b. (a -> b) -> a -> b
$ HashMap Text HideType
-> HashMap Text HideType -> HashMap Text HideType
forall k v.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k v -> HashMap k v
M.union HashMap Text HideType
l HashMap Text HideType
r

-- | A pattern version of record union, for use in pattern matching.
{-# COMPLETE (:+) #-}
infixl 6 :+
pattern (:+) :: forall l r. Disjoint l r => Rec l -> Rec r -> Rec (l .+ r)
pattern l $b:+ :: Rec l -> Rec r -> Rec (l .+ r)
$m:+ :: forall r (l :: Row *) (r :: Row *).
Disjoint l r =>
Rec (l .+ r) -> (Rec l -> Rec r -> r) -> (Void# -> r) -> r
:+ r <- (split @l -> (l, r)) where
        (:+) Rec l
l Rec r
r = Rec l
l Rec l -> Rec r -> Rec (l .+ r)
forall (l :: Row *) (r :: Row *).
FreeForall l =>
Rec l -> Rec r -> Rec (l .+ r)
.+ Rec r
r

-- | Split a record into two sub-records.
split :: forall s r. (Subset s r, FreeForall s)
         => Rec r -> (Rec s, Rec (r .\\ s))
split :: Rec r -> (Rec s, Rec (r .\\ s))
split (OR HashMap Text HideType
m) = (HashMap Text HideType -> Rec s
forall (r :: Row *). HashMap Text HideType -> Rec r
OR (HashMap Text HideType -> Rec s) -> HashMap Text HideType -> Rec s
forall a b. (a -> b) -> a -> b
$ HashMap Text HideType -> HashMap Text () -> HashMap Text HideType
forall k v w.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k w -> HashMap k v
M.intersection HashMap Text HideType
m HashMap Text ()
labelMap, HashMap Text HideType -> Rec (r .\\ s)
forall (r :: Row *). HashMap Text HideType -> Rec r
OR (HashMap Text HideType -> Rec (r .\\ s))
-> HashMap Text HideType -> Rec (r .\\ s)
forall a b. (a -> b) -> a -> b
$ HashMap Text HideType -> HashMap Text () -> HashMap Text HideType
forall k v w.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k w -> HashMap k v
M.difference HashMap Text HideType
m HashMap Text ()
labelMap)
  where
    labelMap :: HashMap Text ()
labelMap = [(Text, ())] -> HashMap Text ()
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(Text, ())] -> HashMap Text ())
-> [(Text, ())] -> HashMap Text ()
forall a b. (a -> b) -> a -> b
$ [Text] -> [()] -> [(Text, ())]
forall a b. [a] -> [b] -> [(a, b)]
L.zip (forall s. (IsString s, Forall s Unconstrained1) => [s]
forall k (ρ :: Row k) s.
(IsString s, Forall ρ Unconstrained1) =>
[s]
labels' @s) (() -> [()]
forall a. a -> [a]
repeat ())

-- | Arbitrary record restriction.  Turn a record into a subset of itself.
restrict :: forall r r'. (FreeForall r, Subset r r') => Rec r' -> Rec r
restrict :: Rec r' -> Rec r
restrict = (Rec r, Rec (r' .\\ r)) -> Rec r
forall a b. (a, b) -> a
fst ((Rec r, Rec (r' .\\ r)) -> Rec r)
-> (Rec r' -> (Rec r, Rec (r' .\\ r))) -> Rec r' -> Rec r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec r' -> (Rec r, Rec (r' .\\ r))
forall (s :: Row *) (r :: Row *).
(Subset s r, FreeForall s) =>
Rec r -> (Rec s, Rec (r .\\ s))
split

-- | Removes a label from the record but does not remove the underlying value.
--
-- This is faster than regular record removal ('.-'), but it has two downsides:
--
-- 1. It may incur a performance penalty during a future merge operation ('.+'), and
--
-- 2. It will keep the reference to the value alive, meaning that it will not get garbage collected.
--
-- Thus, it's great when one knows ahead of time that no future merges will happen
-- and that the whole record will be GC'd soon, for instance, during the catamorphism
-- function of 'metamorph'.
lazyRemove :: KnownSymbol l => Label l -> Rec r -> Rec (r .- l)
lazyRemove :: Label l -> Rec r -> Rec (r .- l)
lazyRemove Label l
_ (OR HashMap Text HideType
m) = HashMap Text HideType -> Rec (r .- l)
forall (r :: Row *). HashMap Text HideType -> Rec r
OR HashMap Text HideType
m

-- | This is the same as @(lazyRemove l r, r .! l)@.
lazyUncons :: KnownSymbol l => Label l -> Rec r -> (Rec (r .- l), r .! l)
lazyUncons :: Label l -> Rec r -> (Rec (r .- l), r .! l)
lazyUncons Label l
l Rec r
r = (Label l -> Rec r -> Rec (r .- l)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Rec r -> Rec (r .- l)
lazyRemove Label l
l Rec r
r, Rec r
r Rec r -> Label l -> r .! l
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Rec r -> Label l -> r .! l
.! Label l
l)

-- | Kind of like 'curry' for functions over records.
curryRec :: forall l t r x. KnownSymbol l => Label l -> (Rec (l .== t .+ r) -> x) -> t -> Rec r -> x
curryRec :: Label l -> (Rec ((l .== t) .+ r) -> x) -> t -> Rec r -> x
curryRec Label l
l Rec ((l .== t) .+ r) -> x
f t
t Rec r
r = Rec ((l .== t) .+ r) -> x
f (Rec ((l .== t) .+ r) -> x) -> Rec ((l .== t) .+ r) -> x
forall a b. (a -> b) -> a -> b
$ (Label l
l Label l -> t -> Rec (l .== t)
forall (l :: Symbol) a.
KnownSymbol l =>
Label l -> a -> Rec (l .== a)
.== t
t) Rec ('R '[ l ':-> t]) -> Rec r -> Rec ('R '[ l ':-> t] .+ r)
forall (l :: Row *) (r :: Row *).
FreeForall l =>
Rec l -> Rec r -> Rec (l .+ r)
.+ Rec r
r

infixl 2 .$
-- | This function allows one to do partial application on a function of a record.
-- Note that this also means that arguments can be supplied in arbitrary order.
-- For instance, if one had a function like
--
-- > xtheny r = (r .! #x) <> (r .! #y)
--
-- and a record like
--
-- > greeting = #x .== "hello " .+ #y .== "world!"
--
-- Then all of the following would be possible:
--
-- >>> xtheny greeting
-- "hello world!"
--
-- >>> xtheny .$ (#x, greeting) .$ (#y, greeting) $ empty
-- "hello world!"
--
-- >>> xtheny .$ (#y, greeting) .$ (#x, greeting) $ empty
-- "hello world!"
--
-- >>> xtheny .$ (#y, greeting) .$ (#x, #x .== "Goodbye ") $ empty
-- "Goodbye world!"
(.$) :: (KnownSymbol l, r' .! l ≈ t) => (Rec (l .== t .+ r) -> x) -> (Label l, Rec r') -> Rec r -> x
.$ :: (Rec ((l .== t) .+ r) -> x) -> (Label l, Rec r') -> Rec r -> x
(.$) Rec ((l .== t) .+ r) -> x
f (Label l
l, Rec r'
r') Rec r
r = Label l -> (Rec ((l .== t) .+ r) -> x) -> t -> Rec r -> x
forall (l :: Symbol) t (r :: Row *) x.
KnownSymbol l =>
Label l -> (Rec ((l .== t) .+ r) -> x) -> t -> Rec r -> x
curryRec Label l
l Rec ((l .== t) .+ r) -> x
f (Rec r'
r' Rec r' -> Label l -> r' .! l
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Rec r -> Label l -> r .! l
.! Label l
l) Rec r
r

{--------------------------------------------------------------------
  Folds and maps
--------------------------------------------------------------------}
-- An easy type synonym for a pair where both elements are the same type.
newtype Pair' a = Pair' { Pair' a -> (a, a)
unPair' :: (a,a) }

-- | A standard fold
erase :: forall c ρ b. Forall ρ c => (forall a. c a => a -> b) -> Rec ρ -> [b]
erase :: (forall a. c a => a -> b) -> Rec ρ -> [b]
erase forall a. c a => a -> b
f = ((String, b) -> b) -> [(String, b)] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall b. (String, b) -> b
forall a b. (a, b) -> b
snd @String) ([(String, b)] -> [b]) -> (Rec ρ -> [(String, b)]) -> Rec ρ -> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. c a => a -> b) -> Rec ρ -> [(String, b)]
forall (c :: * -> Constraint) (ρ :: Row *) s b.
(Forall ρ c, IsString s) =>
(forall a. c a => a -> b) -> Rec ρ -> [(s, b)]
eraseWithLabels @c forall a. c a => a -> b
f

-- | A fold with labels
eraseWithLabels :: forall c ρ s b. (Forall ρ c, IsString s) => (forall a. c a => a -> b) -> Rec ρ -> [(s,b)]
eraseWithLabels :: (forall a. c a => a -> b) -> Rec ρ -> [(s, b)]
eraseWithLabels forall a. c a => a -> b
f = Const [(s, b)] ρ -> [(s, b)]
forall a k (b :: k). Const a b -> a
getConst (Const [(s, b)] ρ -> [(s, b)])
-> (Rec ρ -> Const [(s, b)] ρ) -> Rec ρ -> [(s, b)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (Proxy Identity, Proxy (,))
-> (Rec Empty -> Const [(s, b)] Empty)
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> Rec ρ -> (Rec (ρ .- ℓ), Identity τ))
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ
    -> (Const [(s, b)] ρ, Identity τ) -> Const [(s, b)] (Extend ℓ τ ρ))
-> Rec ρ
-> Const [(s, b)] ρ
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @ρ @c @(,) @Rec @(Const [(s,b)]) @Identity Proxy (Proxy Identity, Proxy (,))
forall k (t :: k). Proxy t
Proxy Rec Empty -> Const [(s, b)] Empty
forall k p a (b :: k). p -> Const [a] b
doNil forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
Label ℓ -> Rec ρ -> (Rec (ρ .- ℓ), Identity τ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Rec r -> (Rec (r .- l), Identity (r .! l))
doUncons forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ
-> (Const [(s, b)] ρ, Identity τ) -> Const [(s, b)] (Extend ℓ τ ρ)
forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ) =>
Label ℓ
-> (Const [(s, b)] ρ, Identity τ) -> Const [(s, b)] (Extend ℓ τ ρ)
doCons
  where doNil :: p -> Const [a] b
doNil p
_ = [a] -> Const [a] b
forall k a (b :: k). a -> Const a b
Const []
        doUncons :: Label l -> Rec r -> (Rec (r .- l), Identity (r .! l))
doUncons Label l
l = ((r .! l) -> Identity (r .! l))
-> (Rec (r .- l), r .! l) -> (Rec (r .- l), Identity (r .! l))
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (r .! l) -> Identity (r .! l)
forall a. a -> Identity a
Identity ((Rec (r .- l), r .! l) -> (Rec (r .- l), Identity (r .! l)))
-> (Rec r -> (Rec (r .- l), r .! l))
-> Rec r
-> (Rec (r .- l), Identity (r .! l))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label l -> Rec r -> (Rec (r .- l), r .! l)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Rec r -> (Rec (r .- l), r .! l)
lazyUncons Label l
l
        doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
               => Label ℓ -> (Const [(s,b)] ρ, Identity τ) -> Const [(s,b)] (Extend ℓ τ ρ)
        doCons :: Label ℓ
-> (Const [(s, b)] ρ, Identity τ) -> Const [(s, b)] (Extend ℓ τ ρ)
doCons Label ℓ
l (Const [(s, b)]
c, Identity τ
x) = [(s, b)] -> Const [(s, b)] (Extend ℓ τ ρ)
forall k a (b :: k). a -> Const a b
Const ([(s, b)] -> Const [(s, b)] (Extend ℓ τ ρ))
-> [(s, b)] -> Const [(s, b)] (Extend ℓ τ ρ)
forall a b. (a -> b) -> a -> b
$ (Label ℓ -> s
forall s a. (IsString s, Show a) => a -> s
show' Label ℓ
l, τ -> b
forall a. c a => a -> b
f τ
x) (s, b) -> [(s, b)] -> [(s, b)]
forall a. a -> [a] -> [a]
: [(s, b)]
c

-- | A fold over two row type structures at once
eraseZip :: forall c ρ b. Forall ρ c => (forall a. c a => a -> a -> b) -> Rec ρ -> Rec ρ -> [b]
eraseZip :: (forall a. c a => a -> a -> b) -> Rec ρ -> Rec ρ -> [b]
eraseZip forall a. c a => a -> a -> b
f Rec ρ
x Rec ρ
y = Const [b] ρ -> [b]
forall a k (b :: k). Const a b -> a
getConst (Const [b] ρ -> [b]) -> Const [b] ρ -> [b]
forall a b. (a -> b) -> a -> b
$ Proxy (Proxy Pair', Proxy (,))
-> (Product Rec Rec Empty -> Const [b] Empty)
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ
    -> Product Rec Rec ρ -> (Product Rec Rec (ρ .- ℓ), Pair' τ))
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> (Const [b] ρ, Pair' τ) -> Const [b] (Extend ℓ τ ρ))
-> Product Rec Rec ρ
-> Const [b] ρ
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @ρ @c @(,) @(Product Rec Rec) @(Const [b]) @Pair' Proxy (Proxy Pair', Proxy (,))
forall k (t :: k). Proxy t
Proxy (Const [b] Empty -> Product Rec Rec Empty -> Const [b] Empty
forall a b. a -> b -> a
const (Const [b] Empty -> Product Rec Rec Empty -> Const [b] Empty)
-> Const [b] Empty -> Product Rec Rec Empty -> Const [b] Empty
forall a b. (a -> b) -> a -> b
$ [b] -> Const [b] Empty
forall k a (b :: k). a -> Const a b
Const []) forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
Label ℓ -> Product Rec Rec ρ -> (Product Rec Rec (ρ .- ℓ), Pair' τ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l
-> Product Rec Rec r -> (Product Rec Rec (r .- l), Pair' (r .! l))
doUncons forall (ℓ :: Symbol) τ (ρ :: Row *).
c τ =>
Label ℓ -> (Const [b] ρ, Pair' τ) -> Const [b] (Extend ℓ τ ρ)
forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ -> (Const [b] ρ, Pair' τ) -> Const [b] (Extend ℓ τ ρ)
doCons (Rec ρ -> Rec ρ -> Product Rec Rec ρ
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair Rec ρ
x Rec ρ
y)
  where doUncons :: Label l
-> Product Rec Rec r -> (Product Rec Rec (r .- l), Pair' (r .! l))
doUncons Label l
l (Pair Rec r
r1 Rec r
r2) = (Rec (r .- l) -> Rec (r .- l) -> Product Rec Rec (r .- l)
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair Rec (r .- l)
r1' Rec (r .- l)
r2', (r .! l, r .! l) -> Pair' (r .! l)
forall a. (a, a) -> Pair' a
Pair' (r .! l
a, r .! l
b))
          where (Rec (r .- l)
r1', r .! l
a) = Label l -> Rec r -> (Rec (r .- l), r .! l)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Rec r -> (Rec (r .- l), r .! l)
lazyUncons Label l
l Rec r
r1
                (Rec (r .- l)
r2', r .! l
b) = Label l -> Rec r -> (Rec (r .- l), r .! l)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Rec r -> (Rec (r .- l), r .! l)
lazyUncons Label l
l Rec r
r2
        doCons :: forall ℓ τ ρ. c τ
               => Label ℓ -> (Const [b] ρ, Pair' τ) -> Const [b] (Extend ℓ τ ρ)
        doCons :: Label ℓ -> (Const [b] ρ, Pair' τ) -> Const [b] (Extend ℓ τ ρ)
doCons Label ℓ
_ (Const [b]
c, Pair' τ -> (τ, τ)
forall a. Pair' a -> (a, a)
unPair' -> (τ, τ)
x) = [b] -> Const [b] (Extend ℓ τ ρ)
forall k a (b :: k). a -> Const a b
Const ([b] -> Const [b] (Extend ℓ τ ρ))
-> [b] -> Const [b] (Extend ℓ τ ρ)
forall a b. (a -> b) -> a -> b
$ (τ -> τ -> b) -> (τ, τ) -> b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry τ -> τ -> b
forall a. c a => a -> a -> b
f (τ, τ)
x b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [b]
c

-- | Turns a record into a 'HashMap' from values representing the labels to
--   the values of the record.
eraseToHashMap :: forall c r s b. (IsString s, Eq s, Hashable s, Forall r c) =>
                  (forall a . c a => a -> b) -> Rec r -> HashMap s b
eraseToHashMap :: (forall a. c a => a -> b) -> Rec r -> HashMap s b
eraseToHashMap forall a. c a => a -> b
f Rec r
r = [(s, b)] -> HashMap s b
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(s, b)] -> HashMap s b) -> [(s, b)] -> HashMap s b
forall a b. (a -> b) -> a -> b
$ (forall a. c a => a -> b) -> Rec r -> [(s, b)]
forall (c :: * -> Constraint) (ρ :: Row *) s b.
(Forall ρ c, IsString s) =>
(forall a. c a => a -> b) -> Rec ρ -> [(s, b)]
eraseWithLabels @c forall a. c a => a -> b
f Rec r
r

-- | RMap is used internally as a type level lambda for defining record maps.
newtype RMap f ρ = RMap { RMap f ρ -> Rec (Map f ρ)
unRMap :: Rec (Map f ρ) }
newtype RMap2 f g ρ = RMap2 { RMap2 f g ρ -> Rec (Map f (Map g ρ))
unRMap2 :: Rec (Map f (Map g ρ)) }

-- | A function to map over a record given a constraint.
map :: forall c f r. Forall r c => (forall a. c a => a -> f a) -> Rec r -> Rec (Map f r)
map :: (forall a. c a => a -> f a) -> Rec r -> Rec (Map f r)
map forall a. c a => a -> f a
f = RMap f r -> Rec (Map f r)
forall a (f :: a -> *) (ρ :: Row a). RMap f ρ -> Rec (Map f ρ)
unRMap (RMap f r -> Rec (Map f r))
-> (Rec r -> RMap f r) -> Rec r -> Rec (Map f r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (Proxy f, Proxy (,))
-> (Rec Empty -> RMap f Empty)
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> Rec ρ -> (Rec (ρ .- ℓ), f τ))
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> (RMap f ρ, f τ) -> RMap f (Extend ℓ τ ρ))
-> Rec r
-> RMap f r
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @r @c @(,) @Rec @(RMap f) @f Proxy (Proxy f, Proxy (,))
forall k (t :: k). Proxy t
Proxy Rec Empty -> RMap f Empty
forall a (f :: a -> *) (ρ :: Row a) p.
(Map f ρ ~ Empty) =>
p -> RMap f ρ
doNil forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
Label ℓ -> Rec ρ -> (Rec (ρ .- ℓ), f τ)
doUncons forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ -> (RMap f ρ, f τ) -> RMap f (Extend ℓ τ ρ)
forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ) =>
Label ℓ -> (RMap f ρ, f τ) -> RMap f (Extend ℓ τ ρ)
doCons
  where
    doNil :: p -> RMap f ρ
doNil p
_ = Rec (Map f ρ) -> RMap f ρ
forall a (f :: a -> *) (ρ :: Row a). Rec (Map f ρ) -> RMap f ρ
RMap Rec (Map f ρ)
Rec Empty
empty
    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, HasType ℓ τ ρ)
             => Label ℓ -> Rec ρ -> (Rec (ρ .- ℓ), f τ)
    doUncons :: Label ℓ -> Rec ρ -> (Rec (ρ .- ℓ), f τ)
doUncons Label ℓ
l = (τ -> f τ) -> (Rec (ρ .- ℓ), τ) -> (Rec (ρ .- ℓ), f τ)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second τ -> f τ
forall a. c a => a -> f a
f ((Rec (ρ .- ℓ), τ) -> (Rec (ρ .- ℓ), f τ))
-> (Rec ρ -> (Rec (ρ .- ℓ), τ)) -> Rec ρ -> (Rec (ρ .- ℓ), f τ)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label ℓ -> Rec ρ -> (Rec (ρ .- ℓ), ρ .! ℓ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Rec r -> (Rec (r .- l), r .! l)
lazyUncons Label ℓ
l
    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
           => Label ℓ -> (RMap f ρ, f τ) -> RMap f (Extend ℓ τ ρ)
    doCons :: Label ℓ -> (RMap f ρ, f τ) -> RMap f (Extend ℓ τ ρ)
doCons Label ℓ
l (RMap Rec (Map f ρ)
r, f τ
v) = Rec (Map f (Extend ℓ τ ρ)) -> RMap f (Extend ℓ τ ρ)
forall a (f :: a -> *) (ρ :: Row a). Rec (Map f ρ) -> RMap f ρ
RMap (Label ℓ -> f τ -> Rec (Map f ρ) -> Rec (Extend ℓ (f τ) (Map f ρ))
forall a (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> a -> Rec r -> Rec (Extend l a r)
extend Label ℓ
l f τ
v Rec (Map f ρ)
r)
      ((Extend ℓ (f τ) (Map f ρ) ~ Map f (Extend ℓ τ ρ)) =>
 RMap f (Extend ℓ τ ρ))
-> Dict (Extend ℓ (f τ) (Map f ρ) ~ Map f (Extend ℓ τ ρ))
-> RMap f (Extend ℓ τ ρ)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict (Extend ℓ (f τ) (Map f ρ) ~ Map f (Extend ℓ τ ρ))
forall k b (f :: k -> b) (ℓ :: Symbol) (τ :: k) (r :: Row k).
Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
mapExtendSwap @f @ℓ @τ @ρ

newtype RFMap (g :: k1 -> k2) (ϕ :: Row (k2 -> *)) (ρ :: Row k1) = RFMap { RFMap g ϕ ρ -> Rec (Ap ϕ (Map g ρ))
unRFMap :: Rec (Ap ϕ (Map g ρ)) }
newtype RecAp (ϕ :: Row (k -> *)) (ρ :: Row k) = RecAp (Rec (Ap ϕ ρ))
newtype App (f :: k -> *) (a :: k) = App (f a)

-- | A function to map over a Ap record given constraints.
mapF :: forall k c g (ϕ :: Row (k -> *)) (ρ :: Row k). BiForall ϕ ρ c
     => (forall h a. (c h a) => h a -> h (g a))
     -> Rec (Ap ϕ ρ)
     -> Rec (Ap ϕ (Map g ρ))
mapF :: (forall (h :: k -> *) (a :: k). c h a => h a -> h (g a))
-> Rec (Ap ϕ ρ) -> Rec (Ap ϕ (Map g ρ))
mapF forall (h :: k -> *) (a :: k). c h a => h a -> h (g a)
f = RFMap g ϕ ρ -> Rec (Ap ϕ (Map g ρ))
forall k2 k1 (g :: k1 -> k2) (ϕ :: Row (k2 -> *)) (ρ :: Row k1).
RFMap g ϕ ρ -> Rec (Ap ϕ (Map g ρ))
unRFMap (RFMap g ϕ ρ -> Rec (Ap ϕ (Map g ρ)))
-> (Rec (Ap ϕ ρ) -> RFMap g ϕ ρ)
-> Rec (Ap ϕ ρ)
-> Rec (Ap ϕ (Map g ρ))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (Proxy App, Proxy (,))
-> (RecAp Empty Empty -> RFMap g Empty Empty)
-> (forall (ℓ :: Symbol) (τ1 :: k -> *) (τ2 :: k)
           (ρ1 :: Row (k -> *)) (ρ2 :: Row k).
    (KnownSymbol ℓ, c τ1 τ2, HasType ℓ τ1 ρ1, HasType ℓ τ2 ρ2) =>
    Label ℓ -> RecAp ρ1 ρ2 -> (RecAp (ρ1 .- ℓ) (ρ2 .- ℓ), App τ1 τ2))
-> (forall (ℓ :: Symbol) (τ1 :: k -> *) (τ2 :: k)
           (ρ1 :: Row (k -> *)) (ρ2 :: Row k).
    (KnownSymbol ℓ, c τ1 τ2, FrontExtends ℓ τ1 ρ1,
     FrontExtends ℓ τ2 ρ2, AllUniqueLabels (Extend ℓ τ1 ρ1),
     AllUniqueLabels (Extend ℓ τ2 ρ2)) =>
    Label ℓ
    -> (RFMap g ρ1 ρ2, App τ1 τ2)
    -> RFMap g (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2))
-> RecAp ϕ ρ
-> RFMap g ϕ ρ
forall k1 k2 (r1 :: Row k1) (r2 :: Row k2)
       (c :: k1 -> k2 -> Constraint) (p :: * -> * -> *)
       (f :: Row k1 -> Row k2 -> *) (g :: Row k1 -> Row k2 -> *)
       (h :: k1 -> k2 -> *).
(BiForall r1 r2 c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty Empty -> g Empty Empty)
-> (forall (ℓ :: Symbol) (τ1 :: k1) (τ2 :: k2) (ρ1 :: Row k1)
           (ρ2 :: Row k2).
    (KnownSymbol ℓ, c τ1 τ2, HasType ℓ τ1 ρ1, HasType ℓ τ2 ρ2) =>
    Label ℓ -> f ρ1 ρ2 -> p (f (ρ1 .- ℓ) (ρ2 .- ℓ)) (h τ1 τ2))
-> (forall (ℓ :: Symbol) (τ1 :: k1) (τ2 :: k2) (ρ1 :: Row k1)
           (ρ2 :: Row k2).
    (KnownSymbol ℓ, c τ1 τ2, FrontExtends ℓ τ1 ρ1,
     FrontExtends ℓ τ2 ρ2, AllUniqueLabels (Extend ℓ τ1 ρ1),
     AllUniqueLabels (Extend ℓ τ2 ρ2)) =>
    Label ℓ
    -> p (g ρ1 ρ2) (h τ1 τ2) -> g (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2))
-> f r1 r2
-> g r1 r2
biMetamorph @_ @_ @ϕ @ρ @c @(,) @RecAp @(RFMap g) @App Proxy (Proxy App, Proxy (,))
forall k (t :: k). Proxy t
Proxy RecAp Empty Empty -> RFMap g Empty Empty
forall k2 k1 (ϕ :: Row (k2 -> *)) (g :: k1 -> k2) (ρ :: Row k1) p.
(Ap ϕ (Map g ρ) ~ Empty) =>
p -> RFMap g ϕ ρ
doNil forall (ℓ :: Symbol) (τ1 :: k -> *) (τ2 :: k) (ρ1 :: Row (k -> *))
       (ρ2 :: Row k).
(KnownSymbol ℓ, c τ1 τ2, HasType ℓ τ1 ρ1, HasType ℓ τ2 ρ2) =>
Label ℓ -> RecAp ρ1 ρ2 -> (RecAp (ρ1 .- ℓ) (ρ2 .- ℓ), App τ1 τ2)
doUncons forall (ℓ :: Symbol) (τ1 :: k -> *) (τ2 :: k) (ρ1 :: Row (k -> *))
       (ρ2 :: Row k).
(KnownSymbol ℓ, c τ1 τ2, FrontExtends ℓ τ1 ρ1,
 FrontExtends ℓ τ2 ρ2, AllUniqueLabels (Extend ℓ τ1 ρ1),
 AllUniqueLabels (Extend ℓ τ2 ρ2)) =>
Label ℓ
-> (RFMap g ρ1 ρ2, App τ1 τ2)
-> RFMap g (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2)
forall (ℓ :: Symbol) (f :: k -> *) (τ :: k) (ϕ :: Row (k -> *))
       (ρ :: Row k).
(KnownSymbol ℓ, c f τ) =>
Label ℓ
-> (RFMap g ϕ ρ, App f τ) -> RFMap g (Extend ℓ f ϕ) (Extend ℓ τ ρ)
doCons (RecAp ϕ ρ -> RFMap g ϕ ρ)
-> (Rec (Ap ϕ ρ) -> RecAp ϕ ρ) -> Rec (Ap ϕ ρ) -> RFMap g ϕ ρ
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec (Ap ϕ ρ) -> RecAp ϕ ρ
forall k (ϕ :: Row (k -> *)) (ρ :: Row k).
Rec (Ap ϕ ρ) -> RecAp ϕ ρ
RecAp
  where
    doNil :: p -> RFMap g ϕ ρ
doNil p
_ = Rec (Ap ϕ (Map g ρ)) -> RFMap g ϕ ρ
forall k1 k2 (g :: k1 -> k2) (ϕ :: Row (k2 -> *)) (ρ :: Row k1).
Rec (Ap ϕ (Map g ρ)) -> RFMap g ϕ ρ
RFMap Rec (Ap ϕ (Map g ρ))
Rec Empty
empty
    doUncons :: forall ℓ f τ ϕ ρ. (KnownSymbol ℓ, c f τ, HasType ℓ f ϕ, HasType ℓ τ ρ)
             => Label ℓ -> RecAp ϕ ρ -> (RecAp (ϕ .- ℓ) (ρ .- ℓ), App f τ)
    doUncons :: Label ℓ -> RecAp ϕ ρ -> (RecAp (ϕ .- ℓ) (ρ .- ℓ), App f τ)
doUncons Label ℓ
l (RecAp Rec (Ap ϕ ρ)
r) = (Rec (Ap (ϕ .- ℓ) (ρ .- ℓ)) -> RecAp (ϕ .- ℓ) (ρ .- ℓ))
-> (f τ -> App f τ)
-> (Rec (Ap (ϕ .- ℓ) (ρ .- ℓ)), f τ)
-> (RecAp (ϕ .- ℓ) (ρ .- ℓ), App f τ)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Rec (Ap (ϕ .- ℓ) (ρ .- ℓ)) -> RecAp (ϕ .- ℓ) (ρ .- ℓ)
forall k (ϕ :: Row (k -> *)) (ρ :: Row k).
Rec (Ap ϕ ρ) -> RecAp ϕ ρ
RecAp f τ -> App f τ
forall k (f :: k -> *) (a :: k). f a -> App f a
App ((Rec (Ap (ϕ .- ℓ) (ρ .- ℓ)), f τ)
 -> (RecAp (ϕ .- ℓ) (ρ .- ℓ), App f τ))
-> (Rec (Ap (ϕ .- ℓ) (ρ .- ℓ)), f τ)
-> (RecAp (ϕ .- ℓ) (ρ .- ℓ), App f τ)
forall a b. (a -> b) -> a -> b
$ Label ℓ -> Rec (Ap ϕ ρ) -> (Rec (Ap ϕ ρ .- ℓ), Ap ϕ ρ .! ℓ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Rec r -> (Rec (r .- l), r .! l)
lazyUncons Label ℓ
l Rec (Ap ϕ ρ)
r
      (((Ap ϕ ρ .! ℓ) ≈ f τ, (Ap ϕ ρ .- ℓ) ≈ Ap (ϕ .- ℓ) (ρ .- ℓ)) =>
 (Rec (Ap (ϕ .- ℓ) (ρ .- ℓ)), f τ))
-> ((f ≈ f, τ ≈ τ)
    :- ((Ap ϕ ρ .! ℓ) ≈ f τ, (Ap ϕ ρ .- ℓ) ≈ Ap (ϕ .- ℓ) (ρ .- ℓ)))
-> (Rec (Ap (ϕ .- ℓ) (ρ .- ℓ)), f τ)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((ϕ .! ℓ) ≈ f, (ρ .! ℓ) ≈ τ)
:- ((Ap ϕ ρ .! ℓ) ≈ f τ, (Ap ϕ ρ .- ℓ) ≈ Ap (ϕ .- ℓ) (ρ .- ℓ))
forall k b (l :: Symbol) (f :: k -> b) (ϕ :: Row (k -> b)) (t :: k)
       (ρ :: Row k).
((ϕ .! l) ≈ f, (ρ .! l) ≈ t)
:- ((Ap ϕ ρ .! l) ≈ f t, (Ap ϕ ρ .- l) ≈ Ap (ϕ .- l) (ρ .- l))
apHas @ℓ @f @ϕ @τ @ρ
    doCons :: forall ℓ f τ ϕ ρ. (KnownSymbol ℓ, c f τ)
           => Label ℓ -> (RFMap g ϕ ρ, App f τ) -> RFMap g (Extend ℓ f ϕ) (Extend ℓ τ ρ)
    doCons :: Label ℓ
-> (RFMap g ϕ ρ, App f τ) -> RFMap g (Extend ℓ f ϕ) (Extend ℓ τ ρ)
doCons Label ℓ
l (RFMap Rec (Ap ϕ (Map g ρ))
r, App f τ
v) = Rec (Ap (Extend ℓ f ϕ) (Map g (Extend ℓ τ ρ)))
-> RFMap g (Extend ℓ f ϕ) (Extend ℓ τ ρ)
forall k1 k2 (g :: k1 -> k2) (ϕ :: Row (k2 -> *)) (ρ :: Row k1).
Rec (Ap ϕ (Map g ρ)) -> RFMap g ϕ ρ
RFMap (Label ℓ
-> f (g τ)
-> Rec (Ap ϕ (Map g ρ))
-> Rec (Extend ℓ (f (g τ)) (Ap ϕ (Map g ρ)))
forall a (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> a -> Rec r -> Rec (Extend l a r)
extend Label ℓ
l (f τ -> f (g τ)
forall (h :: k -> *) (a :: k). c h a => h a -> h (g a)
f @f @τ f τ
v) Rec (Ap ϕ (Map g ρ))
r)
      ((Extend ℓ (g τ) (Map g ρ) ~ Map g (Extend ℓ τ ρ)) =>
 RFMap g (Extend ℓ f ϕ) (Extend ℓ τ ρ))
-> Dict (Extend ℓ (g τ) (Map g ρ) ~ Map g (Extend ℓ τ ρ))
-> RFMap g (Extend ℓ f ϕ) (Extend ℓ τ ρ)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict (Extend ℓ (g τ) (Map g ρ) ~ Map g (Extend ℓ τ ρ))
forall k b (f :: k -> b) (ℓ :: Symbol) (τ :: k) (r :: Row k).
Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
mapExtendSwap @g @ℓ @τ @ρ
      ((Extend ℓ (f (g τ)) (Ap ϕ (Map g ρ))
  ~ Ap (Extend ℓ f ϕ) (Extend ℓ (g τ) (Map g ρ))) =>
 RFMap g (Extend ℓ f ϕ) (Extend ℓ τ ρ))
-> Dict
     (Extend ℓ (f (g τ)) (Ap ϕ (Map g ρ))
      ~ Ap (Extend ℓ f ϕ) (Extend ℓ (g τ) (Map g ρ)))
-> RFMap g (Extend ℓ f ϕ) (Extend ℓ τ ρ)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict
  (Extend ℓ (f (g τ)) (Ap ϕ (Map g ρ))
   ~ Ap (Extend ℓ f ϕ) (Extend ℓ (g τ) (Map g ρ)))
forall k b (ℓ :: Symbol) (f :: k -> b) (fs :: Row (k -> b))
       (τ :: k) (r :: Row k).
Dict (Extend ℓ (f τ) (Ap fs r) ≈ Ap (Extend ℓ f fs) (Extend ℓ τ r))
apExtendSwap @ℓ @f @ϕ @(g τ) @(Map g ρ)

-- | A function to map over a record given no constraint.
map' :: forall f r. FreeForall r => (forall a. a -> f a) -> Rec r -> Rec (Map f r)
map' :: (forall a. a -> f a) -> Rec r -> Rec (Map f r)
map' forall a. a -> f a
f = (forall a. Unconstrained1 a => a -> f a) -> Rec r -> Rec (Map f r)
forall (c :: * -> Constraint) (f :: * -> *) (r :: Row *).
Forall r c =>
(forall a. c a => a -> f a) -> Rec r -> Rec (Map f r)
map @Unconstrained1 forall a. a -> f a
forall a. Unconstrained1 a => a -> f a
f

-- | Lifts a natural transformation over a record.  In other words, it acts as a
-- record transformer to convert a record of @f a@ values to a record of @g a@
-- values.  If no constraint is needed, instantiate the first type argument with
-- 'Unconstrained1' or use 'transform''.
transform :: forall c r f g. Forall r c => (forall a. c a => f a -> g a) -> Rec (Map f r) -> Rec (Map g r)
transform :: (forall (a :: a). c a => f a -> g a)
-> Rec (Map f r) -> Rec (Map g r)
transform forall (a :: a). c a => f a -> g a
f = RMap g r -> Rec (Map g r)
forall a (f :: a -> *) (ρ :: Row a). RMap f ρ -> Rec (Map f ρ)
unRMap (RMap g r -> Rec (Map g r))
-> (Rec (Map f r) -> RMap g r) -> Rec (Map f r) -> Rec (Map g r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (Proxy f, Proxy (,))
-> (RMap f Empty -> RMap g Empty)
-> (forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> RMap f ρ -> (RMap f (ρ .- ℓ), f τ))
-> (forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> (RMap g ρ, f τ) -> RMap g (Extend ℓ τ ρ))
-> RMap f r
-> RMap g r
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @r @c @(,) @(RMap f) @(RMap g) @f Proxy (Proxy f, Proxy (,))
forall k (t :: k). Proxy t
Proxy RMap f Empty -> RMap g Empty
forall a (f :: a -> *) (ρ :: Row a) p.
(Map f ρ ~ Empty) =>
p -> RMap f ρ
doNil forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
(KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
Label ℓ -> RMap f ρ -> (RMap f (ρ .- ℓ), f τ)
doUncons forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
(KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ -> (RMap g ρ, f τ) -> RMap g (Extend ℓ τ ρ)
forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
(KnownSymbol ℓ, c τ) =>
Label ℓ -> (RMap g ρ, f τ) -> RMap g (Extend ℓ τ ρ)
doCons (RMap f r -> RMap g r)
-> (Rec (Map f r) -> RMap f r) -> Rec (Map f r) -> RMap g r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec (Map f r) -> RMap f r
forall a (f :: a -> *) (ρ :: Row a). Rec (Map f ρ) -> RMap f ρ
RMap
  where
    doNil :: p -> RMap f ρ
doNil p
_ = Rec (Map f ρ) -> RMap f ρ
forall a (f :: a -> *) (ρ :: Row a). Rec (Map f ρ) -> RMap f ρ
RMap Rec (Map f ρ)
Rec Empty
empty
    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, HasType ℓ τ ρ)
             => Label ℓ -> RMap f ρ -> (RMap f (ρ .- ℓ), f τ)
    doUncons :: Label ℓ -> RMap f ρ -> (RMap f (ρ .- ℓ), f τ)
doUncons Label ℓ
l (RMap Rec (Map f ρ)
r) = (Rec (Map f (ρ .- ℓ)) -> RMap f (ρ .- ℓ))
-> (Rec (Map f (ρ .- ℓ)), f τ) -> (RMap f (ρ .- ℓ), f τ)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Rec (Map f (ρ .- ℓ)) -> RMap f (ρ .- ℓ)
forall a (f :: a -> *) (ρ :: Row a). Rec (Map f ρ) -> RMap f ρ
RMap ((Rec (Map f (ρ .- ℓ)), f τ) -> (RMap f (ρ .- ℓ), f τ))
-> (Rec (Map f (ρ .- ℓ)), f τ) -> (RMap f (ρ .- ℓ), f τ)
forall a b. (a -> b) -> a -> b
$ Label ℓ -> Rec (Map f ρ) -> (Rec (Map f ρ .- ℓ), Map f ρ .! ℓ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Rec r -> (Rec (r .- l), r .! l)
lazyUncons Label ℓ
l Rec (Map f ρ)
r
      (((Map f ρ .! ℓ) ≈ f τ, (Map f ρ .- ℓ) ≈ Map f (ρ .- ℓ)) =>
 (Rec (Map f (ρ .- ℓ)), f τ))
-> ((τ ≈ τ)
    :- ((Map f ρ .! ℓ) ≈ f τ, (Map f ρ .- ℓ) ≈ Map f (ρ .- ℓ)))
-> (Rec (Map f (ρ .- ℓ)), f τ)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((ρ .! ℓ) ≈ τ)
:- ((Map f ρ .! ℓ) ≈ f τ, (Map f ρ .- ℓ) ≈ Map f (ρ .- ℓ))
forall k b (f :: k -> b) (l :: Symbol) (t :: k) (r :: Row k).
((r .! l) ≈ t)
:- ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l))
mapHas @f @ℓ @τ @ρ
    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
           => Label ℓ -> (RMap g ρ, f τ) -> RMap g (Extend ℓ τ ρ)
    doCons :: Label ℓ -> (RMap g ρ, f τ) -> RMap g (Extend ℓ τ ρ)
doCons Label ℓ
l (RMap Rec (Map g ρ)
r, f τ
v) = Rec (Map g (Extend ℓ τ ρ)) -> RMap g (Extend ℓ τ ρ)
forall a (f :: a -> *) (ρ :: Row a). Rec (Map f ρ) -> RMap f ρ
RMap (Label ℓ -> g τ -> Rec (Map g ρ) -> Rec (Extend ℓ (g τ) (Map g ρ))
forall a (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> a -> Rec r -> Rec (Extend l a r)
extend Label ℓ
l (f τ -> g τ
forall (a :: a). c a => f a -> g a
f f τ
v) Rec (Map g ρ)
r)
      ((Extend ℓ (g τ) (Map g ρ) ~ Map g (Extend ℓ τ ρ)) =>
 RMap g (Extend ℓ τ ρ))
-> Dict (Extend ℓ (g τ) (Map g ρ) ~ Map g (Extend ℓ τ ρ))
-> RMap g (Extend ℓ τ ρ)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict (Extend ℓ (g τ) (Map g ρ) ~ Map g (Extend ℓ τ ρ))
forall k b (f :: k -> b) (ℓ :: Symbol) (τ :: k) (r :: Row k).
Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
mapExtendSwap @g @ℓ @τ @ρ

-- | A version of 'transform' for when there is no constraint.
transform' :: forall r f g. FreeForall r => (forall a. f a -> g a) -> Rec (Map f r) -> Rec (Map g r)
transform' :: (forall (a :: a). f a -> g a) -> Rec (Map f r) -> Rec (Map g r)
transform' forall (a :: a). f a -> g a
f = (forall (a :: a). Unconstrained1 a => f a -> g a)
-> Rec (Map f r) -> Rec (Map g r)
forall a (c :: a -> Constraint) (r :: Row a) (f :: a -> *)
       (g :: a -> *).
Forall r c =>
(forall (a :: a). c a => f a -> g a)
-> Rec (Map f r) -> Rec (Map g r)
transform @Unconstrained1 @r forall (a :: a). f a -> g a
forall (a :: a). Unconstrained1 a => f a -> g a
f


data RecMapPair f g ρ = RecMapPair (Rec (Map f ρ)) (Rec (Map g ρ))

-- | Zip together two records that are the same up to the type being mapped over them,
-- combining their constituent fields with the given function.
zipTransform :: forall c r f g h .
  Forall r c => (forall a. c a => f a -> g a -> h a) -> Rec (Map f r) -> Rec (Map g r) -> Rec (Map h r)
zipTransform :: (forall (a :: a). c a => f a -> g a -> h a)
-> Rec (Map f r) -> Rec (Map g r) -> Rec (Map h r)
zipTransform forall (a :: a). c a => f a -> g a -> h a
f Rec (Map f r)
x Rec (Map g r)
y = RMap h r -> Rec (Map h r)
forall a (f :: a -> *) (ρ :: Row a). RMap f ρ -> Rec (Map f ρ)
unRMap (RMap h r -> Rec (Map h r)) -> RMap h r -> Rec (Map h r)
forall a b. (a -> b) -> a -> b
$ Proxy (Proxy h, Proxy (,))
-> (RecMapPair f g Empty -> RMap h Empty)
-> (forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> RecMapPair f g ρ -> (RecMapPair f g (ρ .- ℓ), h τ))
-> (forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> (RMap h ρ, h τ) -> RMap h (Extend ℓ τ ρ))
-> RecMapPair f g r
-> RMap h r
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @r @c @(,) @(RecMapPair f g) @(RMap h) @h Proxy (Proxy h, Proxy (,))
forall k (t :: k). Proxy t
Proxy RecMapPair f g Empty -> RMap h Empty
forall a (f :: a -> *) (ρ :: Row a) p.
(Map f ρ ~ Empty) =>
p -> RMap f ρ
doNil forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
(KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
Label ℓ -> RecMapPair f g ρ -> (RecMapPair f g (ρ .- ℓ), h τ)
doUncons forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
(KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ -> (RMap h ρ, h τ) -> RMap h (Extend ℓ τ ρ)
forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
(KnownSymbol ℓ, c τ) =>
Label ℓ -> (RMap h ρ, h τ) -> RMap h (Extend ℓ τ ρ)
doCons (RecMapPair f g r -> RMap h r) -> RecMapPair f g r -> RMap h r
forall a b. (a -> b) -> a -> b
$ Rec (Map f r) -> Rec (Map g r) -> RecMapPair f g r
forall a (f :: a -> *) (g :: a -> *) (ρ :: Row a).
Rec (Map f ρ) -> Rec (Map g ρ) -> RecMapPair f g ρ
RecMapPair Rec (Map f r)
x Rec (Map g r)
y
  where
    doNil :: p -> RMap f ρ
doNil p
_ = Rec (Map f ρ) -> RMap f ρ
forall a (f :: a -> *) (ρ :: Row a). Rec (Map f ρ) -> RMap f ρ
RMap Rec (Map f ρ)
Rec Empty
empty
    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, HasType ℓ τ ρ)
             => Label ℓ -> RecMapPair f g ρ -> (RecMapPair f g (ρ .- ℓ), h τ)
    doUncons :: Label ℓ -> RecMapPair f g ρ -> (RecMapPair f g (ρ .- ℓ), h τ)
doUncons Label ℓ
l (RecMapPair Rec (Map f ρ)
x Rec (Map g ρ)
y) = (Rec (Map f (ρ .- ℓ))
-> Rec (Map g (ρ .- ℓ)) -> RecMapPair f g (ρ .- ℓ)
forall a (f :: a -> *) (g :: a -> *) (ρ :: Row a).
Rec (Map f ρ) -> Rec (Map g ρ) -> RecMapPair f g ρ
RecMapPair (Label ℓ -> Rec (Map f ρ) -> Rec (Map f ρ .- ℓ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Rec r -> Rec (r .- l)
lazyRemove Label ℓ
l Rec (Map f ρ)
x) (Label ℓ -> Rec (Map g ρ) -> Rec (Map g ρ .- ℓ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Rec r -> Rec (r .- l)
lazyRemove Label ℓ
l Rec (Map g ρ)
y), f τ -> g τ -> h τ
forall (a :: a). c a => f a -> g a -> h a
f (Rec (Map f ρ)
x Rec (Map f ρ) -> Label ℓ -> Map f ρ .! ℓ
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Rec r -> Label l -> r .! l
.! Label ℓ
l) (Rec (Map g ρ)
y Rec (Map g ρ) -> Label ℓ -> Map g ρ .! ℓ
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Rec r -> Label l -> r .! l
.! Label ℓ
l))
      (((Map f ρ .! ℓ) ≈ f τ, (Map f ρ .- ℓ) ≈ Map f (ρ .- ℓ)) =>
 (RecMapPair f g (ρ .- ℓ), h τ))
-> ((τ ≈ τ)
    :- ((Map f ρ .! ℓ) ≈ f τ, (Map f ρ .- ℓ) ≈ Map f (ρ .- ℓ)))
-> (RecMapPair f g (ρ .- ℓ), h τ)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((ρ .! ℓ) ≈ τ)
:- ((Map f ρ .! ℓ) ≈ f τ, (Map f ρ .- ℓ) ≈ Map f (ρ .- ℓ))
forall k b (f :: k -> b) (l :: Symbol) (t :: k) (r :: Row k).
((r .! l) ≈ t)
:- ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l))
mapHas @f @ℓ @τ @ρ
      (((Map g ρ .! ℓ) ≈ g τ, (Map g ρ .- ℓ) ≈ Map g (ρ .- ℓ)) =>
 (RecMapPair f g (ρ .- ℓ), h τ))
-> ((τ ≈ τ)
    :- ((Map g ρ .! ℓ) ≈ g τ, (Map g ρ .- ℓ) ≈ Map g (ρ .- ℓ)))
-> (RecMapPair f g (ρ .- ℓ), h τ)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((ρ .! ℓ) ≈ τ)
:- ((Map g ρ .! ℓ) ≈ g τ, (Map g ρ .- ℓ) ≈ Map g (ρ .- ℓ))
forall k b (f :: k -> b) (l :: Symbol) (t :: k) (r :: Row k).
((r .! l) ≈ t)
:- ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l))
mapHas @g @ℓ @τ @ρ
    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
           => Label ℓ -> (RMap h ρ, h τ) -> RMap h (Extend ℓ τ ρ)
    doCons :: Label ℓ -> (RMap h ρ, h τ) -> RMap h (Extend ℓ τ ρ)
doCons Label ℓ
l (RMap Rec (Map h ρ)
r, h τ
h) = Rec (Map h (Extend ℓ τ ρ)) -> RMap h (Extend ℓ τ ρ)
forall a (f :: a -> *) (ρ :: Row a). Rec (Map f ρ) -> RMap f ρ
RMap (Label ℓ -> h τ -> Rec (Map h ρ) -> Rec (Extend ℓ (h τ) (Map h ρ))
forall a (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> a -> Rec r -> Rec (Extend l a r)
extend Label ℓ
l h τ
h Rec (Map h ρ)
r)
      ((Extend ℓ (h τ) (Map h ρ) ~ Map h (Extend ℓ τ ρ)) =>
 RMap h (Extend ℓ τ ρ))
-> Dict (Extend ℓ (h τ) (Map h ρ) ~ Map h (Extend ℓ τ ρ))
-> RMap h (Extend ℓ τ ρ)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict (Extend ℓ (h τ) (Map h ρ) ~ Map h (Extend ℓ τ ρ))
forall k b (f :: k -> b) (ℓ :: Symbol) (τ :: k) (r :: Row k).
Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
mapExtendSwap @h @ℓ @τ @ρ

-- | A version of 'zipTransform' for when there is no constraint.
zipTransform' :: forall r f g h .
  FreeForall r => (forall a. f a -> g a -> h a) -> Rec (Map f r) -> Rec (Map g r) -> Rec (Map h r)
zipTransform' :: (forall (a :: a). f a -> g a -> h a)
-> Rec (Map f r) -> Rec (Map g r) -> Rec (Map h r)
zipTransform' forall (a :: a). f a -> g a -> h a
f = (forall (a :: a). Unconstrained1 a => f a -> g a -> h a)
-> Rec (Map f r) -> Rec (Map g r) -> Rec (Map h r)
forall a (c :: a -> Constraint) (r :: Row a) (f :: a -> *)
       (g :: a -> *) (h :: a -> *).
Forall r c =>
(forall (a :: a). c a => f a -> g a -> h a)
-> Rec (Map f r) -> Rec (Map g r) -> Rec (Map h r)
zipTransform @Unconstrained1 @r forall (a :: a). f a -> g a -> h a
forall (a :: a). Unconstrained1 a => f a -> g a -> h a
f

-- | Traverse a function over a record.  Note that the fields of the record will
-- be accessed in lexicographic order by the labels.
traverse :: forall c f r. (Forall r c, Applicative f) => (forall a. c a => a -> f a) -> Rec r -> f (Rec r)
traverse :: (forall a. c a => a -> f a) -> Rec r -> f (Rec r)
traverse forall a. c a => a -> f a
f = (Forall r c, Applicative f) => Rec (Map f r) -> f (Rec r)
forall (f :: * -> *) (r :: Row *) (c :: * -> Constraint).
(Forall r c, Applicative f) =>
Rec (Map f r) -> f (Rec r)
sequence' @f @r @c (Rec (Map f r) -> f (Rec r))
-> (Rec r -> Rec (Map f r)) -> Rec r -> f (Rec r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. c a => a -> f a) -> Rec r -> Rec (Map f r)
forall (c :: * -> Constraint) (f :: * -> *) (r :: Row *).
Forall r c =>
(forall a. c a => a -> f a) -> Rec r -> Rec (Map f r)
map @c @f @r forall a. c a => a -> f a
f

-- | Traverse a function over a Mapped record.  Note that the fields of the record will
-- be accessed in lexicographic order by the labels.
traverseMap :: forall c f g h r.
  (Forall r c, Applicative f) => (forall a. c a => g a -> f (h a)) -> Rec (Map g r) -> f (Rec (Map h r))
traverseMap :: (forall (a :: a). c a => g a -> f (h a))
-> Rec (Map g r) -> f (Rec (Map h r))
traverseMap forall (a :: a). c a => g a -> f (h a)
f =
  (Forall (Map h r) (IsA c h), Applicative f) =>
Rec (Map f (Map h r)) -> f (Rec (Map h r))
forall (f :: * -> *) (r :: Row *) (c :: * -> Constraint).
(Forall r c, Applicative f) =>
Rec (Map f r) -> f (Rec r)
sequence' @f @(Map h r) @(IsA c h) (Rec (Map f (Map h r)) -> f (Rec (Map h r)))
-> (Rec (Map g r) -> Rec (Map f (Map h r)))
-> Rec (Map g r)
-> f (Rec (Map h r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  Forall r c => Rec (Map (Compose f h) r) -> Rec (Map f (Map h r))
forall a b (c :: a -> Constraint) (f :: b -> *) (g :: a -> b)
       (r :: Row a).
Forall r c =>
Rec (Map (Compose f g) r) -> Rec (Map f (Map g r))
uncompose' @c @f @h @r (Rec (Map (Compose f h) r) -> Rec (Map f (Map h r)))
-> (Rec (Map g r) -> Rec (Map (Compose f h) r))
-> Rec (Map g r)
-> Rec (Map f (Map h r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  (forall (a :: a). c a => g a -> Compose f h a)
-> Rec (Map g r) -> Rec (Map (Compose f h) r)
forall a (c :: a -> Constraint) (r :: Row a) (f :: a -> *)
       (g :: a -> *).
Forall r c =>
(forall (a :: a). c a => f a -> g a)
-> Rec (Map f r) -> Rec (Map g r)
transform @c @r @g @(Compose f h) (f (h a) -> Compose f h a
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (h a) -> Compose f h a)
-> (g a -> f (h a)) -> g a -> Compose f h a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g a -> f (h a)
forall (a :: a). c a => g a -> f (h a)
f)
  (Forall (Map h r) (IsA c h) => Rec (Map g r) -> f (Rec (Map h r)))
-> (Forall r c :- Forall (Map h r) (IsA c h))
-> Rec (Map g r)
-> f (Rec (Map h r))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Forall r c :- Forall (Map h r) (IsA c h)
forall k1 k2 (f :: k1 -> k2) (ρ :: Row k1) (c :: k1 -> Constraint).
Forall ρ c :- Forall (Map f ρ) (IsA c f)
mapForall @h @r @c

-- | A version of 'sequence' in which the constraint for 'Forall' can be chosen.
sequence' :: forall f r c. (Forall r c, Applicative f)
          => Rec (Map f r) -> f (Rec r)
sequence' :: Rec (Map f r) -> f (Rec r)
sequence' = Compose f Rec r -> f (Rec r)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose f Rec r -> f (Rec r))
-> (Rec (Map f r) -> Compose f Rec r) -> Rec (Map f r) -> f (Rec r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (Proxy f, Proxy (,))
-> (RMap f Empty -> Compose f Rec Empty)
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> RMap f ρ -> (RMap f (ρ .- ℓ), f τ))
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> (Compose f Rec ρ, f τ) -> Compose f Rec (Extend ℓ τ ρ))
-> RMap f r
-> Compose f Rec r
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @r @c @(,) @(RMap f) @(Compose f Rec) @f Proxy (Proxy f, Proxy (,))
forall k (t :: k). Proxy t
Proxy RMap f Empty -> Compose f Rec Empty
forall (f :: * -> *) p. Applicative f => p -> Compose f Rec Empty
doNil forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
Label ℓ -> RMap f ρ -> (RMap f (ρ .- ℓ), f τ)
doUncons forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ -> (Compose f Rec ρ, f τ) -> Compose f Rec (Extend ℓ τ ρ)
forall (f :: * -> *) (l :: Symbol) (a :: Row *) a.
(Applicative f, KnownSymbol l) =>
Label l -> (Compose f Rec a, f a) -> Compose f Rec (Extend l a a)
doCons (RMap f r -> Compose f Rec r)
-> (Rec (Map f r) -> RMap f r) -> Rec (Map f r) -> Compose f Rec r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec (Map f r) -> RMap f r
forall a (f :: a -> *) (ρ :: Row a). Rec (Map f ρ) -> RMap f ρ
RMap
  where
    doNil :: p -> Compose f Rec Empty
doNil p
_ = f (Rec Empty) -> Compose f Rec Empty
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Rec Empty -> f (Rec Empty)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Rec Empty
empty)
    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, HasType ℓ τ ρ)
             => Label ℓ -> RMap f ρ -> (RMap f (ρ .- ℓ), f τ)
    doUncons :: Label ℓ -> RMap f ρ -> (RMap f (ρ .- ℓ), f τ)
doUncons Label ℓ
l (RMap Rec (Map f ρ)
r) = (Rec (Map f (ρ .- ℓ)) -> RMap f (ρ .- ℓ))
-> (Rec (Map f (ρ .- ℓ)), f τ) -> (RMap f (ρ .- ℓ), f τ)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Rec (Map f (ρ .- ℓ)) -> RMap f (ρ .- ℓ)
forall a (f :: a -> *) (ρ :: Row a). Rec (Map f ρ) -> RMap f ρ
RMap ((Rec (Map f (ρ .- ℓ)), f τ) -> (RMap f (ρ .- ℓ), f τ))
-> (Rec (Map f (ρ .- ℓ)), f τ) -> (RMap f (ρ .- ℓ), f τ)
forall a b. (a -> b) -> a -> b
$ Label ℓ -> Rec (Map f ρ) -> (Rec (Map f ρ .- ℓ), Map f ρ .! ℓ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Rec r -> (Rec (r .- l), r .! l)
lazyUncons Label ℓ
l Rec (Map f ρ)
r
      (((Map f ρ .! ℓ) ≈ f τ, (Map f ρ .- ℓ) ≈ Map f (ρ .- ℓ)) =>
 (Rec (Map f (ρ .- ℓ)), f τ))
-> ((τ ≈ τ)
    :- ((Map f ρ .! ℓ) ≈ f τ, (Map f ρ .- ℓ) ≈ Map f (ρ .- ℓ)))
-> (Rec (Map f (ρ .- ℓ)), f τ)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((ρ .! ℓ) ≈ τ)
:- ((Map f ρ .! ℓ) ≈ f τ, (Map f ρ .- ℓ) ≈ Map f (ρ .- ℓ))
forall k b (f :: k -> b) (l :: Symbol) (t :: k) (r :: Row k).
((r .! l) ≈ t)
:- ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l))
mapHas @f @ℓ @τ @ρ
    doCons :: Label l -> (Compose f Rec a, f a) -> Compose f Rec (Extend l a a)
doCons Label l
l (Compose f (Rec a)
fr, f a
fv) = f (Rec (Extend l a a)) -> Compose f Rec (Extend l a a)
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (Rec (Extend l a a)) -> Compose f Rec (Extend l a a))
-> f (Rec (Extend l a a)) -> Compose f Rec (Extend l a a)
forall a b. (a -> b) -> a -> b
$ Label l -> a -> Rec a -> Rec (Extend l a a)
forall a (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> a -> Rec r -> Rec (Extend l a r)
extend Label l
l (a -> Rec a -> Rec (Extend l a a))
-> f a -> f (Rec a -> Rec (Extend l a a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
fv f (Rec a -> Rec (Extend l a a))
-> f (Rec a) -> f (Rec (Extend l a a))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (Rec a)
fr

-- | Applicative sequencing over a record.
sequence :: forall f r. (Applicative f, FreeForall r)
         => Rec (Map f r) -> f (Rec r)
sequence :: Rec (Map f r) -> f (Rec r)
sequence = (Forall r Unconstrained1, Applicative f) =>
Rec (Map f r) -> f (Rec r)
forall (f :: * -> *) (r :: Row *) (c :: * -> Constraint).
(Forall r c, Applicative f) =>
Rec (Map f r) -> f (Rec r)
sequence' @_ @_ @Unconstrained1

-- | This function acts as the inversion of `sequence`, allowing one to move a
-- functor level into a record.
distribute :: forall f r. (FreeForall r, Functor f) => f (Rec r) -> Rec (Map f r)
distribute :: f (Rec r) -> Rec (Map f r)
distribute  = RMap f r -> Rec (Map f r)
forall a (f :: a -> *) (ρ :: Row a). RMap f ρ -> Rec (Map f ρ)
unRMap (RMap f r -> Rec (Map f r))
-> (f (Rec r) -> RMap f r) -> f (Rec r) -> Rec (Map f r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (Proxy f, Proxy (,))
-> (Compose f Rec Empty -> RMap f Empty)
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, Unconstrained1 τ, HasType ℓ τ ρ) =>
    Label ℓ -> Compose f Rec ρ -> (Compose f Rec (ρ .- ℓ), f τ))
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, Unconstrained1 τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> (RMap f ρ, f τ) -> RMap f (Extend ℓ τ ρ))
-> Compose f Rec r
-> RMap f r
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @r @Unconstrained1 @(,) @(Compose f Rec) @(RMap f) @f Proxy (Proxy f, Proxy (,))
forall k (t :: k). Proxy t
Proxy Compose f Rec Empty -> RMap f Empty
forall a (f :: a -> *) (ρ :: Row a) p.
(Map f ρ ~ Empty) =>
p -> RMap f ρ
doNil forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, Unconstrained1 τ, HasType ℓ τ ρ) =>
Label ℓ -> Compose f Rec ρ -> (Compose f Rec (ρ .- ℓ), f τ)
forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, HasType ℓ τ ρ) =>
Label ℓ -> Compose f Rec ρ -> (Compose f Rec (ρ .- ℓ), f τ)
doUncons forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, Unconstrained1 τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ -> (RMap f ρ, f τ) -> RMap f (Extend ℓ τ ρ)
forall (ℓ :: Symbol) τ (ρ :: Row *).
KnownSymbol ℓ =>
Label ℓ -> (RMap f ρ, f τ) -> RMap f (Extend ℓ τ ρ)
doCons (Compose f Rec r -> RMap f r)
-> (f (Rec r) -> Compose f Rec r) -> f (Rec r) -> RMap f r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Rec r) -> Compose f Rec r
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose
  where
    doNil :: p -> RMap f ρ
doNil p
_ = Rec (Map f ρ) -> RMap f ρ
forall a (f :: a -> *) (ρ :: Row a). Rec (Map f ρ) -> RMap f ρ
RMap Rec (Map f ρ)
Rec Empty
empty
    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, HasType ℓ τ ρ)
             => Label ℓ -> Compose f Rec ρ -> (Compose f Rec (ρ .- ℓ), f τ)
    doUncons :: Label ℓ -> Compose f Rec ρ -> (Compose f Rec (ρ .- ℓ), f τ)
doUncons Label ℓ
l (Compose f (Rec ρ)
fr) = (f (Rec (ρ .- ℓ)) -> Compose f Rec (ρ .- ℓ)
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (Rec (ρ .- ℓ)) -> Compose f Rec (ρ .- ℓ))
-> f (Rec (ρ .- ℓ)) -> Compose f Rec (ρ .- ℓ)
forall a b. (a -> b) -> a -> b
$ Label ℓ -> Rec ρ -> Rec (ρ .- ℓ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Rec r -> Rec (r .- l)
lazyRemove Label ℓ
l (Rec ρ -> Rec (ρ .- ℓ)) -> f (Rec ρ) -> f (Rec (ρ .- ℓ))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Rec ρ)
fr, (Rec ρ -> Label ℓ -> ρ .! ℓ
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Rec r -> Label l -> r .! l
.! Label ℓ
l) (Rec ρ -> τ) -> f (Rec ρ) -> f τ
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Rec ρ)
fr)
    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ)
           => Label ℓ -> (RMap f ρ, f τ) -> RMap f (Extend ℓ τ ρ)
    doCons :: Label ℓ -> (RMap f ρ, f τ) -> RMap f (Extend ℓ τ ρ)
doCons Label ℓ
l (RMap Rec (Map f ρ)
r, f τ
fv) = Rec (Map f (Extend ℓ τ ρ)) -> RMap f (Extend ℓ τ ρ)
forall a (f :: a -> *) (ρ :: Row a). Rec (Map f ρ) -> RMap f ρ
RMap (Label ℓ -> f τ -> Rec (Map f ρ) -> Rec (Extend ℓ (f τ) (Map f ρ))
forall a (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> a -> Rec r -> Rec (Extend l a r)
extend Label ℓ
l f τ
fv Rec (Map f ρ)
r)
      ((Extend ℓ (f τ) (Map f ρ) ~ Map f (Extend ℓ τ ρ)) =>
 RMap f (Extend ℓ τ ρ))
-> Dict (Extend ℓ (f τ) (Map f ρ) ~ Map f (Extend ℓ τ ρ))
-> RMap f (Extend ℓ τ ρ)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict (Extend ℓ (f τ) (Map f ρ) ~ Map f (Extend ℓ τ ρ))
forall k b (f :: k -> b) (ℓ :: Symbol) (τ :: k) (r :: Row k).
Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
mapExtendSwap @f @ℓ @τ @ρ


-- $compose
-- We can easily convert between mapping two functors over the types of a row
-- and mapping the composition of the two functors.  The following two functions
-- perform this composition with the gaurantee that:
--
-- >>> compose . uncompose = id
--
-- >>> uncompose . compose = id

-- | A version of 'compose' in which the constraint for 'Forall' can be chosen.
compose' :: forall c f g r . Forall r c
        => Rec (Map f (Map g r)) -> Rec (Map (Compose f g) r)
compose' :: Rec (Map f (Map g r)) -> Rec (Map (Compose f g) r)
compose' = RMap (Compose f g) r -> Rec (Map (Compose f g) r)
forall a (f :: a -> *) (ρ :: Row a). RMap f ρ -> Rec (Map f ρ)
unRMap (RMap (Compose f g) r -> Rec (Map (Compose f g) r))
-> (Rec (Map f (Map g r)) -> RMap (Compose f g) r)
-> Rec (Map f (Map g r))
-> Rec (Map (Compose f g) r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (Proxy (Compose f g), Proxy (,))
-> (RMap2 f g Empty -> RMap (Compose f g) Empty)
-> (forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> RMap2 f g ρ -> (RMap2 f g (ρ .- ℓ), Compose f g τ))
-> (forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ
    -> (RMap (Compose f g) ρ, Compose f g τ)
    -> RMap (Compose f g) (Extend ℓ τ ρ))
-> RMap2 f g r
-> RMap (Compose f g) r
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @r @c @(,) @(RMap2 f g) @(RMap (Compose f g)) @(Compose f g) Proxy (Proxy (Compose f g), Proxy (,))
forall k (t :: k). Proxy t
Proxy RMap2 f g Empty -> RMap (Compose f g) Empty
forall a (f :: a -> *) (ρ :: Row a) p.
(Map f ρ ~ Empty) =>
p -> RMap f ρ
doNil forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
(KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
Label ℓ -> RMap2 f g ρ -> (RMap2 f g (ρ .- ℓ), Compose f g τ)
doUncons forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
(KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ
-> (RMap (Compose f g) ρ, Compose f g τ)
-> RMap (Compose f g) (Extend ℓ τ ρ)
forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
(KnownSymbol ℓ, c τ) =>
Label ℓ
-> (RMap (Compose f g) ρ, Compose f g τ)
-> RMap (Compose f g) (Extend ℓ τ ρ)
doCons (RMap2 f g r -> RMap (Compose f g) r)
-> (Rec (Map f (Map g r)) -> RMap2 f g r)
-> Rec (Map f (Map g r))
-> RMap (Compose f g) r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec (Map f (Map g r)) -> RMap2 f g r
forall a a (f :: a -> *) (g :: a -> a) (ρ :: Row a).
Rec (Map f (Map g ρ)) -> RMap2 f g ρ
RMap2
  where
    doNil :: p -> RMap f ρ
doNil p
_ = Rec (Map f ρ) -> RMap f ρ
forall a (f :: a -> *) (ρ :: Row a). Rec (Map f ρ) -> RMap f ρ
RMap Rec (Map f ρ)
Rec Empty
empty
    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, HasType ℓ τ ρ)
             => Label ℓ -> RMap2 f g ρ -> (RMap2 f g (ρ .- ℓ), Compose f g τ)
    doUncons :: Label ℓ -> RMap2 f g ρ -> (RMap2 f g (ρ .- ℓ), Compose f g τ)
doUncons Label ℓ
l (RMap2 Rec (Map f (Map g ρ))
r) = (Rec (Map f (Map g (ρ .- ℓ))) -> RMap2 f g (ρ .- ℓ))
-> (f (g τ) -> Compose f g τ)
-> (Rec (Map f (Map g (ρ .- ℓ))), f (g τ))
-> (RMap2 f g (ρ .- ℓ), Compose f g τ)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Rec (Map f (Map g (ρ .- ℓ))) -> RMap2 f g (ρ .- ℓ)
forall a a (f :: a -> *) (g :: a -> a) (ρ :: Row a).
Rec (Map f (Map g ρ)) -> RMap2 f g ρ
RMap2 f (g τ) -> Compose f g τ
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose ((Rec (Map f (Map g (ρ .- ℓ))), f (g τ))
 -> (RMap2 f g (ρ .- ℓ), Compose f g τ))
-> (Rec (Map f (Map g (ρ .- ℓ))), f (g τ))
-> (RMap2 f g (ρ .- ℓ), Compose f g τ)
forall a b. (a -> b) -> a -> b
$ Label ℓ
-> Rec (Map f (Map g ρ))
-> (Rec (Map f (Map g ρ) .- ℓ), Map f (Map g ρ) .! ℓ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Rec r -> (Rec (r .- l), r .! l)
lazyUncons Label ℓ
l Rec (Map f (Map g ρ))
r
      (((Map f (Map g ρ) .! ℓ) ≈ f (g τ),
  (Map f (Map g ρ) .- ℓ) ≈ Map f (Map g (ρ .- ℓ))) =>
 (Rec (Map f (Map g (ρ .- ℓ))), f (g τ)))
-> ((g τ ≈ g τ)
    :- ((Map f (Map g ρ) .! ℓ) ≈ f (g τ),
        (Map f (Map g ρ) .- ℓ) ≈ Map f (Map g (ρ .- ℓ))))
-> (Rec (Map f (Map g (ρ .- ℓ))), f (g τ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((Map g ρ .! ℓ) ≈ g τ)
:- ((Map f (Map g ρ) .! ℓ) ≈ f (g τ),
    (Map f (Map g ρ) .- ℓ) ≈ Map f (Map g ρ .- ℓ))
forall k b (f :: k -> b) (l :: Symbol) (t :: k) (r :: Row k).
((r .! l) ≈ t)
:- ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l))
mapHas @f @ℓ @(g τ) @(Map g ρ)
      (((Map g ρ .! ℓ) ≈ g τ, (Map g ρ .- ℓ) ≈ Map g (ρ .- ℓ)) =>
 (Rec (Map f (Map g (ρ .- ℓ))), f (g τ)))
-> ((τ ≈ τ)
    :- ((Map g ρ .! ℓ) ≈ g τ, (Map g ρ .- ℓ) ≈ Map g (ρ .- ℓ)))
-> (Rec (Map f (Map g (ρ .- ℓ))), f (g τ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((ρ .! ℓ) ≈ τ)
:- ((Map g ρ .! ℓ) ≈ g τ, (Map g ρ .- ℓ) ≈ Map g (ρ .- ℓ))
forall k b (f :: k -> b) (l :: Symbol) (t :: k) (r :: Row k).
((r .! l) ≈ t)
:- ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l))
mapHas @g @ℓ @τ @ρ
    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
           => Label ℓ -> (RMap (Compose f g) ρ, Compose f g τ) -> RMap (Compose f g) (Extend ℓ τ ρ)
    doCons :: Label ℓ
-> (RMap (Compose f g) ρ, Compose f g τ)
-> RMap (Compose f g) (Extend ℓ τ ρ)
doCons Label ℓ
l (RMap Rec (Map (Compose f g) ρ)
r, Compose f g τ
v) = Rec (Map (Compose f g) (Extend ℓ τ ρ))
-> RMap (Compose f g) (Extend ℓ τ ρ)
forall a (f :: a -> *) (ρ :: Row a). Rec (Map f ρ) -> RMap f ρ
RMap (Rec (Map (Compose f g) (Extend ℓ τ ρ))
 -> RMap (Compose f g) (Extend ℓ τ ρ))
-> Rec (Map (Compose f g) (Extend ℓ τ ρ))
-> RMap (Compose f g) (Extend ℓ τ ρ)
forall a b. (a -> b) -> a -> b
$ Label ℓ
-> Compose f g τ
-> Rec (Map (Compose f g) ρ)
-> Rec (Extend ℓ (Compose f g τ) (Map (Compose f g) ρ))
forall a (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> a -> Rec r -> Rec (Extend l a r)
extend Label ℓ
l Compose f g τ
v Rec (Map (Compose f g) ρ)
r
      ((Extend ℓ (Compose f g τ) (Map (Compose f g) ρ)
  ~ Map (Compose f g) (Extend ℓ τ ρ)) =>
 Rec (Map (Compose f g) (Extend ℓ τ ρ)))
-> Dict
     (Extend ℓ (Compose f g τ) (Map (Compose f g) ρ)
      ~ Map (Compose f g) (Extend ℓ τ ρ))
-> Rec (Map (Compose f g) (Extend ℓ τ ρ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict
  (Extend ℓ (Compose f g τ) (Map (Compose f g) ρ)
   ~ Map (Compose f g) (Extend ℓ τ ρ))
forall k b (f :: k -> b) (ℓ :: Symbol) (τ :: k) (r :: Row k).
Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
mapExtendSwap @(Compose f g) @ℓ @τ @ρ

-- | Convert from a record where two functors have been mapped over the types to
-- one where the composition of the two functors is mapped over the types.
compose :: forall f g r . FreeForall r
        => Rec (Map f (Map g r)) -> Rec (Map (Compose f g) r)
compose :: Rec (Map f (Map g r)) -> Rec (Map (Compose f g) r)
compose = Forall r Unconstrained1 =>
Rec (Map f (Map g r)) -> Rec (Map (Compose f g) r)
forall a k (c :: a -> Constraint) (f :: k -> *) (g :: a -> k)
       (r :: Row a).
Forall r c =>
Rec (Map f (Map g r)) -> Rec (Map (Compose f g) r)
compose' @Unconstrained1 @f @g @r

-- | A version of 'uncompose' in which the constraint for 'Forall' can be chosen.
uncompose' :: forall c f g r . Forall r c
           => Rec (Map (Compose f g) r) -> Rec (Map f (Map g r))
uncompose' :: Rec (Map (Compose f g) r) -> Rec (Map f (Map g r))
uncompose' = RMap2 f g r -> Rec (Map f (Map g r))
forall a (f :: a -> *) a (g :: a -> a) (ρ :: Row a).
RMap2 f g ρ -> Rec (Map f (Map g ρ))
unRMap2 (RMap2 f g r -> Rec (Map f (Map g r)))
-> (Rec (Map (Compose f g) r) -> RMap2 f g r)
-> Rec (Map (Compose f g) r)
-> Rec (Map f (Map g r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (Proxy (Compose f g), Proxy (,))
-> (RMap (Compose f g) Empty -> RMap2 f g Empty)
-> (forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ
    -> RMap (Compose f g) ρ
    -> (RMap (Compose f g) (ρ .- ℓ), Compose f g τ))
-> (forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ
    -> (RMap2 f g ρ, Compose f g τ) -> RMap2 f g (Extend ℓ τ ρ))
-> RMap (Compose f g) r
-> RMap2 f g r
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @r @c @(,) @(RMap (Compose f g)) @(RMap2 f g) @(Compose f g) Proxy (Proxy (Compose f g), Proxy (,))
forall k (t :: k). Proxy t
Proxy RMap (Compose f g) Empty -> RMap2 f g Empty
forall a a (f :: a -> *) (g :: a -> a) (ρ :: Row a) p.
(Map f (Map g ρ) ~ Empty) =>
p -> RMap2 f g ρ
doNil forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
(KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
Label ℓ
-> RMap (Compose f g) ρ
-> (RMap (Compose f g) (ρ .- ℓ), Compose f g τ)
doUncons forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
(KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ -> (RMap2 f g ρ, Compose f g τ) -> RMap2 f g (Extend ℓ τ ρ)
forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
(KnownSymbol ℓ, c τ) =>
Label ℓ -> (RMap2 f g ρ, Compose f g τ) -> RMap2 f g (Extend ℓ τ ρ)
doCons (RMap (Compose f g) r -> RMap2 f g r)
-> (Rec (Map (Compose f g) r) -> RMap (Compose f g) r)
-> Rec (Map (Compose f g) r)
-> RMap2 f g r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec (Map (Compose f g) r) -> RMap (Compose f g) r
forall a (f :: a -> *) (ρ :: Row a). Rec (Map f ρ) -> RMap f ρ
RMap
  where
    doNil :: p -> RMap2 f g ρ
doNil p
_ = Rec (Map f (Map g ρ)) -> RMap2 f g ρ
forall a a (f :: a -> *) (g :: a -> a) (ρ :: Row a).
Rec (Map f (Map g ρ)) -> RMap2 f g ρ
RMap2 Rec (Map f (Map g ρ))
Rec Empty
empty
    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, HasType ℓ τ ρ)
             => Label ℓ -> RMap (Compose f g) ρ -> (RMap (Compose f g) (ρ .- ℓ), Compose f g τ)
    doUncons :: Label ℓ
-> RMap (Compose f g) ρ
-> (RMap (Compose f g) (ρ .- ℓ), Compose f g τ)
doUncons Label ℓ
l (RMap Rec (Map (Compose f g) ρ)
r) = (Rec (Map (Compose f g) (ρ .- ℓ)) -> RMap (Compose f g) (ρ .- ℓ))
-> (Rec (Map (Compose f g) (ρ .- ℓ)), Compose f g τ)
-> (RMap (Compose f g) (ρ .- ℓ), Compose f g τ)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Rec (Map (Compose f g) (ρ .- ℓ)) -> RMap (Compose f g) (ρ .- ℓ)
forall a (f :: a -> *) (ρ :: Row a). Rec (Map f ρ) -> RMap f ρ
RMap ((Rec (Map (Compose f g) (ρ .- ℓ)), Compose f g τ)
 -> (RMap (Compose f g) (ρ .- ℓ), Compose f g τ))
-> (Rec (Map (Compose f g) (ρ .- ℓ)), Compose f g τ)
-> (RMap (Compose f g) (ρ .- ℓ), Compose f g τ)
forall a b. (a -> b) -> a -> b
$ Label ℓ
-> Rec (Map (Compose f g) ρ)
-> (Rec (Map (Compose f g) ρ .- ℓ), Map (Compose f g) ρ .! ℓ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Rec r -> (Rec (r .- l), r .! l)
lazyUncons Label ℓ
l Rec (Map (Compose f g) ρ)
r
      (((Map (Compose f g) ρ .! ℓ) ≈ Compose f g τ,
  (Map (Compose f g) ρ .- ℓ) ≈ Map (Compose f g) (ρ .- ℓ)) =>
 (Rec (Map (Compose f g) (ρ .- ℓ)), Compose f g τ))
-> ((τ ≈ τ)
    :- ((Map (Compose f g) ρ .! ℓ) ≈ Compose f g τ,
        (Map (Compose f g) ρ .- ℓ) ≈ Map (Compose f g) (ρ .- ℓ)))
-> (Rec (Map (Compose f g) (ρ .- ℓ)), Compose f g τ)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((ρ .! ℓ) ≈ τ)
:- ((Map (Compose f g) ρ .! ℓ) ≈ Compose f g τ,
    (Map (Compose f g) ρ .- ℓ) ≈ Map (Compose f g) (ρ .- ℓ))
forall k b (f :: k -> b) (l :: Symbol) (t :: k) (r :: Row k).
((r .! l) ≈ t)
:- ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l))
mapHas @(Compose f g) @ℓ @τ @ρ
    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
           => Label ℓ -> (RMap2 f g ρ, Compose f g τ) -> RMap2 f g (Extend ℓ τ ρ)
    doCons :: Label ℓ -> (RMap2 f g ρ, Compose f g τ) -> RMap2 f g (Extend ℓ τ ρ)
doCons Label ℓ
l (RMap2 Rec (Map f (Map g ρ))
r, Compose f (g τ)
v) = Rec (Map f (Map g (Extend ℓ τ ρ))) -> RMap2 f g (Extend ℓ τ ρ)
forall a a (f :: a -> *) (g :: a -> a) (ρ :: Row a).
Rec (Map f (Map g ρ)) -> RMap2 f g ρ
RMap2 (Rec (Map f (Map g (Extend ℓ τ ρ))) -> RMap2 f g (Extend ℓ τ ρ))
-> Rec (Map f (Map g (Extend ℓ τ ρ))) -> RMap2 f g (Extend ℓ τ ρ)
forall a b. (a -> b) -> a -> b
$ Label ℓ
-> f (g τ)
-> Rec (Map f (Map g ρ))
-> Rec (Extend ℓ (f (g τ)) (Map f (Map g ρ)))
forall a (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> a -> Rec r -> Rec (Extend l a r)
extend Label ℓ
l f (g τ)
v Rec (Map f (Map g ρ))
r
      ((Extend ℓ (f (g τ)) (Map f (Map g ρ))
  ~ Map f (Map g (Extend ℓ τ ρ))) =>
 Rec (Map f (Map g (Extend ℓ τ ρ))))
-> Dict
     (Extend ℓ (f (g τ)) (Map f (Map g ρ))
      ~ Map f (Map g (Extend ℓ τ ρ)))
-> Rec (Map f (Map g (Extend ℓ τ ρ)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict
  (Extend ℓ (f (g τ)) (Map f (Map g ρ))
   ≈ Map f (Extend ℓ (g τ) (Map g ρ)))
forall k b (f :: k -> b) (ℓ :: Symbol) (τ :: k) (r :: Row k).
Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
mapExtendSwap @f @ℓ @(g τ) @(Map g ρ)
      ((Extend ℓ (g τ) (Map g ρ) ~ Map g (Extend ℓ τ ρ)) =>
 Rec (Map f (Map g (Extend ℓ τ ρ))))
-> Dict (Extend ℓ (g τ) (Map g ρ) ~ Map g (Extend ℓ τ ρ))
-> Rec (Map f (Map g (Extend ℓ τ ρ)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict (Extend ℓ (g τ) (Map g ρ) ~ Map g (Extend ℓ τ ρ))
forall k b (f :: k -> b) (ℓ :: Symbol) (τ :: k) (r :: Row k).
Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
mapExtendSwap @g @ℓ @τ @ρ

-- | Convert from a record where the composition of two functors have been mapped
-- over the types to one where the two functors are mapped individually one at a
-- time over the types.
uncompose :: forall f g r . FreeForall r
          => Rec (Map (Compose f g) r) -> Rec (Map f (Map g r))
uncompose :: Rec (Map (Compose f g) r) -> Rec (Map f (Map g r))
uncompose = Forall r Unconstrained1 =>
Rec (Map (Compose f g) r) -> Rec (Map f (Map g r))
forall a b (c :: a -> Constraint) (f :: b -> *) (g :: a -> b)
       (r :: Row a).
Forall r c =>
Rec (Map (Compose f g) r) -> Rec (Map f (Map g r))
uncompose' @Unconstrained1 @f @g @r


-- | Coerce a record to a coercible representation.  The 'BiForall' in the context
-- indicates that the type of every field in @r1@ can be coerced to the type of
-- the corresponding fields in @r2@.
--
-- Internally, this is implemented just with `unsafeCoerce`, but we provide the
-- following implementation as a proof:
--
-- > newtype ConstR a b = ConstR (Rec a)
-- > newtype FlipConstR a b = FlipConstR { unFlipConstR :: Rec b }
-- > coerceRec :: forall r1 r2. BiForall r1 r2 Coercible => Rec r1 -> Rec r2
-- > coerceRec = unFlipConstR . biMetamorph @_ @_ @r1 @r2 @Coercible @(,) @ConstR @FlipConstR @Const Proxy doNil doUncons doCons . ConstR
-- >   where
-- >     doNil _ = FlipConstR empty
-- >     doUncons l (ConstR r) = bimap ConstR Const $ lazyUncons l r
-- >     doCons :: forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, Coercible τ1 τ2)
-- >            => Label ℓ -> (FlipConstR ρ1 ρ2, Const τ1 τ2) -> FlipConstR (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2)
-- >     doCons l (FlipConstR r, Const v) = FlipConstR $ extend l (coerce @τ1 @τ2 v) r
coerceRec :: forall r1 r2. BiForall r1 r2 Coercible => Rec r1 -> Rec r2
coerceRec :: Rec r1 -> Rec r2
coerceRec = Rec r1 -> Rec r2
forall a b. a -> b
unsafeCoerce


-- | RZipPair is used internally as a type level lambda for zipping records.
newtype RecPair  (ρ1 :: Row *) (ρ2 :: Row *) = RecPair  (Rec ρ1, Rec ρ2)
newtype RZipPair (ρ1 :: Row *) (ρ2 :: Row *) = RZipPair { RZipPair ρ1 ρ2 -> Rec (Zip ρ1 ρ2)
unRZipPair :: Rec (Zip ρ1 ρ2) }

-- | Zips together two records that have the same set of labels.
zip :: forall r1 r2. FreeBiForall r1 r2 => Rec r1 -> Rec r2 -> Rec (Zip r1 r2)
zip :: Rec r1 -> Rec r2 -> Rec (Zip r1 r2)
zip Rec r1
r1 Rec r2
r2 = RZipPair r1 r2 -> Rec (Zip r1 r2)
forall (ρ1 :: Row *) (ρ2 :: Row *).
RZipPair ρ1 ρ2 -> Rec (Zip ρ1 ρ2)
unRZipPair (RZipPair r1 r2 -> Rec (Zip r1 r2))
-> RZipPair r1 r2 -> Rec (Zip r1 r2)
forall a b. (a -> b) -> a -> b
$ Proxy (Proxy (,), Proxy (,))
-> (RecPair Empty Empty -> RZipPair Empty Empty)
-> (forall (ℓ :: Symbol) τ1 τ2 (ρ1 :: Row *) (ρ2 :: Row *).
    (KnownSymbol ℓ, Unconstrained2 τ1 τ2, HasType ℓ τ1 ρ1,
     HasType ℓ τ2 ρ2) =>
    Label ℓ
    -> RecPair ρ1 ρ2 -> (RecPair (ρ1 .- ℓ) (ρ2 .- ℓ), (τ1, τ2)))
-> (forall (ℓ :: Symbol) τ1 τ2 (ρ1 :: Row *) (ρ2 :: Row *).
    (KnownSymbol ℓ, Unconstrained2 τ1 τ2, FrontExtends ℓ τ1 ρ1,
     FrontExtends ℓ τ2 ρ2, AllUniqueLabels (Extend ℓ τ1 ρ1),
     AllUniqueLabels (Extend ℓ τ2 ρ2)) =>
    Label ℓ
    -> (RZipPair ρ1 ρ2, (τ1, τ2))
    -> RZipPair (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2))
-> RecPair r1 r2
-> RZipPair r1 r2
forall k1 k2 (r1 :: Row k1) (r2 :: Row k2)
       (c :: k1 -> k2 -> Constraint) (p :: * -> * -> *)
       (f :: Row k1 -> Row k2 -> *) (g :: Row k1 -> Row k2 -> *)
       (h :: k1 -> k2 -> *).
(BiForall r1 r2 c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty Empty -> g Empty Empty)
-> (forall (ℓ :: Symbol) (τ1 :: k1) (τ2 :: k2) (ρ1 :: Row k1)
           (ρ2 :: Row k2).
    (KnownSymbol ℓ, c τ1 τ2, HasType ℓ τ1 ρ1, HasType ℓ τ2 ρ2) =>
    Label ℓ -> f ρ1 ρ2 -> p (f (ρ1 .- ℓ) (ρ2 .- ℓ)) (h τ1 τ2))
-> (forall (ℓ :: Symbol) (τ1 :: k1) (τ2 :: k2) (ρ1 :: Row k1)
           (ρ2 :: Row k2).
    (KnownSymbol ℓ, c τ1 τ2, FrontExtends ℓ τ1 ρ1,
     FrontExtends ℓ τ2 ρ2, AllUniqueLabels (Extend ℓ τ1 ρ1),
     AllUniqueLabels (Extend ℓ τ2 ρ2)) =>
    Label ℓ
    -> p (g ρ1 ρ2) (h τ1 τ2) -> g (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2))
-> f r1 r2
-> g r1 r2
biMetamorph @_ @_ @r1 @r2 @Unconstrained2 @(,) @RecPair @RZipPair @(,) Proxy (Proxy (,), Proxy (,))
forall k (t :: k). Proxy t
Proxy RecPair Empty Empty -> RZipPair Empty Empty
forall (ρ1 :: Row *) (ρ2 :: Row *) p.
(Zip ρ1 ρ2 ~ Empty) =>
p -> RZipPair ρ1 ρ2
doNil forall (ℓ :: Symbol) τ1 τ2 (ρ1 :: Row *) (ρ2 :: Row *).
(KnownSymbol ℓ, Unconstrained2 τ1 τ2, HasType ℓ τ1 ρ1,
 HasType ℓ τ2 ρ2) =>
Label ℓ -> RecPair ρ1 ρ2 -> (RecPair (ρ1 .- ℓ) (ρ2 .- ℓ), (τ1, τ2))
forall (l :: Symbol) (r :: Row *) (r :: Row *).
KnownSymbol l =>
Label l
-> RecPair r r -> (RecPair (r .- l) (r .- l), (r .! l, r .! l))
doUncons forall (ℓ :: Symbol) τ1 τ2 (ρ1 :: Row *) (ρ2 :: Row *).
(KnownSymbol ℓ, Unconstrained2 τ1 τ2, FrontExtends ℓ τ1 ρ1,
 FrontExtends ℓ τ2 ρ2, AllUniqueLabels (Extend ℓ τ1 ρ1),
 AllUniqueLabels (Extend ℓ τ2 ρ2)) =>
Label ℓ
-> (RZipPair ρ1 ρ2, (τ1, τ2))
-> RZipPair (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2)
forall (ℓ :: Symbol) τ1 τ2 (ρ1 :: Row *) (ρ2 :: Row *).
KnownSymbol ℓ =>
Label ℓ
-> (RZipPair ρ1 ρ2, (τ1, τ2))
-> RZipPair (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2)
doCons (RecPair r1 r2 -> RZipPair r1 r2)
-> RecPair r1 r2 -> RZipPair r1 r2
forall a b. (a -> b) -> a -> b
$ (Rec r1, Rec r2) -> RecPair r1 r2
forall (ρ1 :: Row *) (ρ2 :: Row *).
(Rec ρ1, Rec ρ2) -> RecPair ρ1 ρ2
RecPair (Rec r1
r1, Rec r2
r2)
  where
    doNil :: p -> RZipPair ρ1 ρ2
doNil p
_ = Rec (Zip ρ1 ρ2) -> RZipPair ρ1 ρ2
forall (ρ1 :: Row *) (ρ2 :: Row *).
Rec (Zip ρ1 ρ2) -> RZipPair ρ1 ρ2
RZipPair Rec (Zip ρ1 ρ2)
Rec Empty
empty
    doUncons :: Label l
-> RecPair r r -> (RecPair (r .- l) (r .- l), (r .! l, r .! l))
doUncons Label l
l (RecPair (Rec r
r1, Rec r
r2)) = ((Rec (r .- l), Rec (r .- l)) -> RecPair (r .- l) (r .- l)
forall (ρ1 :: Row *) (ρ2 :: Row *).
(Rec ρ1, Rec ρ2) -> RecPair ρ1 ρ2
RecPair (Label l -> Rec r -> Rec (r .- l)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Rec r -> Rec (r .- l)
lazyRemove Label l
l Rec r
r1, Label l -> Rec r -> Rec (r .- l)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Rec r -> Rec (r .- l)
lazyRemove Label l
l Rec r
r2), (Rec r
r1 Rec r -> Label l -> r .! l
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Rec r -> Label l -> r .! l
.! Label l
l, Rec r
r2 Rec r -> Label l -> r .! l
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Rec r -> Label l -> r .! l
.! Label l
l))
    doCons :: forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ)
           => Label ℓ -> (RZipPair ρ1 ρ2, (τ1, τ2)) -> RZipPair (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2)
    doCons :: Label ℓ
-> (RZipPair ρ1 ρ2, (τ1, τ2))
-> RZipPair (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2)
doCons Label ℓ
l (RZipPair Rec (Zip ρ1 ρ2)
r, (τ1, τ2)
vs) = Rec (Zip (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2))
-> RZipPair (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2)
forall (ρ1 :: Row *) (ρ2 :: Row *).
Rec (Zip ρ1 ρ2) -> RZipPair ρ1 ρ2
RZipPair (Rec (Zip (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2))
 -> RZipPair (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2))
-> Rec (Zip (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2))
-> RZipPair (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2)
forall a b. (a -> b) -> a -> b
$ Label ℓ
-> (τ1, τ2)
-> Rec (Zip ρ1 ρ2)
-> Rec (Extend ℓ (τ1, τ2) (Zip ρ1 ρ2))
forall a (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> a -> Rec r -> Rec (Extend l a r)
extend Label ℓ
l (τ1, τ2)
vs Rec (Zip ρ1 ρ2)
r
      ((Extend ℓ (τ1, τ2) (Zip ρ1 ρ2)
  ~ Zip (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2)) =>
 Rec (Zip (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2)))
-> Dict
     (Extend ℓ (τ1, τ2) (Zip ρ1 ρ2)
      ~ Zip (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2))
-> Rec (Zip (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict
  (Extend ℓ (τ1, τ2) (Zip ρ1 ρ2)
   ~ Zip (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2))
forall (ℓ :: Symbol) τ1 (r1 :: Row *) τ2 (r2 :: Row *).
Dict
  (Extend ℓ (τ1, τ2) (Zip r1 r2)
   ≈ Zip (Extend ℓ τ1 r1) (Extend ℓ τ2 r2))
zipExtendSwap @ℓ @τ1 @ρ1 @τ2 @ρ2

{--------------------------------------------------------------------
  Record initialization
--------------------------------------------------------------------}

-- | Initialize a record with a default value at each label.
default' :: forall c ρ. (Forall ρ c, AllUniqueLabels ρ) => (forall a. c a => a) -> Rec ρ
default' :: (forall a. c a => a) -> Rec ρ
default' forall a. c a => a
v = Identity (Rec ρ) -> Rec ρ
forall a. Identity a -> a
runIdentity (Identity (Rec ρ) -> Rec ρ) -> Identity (Rec ρ) -> Rec ρ
forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) (ρ :: Row *).
(Applicative f, Forall ρ c, AllUniqueLabels ρ) =>
(forall a. c a => f a) -> f (Rec ρ)
forall (c :: * -> Constraint) (f :: * -> *) (ρ :: Row *).
(Applicative f, Forall ρ c, AllUniqueLabels ρ) =>
(forall a. c a => f a) -> f (Rec ρ)
defaultA @c ((forall a. c a => Identity a) -> Identity (Rec ρ))
-> (forall a. c a => Identity a) -> Identity (Rec ρ)
forall a b. (a -> b) -> a -> b
$ a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
forall a. c a => a
v

-- | Initialize a record with a default value at each label; works over an 'Applicative'.
defaultA :: forall c f ρ. (Applicative f, Forall ρ c, AllUniqueLabels ρ)
         => (forall a. c a => f a) -> f (Rec ρ)
defaultA :: (forall a. c a => f a) -> f (Rec ρ)
defaultA forall a. c a => f a
v = forall (f :: * -> *) (ρ :: Row *).
(Applicative f, Forall ρ c, AllUniqueLabels ρ) =>
(forall (l :: Symbol) a. (KnownSymbol l, c a) => Label l -> f a)
-> f (Rec ρ)
forall (c :: * -> Constraint) (f :: * -> *) (ρ :: Row *).
(Applicative f, Forall ρ c, AllUniqueLabels ρ) =>
(forall (l :: Symbol) a. (KnownSymbol l, c a) => Label l -> f a)
-> f (Rec ρ)
fromLabelsA @c ((forall (l :: Symbol) a. (KnownSymbol l, c a) => Label l -> f a)
 -> f (Rec ρ))
-> (forall (l :: Symbol) a. (KnownSymbol l, c a) => Label l -> f a)
-> f (Rec ρ)
forall a b. (a -> b) -> a -> b
$ f a -> Label l -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure f a
forall a. c a => f a
v

-- | Initialize a record, where each value is determined by the given function over
-- the label at that value.
fromLabels :: forall c ρ. (Forall ρ c, AllUniqueLabels ρ)
           => (forall l a. (KnownSymbol l, c a) => Label l -> a) -> Rec ρ
fromLabels :: (forall (l :: Symbol) a. (KnownSymbol l, c a) => Label l -> a)
-> Rec ρ
fromLabels forall (l :: Symbol) a. (KnownSymbol l, c a) => Label l -> a
f = Identity (Rec ρ) -> Rec ρ
forall a. Identity a -> a
runIdentity (Identity (Rec ρ) -> Rec ρ) -> Identity (Rec ρ) -> Rec ρ
forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) (ρ :: Row *).
(Applicative f, Forall ρ c, AllUniqueLabels ρ) =>
(forall (l :: Symbol) a. (KnownSymbol l, c a) => Label l -> f a)
-> f (Rec ρ)
forall (c :: * -> Constraint) (f :: * -> *) (ρ :: Row *).
(Applicative f, Forall ρ c, AllUniqueLabels ρ) =>
(forall (l :: Symbol) a. (KnownSymbol l, c a) => Label l -> f a)
-> f (Rec ρ)
fromLabelsA @c ((forall (l :: Symbol) a.
  (KnownSymbol l, c a) =>
  Label l -> Identity a)
 -> Identity (Rec ρ))
-> (forall (l :: Symbol) a.
    (KnownSymbol l, c a) =>
    Label l -> Identity a)
-> Identity (Rec ρ)
forall a b. (a -> b) -> a -> b
$ (a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> Identity a) -> (Label l -> a) -> Label l -> Identity a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) Label l -> a
forall (l :: Symbol) a. (KnownSymbol l, c a) => Label l -> a
f

-- | Initialize a record, where each value is determined by the given function over
-- the label at that value.  This function works over an 'Applicative'.
fromLabelsA :: forall c f ρ. (Applicative f, Forall ρ c, AllUniqueLabels ρ)
            => (forall l a. (KnownSymbol l, c a) => Label l -> f a) -> f (Rec ρ)
fromLabelsA :: (forall (l :: Symbol) a. (KnownSymbol l, c a) => Label l -> f a)
-> f (Rec ρ)
fromLabelsA forall (l :: Symbol) a. (KnownSymbol l, c a) => Label l -> f a
mk = Compose f Rec ρ -> f (Rec ρ)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose f Rec ρ -> f (Rec ρ)) -> Compose f Rec ρ -> f (Rec ρ)
forall a b. (a -> b) -> a -> b
$ Proxy (Proxy Proxy, Proxy Const)
-> (Const () Empty -> Compose f Rec Empty)
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> Const () ρ -> Const (Const () (ρ .- ℓ)) (Proxy τ))
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ
    -> Const (Compose f Rec ρ) (Proxy τ)
    -> Compose f Rec (Extend ℓ τ ρ))
-> Const () ρ
-> Compose f Rec ρ
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @ρ @c @Const @(Const ()) @(Compose f Rec) @Proxy Proxy (Proxy Proxy, Proxy Const)
forall k (t :: k). Proxy t
Proxy Const () Empty -> Compose f Rec Empty
forall (f :: * -> *) p. Applicative f => p -> Compose f Rec Empty
doNil forall k k p p (b :: k) (b :: k). p -> p -> Const (Const () b) b
forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
Label ℓ -> Const () ρ -> Const (Const () (ρ .- ℓ)) (Proxy τ)
doUncons forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ
-> Const (Compose f Rec ρ) (Proxy τ)
-> Compose f Rec (Extend ℓ τ ρ)
forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ) =>
Label ℓ
-> Const (Compose f Rec ρ) (Proxy τ)
-> Compose f Rec (Extend ℓ τ ρ)
doCons (() -> Const () ρ
forall k a (b :: k). a -> Const a b
Const ())
  where doNil :: p -> Compose f Rec Empty
doNil p
_ = f (Rec Empty) -> Compose f Rec Empty
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (Rec Empty) -> Compose f Rec Empty)
-> f (Rec Empty) -> Compose f Rec Empty
forall a b. (a -> b) -> a -> b
$ Rec Empty -> f (Rec Empty)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Rec Empty
empty
        doUncons :: p -> p -> Const (Const () b) b
doUncons p
_ p
_ = Const () b -> Const (Const () b) b
forall k a (b :: k). a -> Const a b
Const (Const () b -> Const (Const () b) b)
-> Const () b -> Const (Const () b) b
forall a b. (a -> b) -> a -> b
$ () -> Const () b
forall k a (b :: k). a -> Const a b
Const ()
        doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
               => Label ℓ -> Const (Compose f Rec ρ) (Proxy τ) -> Compose f Rec (Extend ℓ τ ρ)
        doCons :: Label ℓ
-> Const (Compose f Rec ρ) (Proxy τ)
-> Compose f Rec (Extend ℓ τ ρ)
doCons Label ℓ
l (Const (Compose f (Rec ρ)
r)) = f (Rec (Extend ℓ τ ρ)) -> Compose f Rec (Extend ℓ τ ρ)
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (Rec (Extend ℓ τ ρ)) -> Compose f Rec (Extend ℓ τ ρ))
-> f (Rec (Extend ℓ τ ρ)) -> Compose f Rec (Extend ℓ τ ρ)
forall a b. (a -> b) -> a -> b
$ Label ℓ -> τ -> Rec ρ -> Rec (Extend ℓ τ ρ)
forall a (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> a -> Rec r -> Rec (Extend l a r)
extend Label ℓ
l (τ -> Rec ρ -> Rec (Extend ℓ τ ρ))
-> f τ -> f (Rec ρ -> Rec (Extend ℓ τ ρ))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Label ℓ -> f τ
forall (l :: Symbol) a. (KnownSymbol l, c a) => Label l -> f a
mk @ℓ @τ Label ℓ
l f (Rec ρ -> Rec (Extend ℓ τ ρ))
-> f (Rec ρ) -> f (Rec (Extend ℓ τ ρ))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (Rec ρ)
r

-- | Initialize a record over a `Map`.
fromLabelsMapA :: forall c f g ρ. (Applicative f, Forall ρ c, AllUniqueLabels ρ)
               => (forall l a. (KnownSymbol l, c a) => Label l -> f (g a)) -> f (Rec (Map g ρ))
fromLabelsMapA :: (forall (l :: Symbol) (a :: a).
 (KnownSymbol l, c a) =>
 Label l -> f (g a))
-> f (Rec (Map g ρ))
fromLabelsMapA forall (l :: Symbol) (a :: a).
(KnownSymbol l, c a) =>
Label l -> f (g a)
f = (forall (l :: Symbol) a.
 (KnownSymbol l, IsA c g a) =>
 Label l -> f a)
-> f (Rec (Map g ρ))
forall (c :: * -> Constraint) (f :: * -> *) (ρ :: Row *).
(Applicative f, Forall ρ c, AllUniqueLabels ρ) =>
(forall (l :: Symbol) a. (KnownSymbol l, c a) => Label l -> f a)
-> f (Rec ρ)
fromLabelsA @(IsA c g) @f @(Map g ρ) forall (l :: Symbol) a.
(KnownSymbol l, IsA c g a) =>
Label l -> f a
inner
                (Forall (Map g ρ) (IsA c g) => f (Rec (Map g ρ)))
-> (Forall ρ c :- Forall (Map g ρ) (IsA c g)) -> f (Rec (Map g ρ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Forall ρ c :- Forall (Map g ρ) (IsA c g)
forall k1 k2 (f :: k1 -> k2) (ρ :: Row k1) (c :: k1 -> Constraint).
Forall ρ c :- Forall (Map f ρ) (IsA c f)
mapForall @g @ρ @c
                ((AllUniqueLabels (Map g ρ) ~ AllUniqueLabels ρ) =>
 f (Rec (Map g ρ)))
-> Dict (AllUniqueLabels (Map g ρ) ~ AllUniqueLabels ρ)
-> f (Rec (Map g ρ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict (AllUniqueLabels (Map g ρ) ~ AllUniqueLabels ρ)
forall k1 k2 (f :: k1 -> k2) (r :: Row k1).
Dict (AllUniqueLabels (Map f r) ≈ AllUniqueLabels r)
uniqueMap @g @ρ
   where inner :: forall l a. (KnownSymbol l, IsA c g a) => Label l -> f a
         inner :: Label l -> f a
inner Label l
l = case IsA c g a => As c g a
forall k k (c :: k -> Constraint) (f :: k -> k) (a :: k).
IsA c f a =>
As c f a
as @c @g @a of As c g a
As -> Label l -> f (g t)
forall (l :: Symbol) (a :: a).
(KnownSymbol l, c a) =>
Label l -> f (g a)
f Label l
l


{--------------------------------------------------------------------
  Dynamic compatibility
--------------------------------------------------------------------}

-- | Converts a 'Rec' into a 'HashMap' of 'Dynamic's.
toDynamicMap :: Forall r Typeable => Rec r -> HashMap Text Dynamic
toDynamicMap :: Rec r -> HashMap Text Dynamic
toDynamicMap = (forall a. Typeable a => a -> Dynamic)
-> Rec r -> HashMap Text Dynamic
forall (c :: * -> Constraint) (r :: Row *) s b.
(IsString s, Eq s, Hashable s, Forall r c) =>
(forall a. c a => a -> b) -> Rec r -> HashMap s b
eraseToHashMap @Typeable @_ @Text @Dynamic forall a. Typeable a => a -> Dynamic
toDyn

-- | Produces a 'Rec' from a 'HashMap' of 'Dynamic's.
fromDynamicMap :: (AllUniqueLabels r, Forall r Typeable)
               => HashMap Text Dynamic -> Maybe (Rec r)
fromDynamicMap :: HashMap Text Dynamic -> Maybe (Rec r)
fromDynamicMap HashMap Text Dynamic
m = forall (f :: * -> *) (ρ :: Row *).
(Applicative f, Forall ρ Typeable, AllUniqueLabels ρ) =>
(forall (l :: Symbol) a.
 (KnownSymbol l, Typeable a) =>
 Label l -> f a)
-> f (Rec ρ)
forall (c :: * -> Constraint) (f :: * -> *) (ρ :: Row *).
(Applicative f, Forall ρ c, AllUniqueLabels ρ) =>
(forall (l :: Symbol) a. (KnownSymbol l, c a) => Label l -> f a)
-> f (Rec ρ)
fromLabelsA @Typeable
  ((forall (l :: Symbol) a.
  (KnownSymbol l, Typeable a) =>
  Label l -> Maybe a)
 -> Maybe (Rec r))
-> (forall (l :: Symbol) a.
    (KnownSymbol l, Typeable a) =>
    Label l -> Maybe a)
-> Maybe (Rec r)
forall a b. (a -> b) -> a -> b
$ \ (Label l -> Text
forall (s :: Symbol). KnownSymbol s => Label s -> Text
toKey -> Text
k) -> Text -> HashMap Text Dynamic -> Maybe Dynamic
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Text
k HashMap Text Dynamic
m Maybe Dynamic -> (Dynamic -> Maybe a) -> Maybe a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Dynamic -> Maybe a
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic


{--------------------------------------------------------------------
  Generic instance
--------------------------------------------------------------------}

-- The generic structure we want Recs to have is not the hidden internal one,
-- but rather one that appears as a Haskell record.  Thus, we can't derive
-- Generic automatically.
--
-- The following Generic instance creates a representation of a Rec that is
-- very similar to a native Haskell record except that the tree of pairs (':*:')
-- that it produces will be extremely unbalanced.  I don't think this is a problem.
-- Furthermore, because we don't want Recs to always have a trailing unit on
-- the end, we must have a special case for singleton Recs, which means that
-- we can't use metamorph.

instance GenericRec r => G.Generic (Rec r) where
  type Rep (Rec r) =
    G.D1 ('G.MetaData "Rec" "Data.Row.Records" "row-types" 'False)
      (G.C1 ('G.MetaCons "Rec" 'G.PrefixI 'True)
        (RepRec r))
  from :: Rec r -> Rep (Rec r) x
from = M1 C ('MetaCons "Rec" 'PrefixI 'True) (RepRec r) x
-> M1
     D
     ('MetaData "Rec" "Data.Row.Records" "row-types" 'False)
     (M1 C ('MetaCons "Rec" 'PrefixI 'True) (RepRec r))
     x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (M1 C ('MetaCons "Rec" 'PrefixI 'True) (RepRec r) x
 -> M1
      D
      ('MetaData "Rec" "Data.Row.Records" "row-types" 'False)
      (M1 C ('MetaCons "Rec" 'PrefixI 'True) (RepRec r))
      x)
-> (Rec r -> M1 C ('MetaCons "Rec" 'PrefixI 'True) (RepRec r) x)
-> Rec r
-> M1
     D
     ('MetaData "Rec" "Data.Row.Records" "row-types" 'False)
     (M1 C ('MetaCons "Rec" 'PrefixI 'True) (RepRec r))
     x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RepRec r x -> M1 C ('MetaCons "Rec" 'PrefixI 'True) (RepRec r) x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (RepRec r x -> M1 C ('MetaCons "Rec" 'PrefixI 'True) (RepRec r) x)
-> (Rec r -> RepRec r x)
-> Rec r
-> M1 C ('MetaCons "Rec" 'PrefixI 'True) (RepRec r) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec r -> RepRec r x
forall (r :: Row *) x. GenericRec r => Rec r -> RepRec r x
fromRec
  to :: Rep (Rec r) x -> Rec r
to = RepRec r x -> Rec r
forall (r :: Row *) x. GenericRec r => RepRec r x -> Rec r
toRec (RepRec r x -> Rec r)
-> (M1
      D
      ('MetaData "Rec" "Data.Row.Records" "row-types" 'False)
      (M1 C ('MetaCons "Rec" 'PrefixI 'True) (RepRec r))
      x
    -> RepRec r x)
-> M1
     D
     ('MetaData "Rec" "Data.Row.Records" "row-types" 'False)
     (M1 C ('MetaCons "Rec" 'PrefixI 'True) (RepRec r))
     x
-> Rec r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 C ('MetaCons "Rec" 'PrefixI 'True) (RepRec r) x -> RepRec r x
forall i (c :: Meta) k (f :: k -> *) (p :: k). M1 i c f p -> f p
G.unM1 (M1 C ('MetaCons "Rec" 'PrefixI 'True) (RepRec r) x -> RepRec r x)
-> (M1
      D
      ('MetaData "Rec" "Data.Row.Records" "row-types" 'False)
      (M1 C ('MetaCons "Rec" 'PrefixI 'True) (RepRec r))
      x
    -> M1 C ('MetaCons "Rec" 'PrefixI 'True) (RepRec r) x)
-> M1
     D
     ('MetaData "Rec" "Data.Row.Records" "row-types" 'False)
     (M1 C ('MetaCons "Rec" 'PrefixI 'True) (RepRec r))
     x
-> RepRec r x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1
  D
  ('MetaData "Rec" "Data.Row.Records" "row-types" 'False)
  (M1 C ('MetaCons "Rec" 'PrefixI 'True) (RepRec r))
  x
-> M1 C ('MetaCons "Rec" 'PrefixI 'True) (RepRec r) x
forall i (c :: Meta) k (f :: k -> *) (p :: k). M1 i c f p -> f p
G.unM1

class GenericRec r where
  type RepRec (r :: Row *) :: * -> *
  fromRec :: Rec r -> RepRec r x
  toRec   :: RepRec r x -> Rec r

instance GenericRec Empty where
  type RepRec (R '[]) = G.U1
  fromRec :: Rec Empty -> RepRec Empty x
fromRec Rec Empty
_ = RepRec Empty x
forall k (p :: k). U1 p
G.U1
  toRec :: RepRec Empty x -> Rec Empty
toRec RepRec Empty x
_ = Rec Empty
empty

instance KnownSymbol name => GenericRec (R '[name :-> t]) where
  type RepRec (R (name :-> t ': '[])) = G.S1
    ('G.MetaSel ('Just name) 'G.NoSourceUnpackedness 'G.NoSourceStrictness 'G.DecidedLazy)
    (G.Rec0 t)
  fromRec :: Rec ('R '[ name ':-> t]) -> RepRec ('R '[ name ':-> t]) x
fromRec (_ :== a) = K1 R t x
-> M1
     S
     ('MetaSel
        ('Just name)
        'NoSourceUnpackedness
        'NoSourceStrictness
        'DecidedLazy)
     (K1 R t)
     x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (t -> K1 R t x
forall k i c (p :: k). c -> K1 i c p
G.K1 t
a)
  toRec :: RepRec ('R '[ name ':-> t]) x -> Rec ('R '[ name ':-> t])
toRec (G.M1 (G.K1 a)) = (Label name
forall (s :: Symbol). Label s
Label @name) Label name -> t -> Rec (name .== t)
forall (l :: Symbol) a.
KnownSymbol l =>
Label l -> a -> Rec (l .== a)
:== t
a

instance
    ( r ~ (name' :-> t' ': r'), GenericRec (R r)
    , KnownSymbol name, Extend name t ('R r) ≈ 'R (name :-> t ': r)
    ) => GenericRec (R (name :-> t ': (name' :-> t' ': r'))) where
  type RepRec (R (name :-> t ': (name' :-> t' ': r'))) = (G.S1
    ('G.MetaSel ('Just name) 'G.NoSourceUnpackedness 'G.NoSourceStrictness 'G.DecidedLazy)
    (G.Rec0 t)) G.:*: RepRec (R (name' :-> t' ': r'))
  fromRec :: Rec ('R ((name ':-> t) : (name' ':-> t') : r'))
-> RepRec ('R ((name ':-> t) : (name' ':-> t') : r')) x
fromRec Rec ('R ((name ':-> t) : (name' ':-> t') : r'))
r = K1 R t x
-> M1
     S
     ('MetaSel
        ('Just name)
        'NoSourceUnpackedness
        'NoSourceStrictness
        'DecidedLazy)
     (K1 R t)
     x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (t -> K1 R t x
forall k i c (p :: k). c -> K1 i c p
G.K1 (Rec ('R ((name ':-> t) : (name' ':-> t') : r'))
r Rec ('R ((name ':-> t) : (name' ':-> t') : r'))
-> Label name -> 'R ((name ':-> t) : (name' ':-> t') : r') .! name
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Rec r -> Label l -> r .! l
.! Label name
forall (s :: Symbol). Label s
Label @name)) M1
  S
  ('MetaSel
     ('Just name)
     'NoSourceUnpackedness
     'NoSourceStrictness
     'DecidedLazy)
  (K1 R t)
  x
-> RepRec ('R ((name' ':-> t') : r')) x
-> (:*:)
     (M1
        S
        ('MetaSel
           ('Just name)
           'NoSourceUnpackedness
           'NoSourceStrictness
           'DecidedLazy)
        (K1 R t))
     (RepRec ('R ((name' ':-> t') : r')))
     x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
G.:*: Rec ('R ((name' ':-> t') : r'))
-> RepRec ('R ((name' ':-> t') : r')) x
forall (r :: Row *) x. GenericRec r => Rec r -> RepRec r x
fromRec (Label name
-> Rec ('R ((name ':-> t) : (name' ':-> t') : r'))
-> Rec ('R ((name ':-> t) : (name' ':-> t') : r') .- name)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Rec r -> Rec (r .- l)
lazyRemove @name Label name
forall (s :: Symbol). Label s
Label Rec ('R ((name ':-> t) : (name' ':-> t') : r'))
r)
  toRec :: RepRec ('R ((name ':-> t) : (name' ':-> t') : r')) x
-> Rec ('R ((name ':-> t) : (name' ':-> t') : r'))
toRec (G.M1 (G.K1 a) G.:*: r) = Label name
-> t
-> Rec ('R ((name' ':-> t') : r'))
-> Rec (Extend name t ('R ((name' ':-> t') : r')))
forall a (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> a -> Rec r -> Rec (Extend l a r)
extend @_ @name @('R (name' :-> t' ': r')) Label name
forall (s :: Symbol). Label s
Label t
a (RepRec ('R ((name' ':-> t') : r')) x
-> Rec ('R ((name' ':-> t') : r'))
forall (r :: Row *) x. GenericRec r => RepRec r x -> Rec r
toRec RepRec ('R ((name' ':-> t') : r')) x
r)

{--------------------------------------------------------------------
  Native data type compatibility
--------------------------------------------------------------------}
-- ToNative is shamelessly copied from
--   https://www.athiemann.net/2017/07/02/superrecord.html

-- $native
-- The 'toNative' and 'fromNative' functions allow one to convert between
-- 'Rec's and regular Haskell data types ("native" types) that have a single constructor and any
-- number of named fields with the same names and types as the 'Rec'.  As expected,
-- they compose to form the identity.  Alternatively, one may use 'toNativeGeneral',
-- which allows fields to be dropped when a record has excess fields compared
-- to the native type.  Because of this, 'toNativeGeneral' requires a type
-- application (although 'fromNative' does not).  The only requirement is that
-- the native Haskell data type be an instance of 'Generic'.
--
-- For example, consider the following simple data type:
--
-- >>> data Person = Person { name :: String, age :: Int} deriving (Generic, Show)
--
-- Then, we have the following:
--
-- >>> toNative @Person $ #name .== "Alice" .+ #age .== 7 .+ #hasDog .== True
-- Person {name = "Alice", age = 7}
-- >>> fromNative $ Person "Bob" 9
-- { age=9, name="Bob" }

type family NativeRow t where
  NativeRow t = NativeRowG (G.Rep t)

type family NativeRowG t where
  NativeRowG (G.M1 G.D m cs) = NativeRowG cs
  NativeRowG (G.M1 G.C m cs) = NativeRowG cs
  NativeRowG G.U1 = Empty
  NativeRowG (l G.:*: r) = NativeRowG l .+ NativeRowG r
  NativeRowG (G.M1 G.S ('G.MetaSel ('Just name) p s l) (G.Rec0 t)) = name .== t


-- | Conversion helper to turn a Haskell record into a row-types extensible
-- record. Note that the native Haskell type must be an instance of 'Generic'.
class FromNativeG a where
  fromNative' :: a x -> Rec (NativeRowG a)

instance FromNativeG cs => FromNativeG (G.D1 m cs) where
  fromNative' :: D1 m cs x -> Rec (NativeRowG (D1 m cs))
fromNative' (G.M1 cs x
xs) = cs x -> Rec (NativeRowG cs)
forall k (a :: k -> *) (x :: k).
FromNativeG a =>
a x -> Rec (NativeRowG a)
fromNative' cs x
xs

instance FromNativeG cs => FromNativeG (G.C1 m cs) where
  fromNative' :: C1 m cs x -> Rec (NativeRowG (C1 m cs))
fromNative' (G.M1 cs x
xs) = cs x -> Rec (NativeRowG cs)
forall k (a :: k -> *) (x :: k).
FromNativeG a =>
a x -> Rec (NativeRowG a)
fromNative' cs x
xs

instance FromNativeG G.U1 where
  fromNative' :: U1 x -> Rec (NativeRowG U1)
fromNative' U1 x
G.U1 = Rec Empty
Rec (NativeRowG U1)
empty

instance KnownSymbol name => FromNativeG (G.S1 ('G.MetaSel ('Just name) p s l) (G.Rec0 t)) where
  fromNative' :: S1 ('MetaSel ('Just name) p s l) (Rec0 t) x
-> Rec (NativeRowG (S1 ('MetaSel ('Just name) p s l) (Rec0 t)))
fromNative' (G.M1 (G.K1 t
x)) =  (Label name
forall (s :: Symbol). Label s
Label @name) Label name -> t -> Rec (name .== t)
forall (l :: Symbol) a.
KnownSymbol l =>
Label l -> a -> Rec (l .== a)
.== t
x

instance (FromNativeG l, FromNativeG r, FreeForall (NativeRowG l)) => FromNativeG (l G.:*: r) where
  fromNative' :: (:*:) l r x -> Rec (NativeRowG (l :*: r))
fromNative' (l x
x G.:*: r x
y) = l x -> Rec (NativeRowG l)
forall k (a :: k -> *) (x :: k).
FromNativeG a =>
a x -> Rec (NativeRowG a)
fromNative' @l l x
x Rec (NativeRowG l)
-> Rec (NativeRowG r) -> Rec (NativeRowG l .+ NativeRowG r)
forall (l :: Row *) (r :: Row *).
FreeForall l =>
Rec l -> Rec r -> Rec (l .+ r)
.+ r x -> Rec (NativeRowG r)
forall k (a :: k -> *) (x :: k).
FromNativeG a =>
a x -> Rec (NativeRowG a)
fromNative' @r r x
y

type FromNative t = (G.Generic t, FromNativeG (G.Rep t))

-- | Convert a Haskell record to a row-types Rec.
fromNative :: FromNative t => t -> Rec (NativeRow t)
fromNative :: t -> Rec (NativeRow t)
fromNative = Rep t Any -> Rec (NativeRowG (Rep t))
forall k (a :: k -> *) (x :: k).
FromNativeG a =>
a x -> Rec (NativeRowG a)
fromNative' (Rep t Any -> Rec (NativeRowG (Rep t)))
-> (t -> Rep t Any) -> t -> Rec (NativeRowG (Rep t))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Rep t Any
forall a x. Generic a => a -> Rep a x
G.from


-- | Conversion helper to bring a record back into a Haskell type. Note that the
-- native Haskell type must be an instance of 'Generic'.
class ToNativeG a where
  toNative' :: Rec (NativeRowG a) -> a x

instance ToNativeG cs => ToNativeG (G.D1 m cs) where
  toNative' :: Rec (NativeRowG (D1 m cs)) -> D1 m cs x
toNative' Rec (NativeRowG (D1 m cs))
xs = cs x -> D1 m cs x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (cs x -> D1 m cs x) -> cs x -> D1 m cs x
forall a b. (a -> b) -> a -> b
$ Rec (NativeRowG cs) -> cs x
forall k (a :: k -> *) (x :: k).
ToNativeG a =>
Rec (NativeRowG a) -> a x
toNative' Rec (NativeRowG cs)
Rec (NativeRowG (D1 m cs))
xs

instance ToNativeG cs => ToNativeG (G.C1 m cs) where
  toNative' :: Rec (NativeRowG (C1 m cs)) -> C1 m cs x
toNative' Rec (NativeRowG (C1 m cs))
xs = cs x -> C1 m cs x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (cs x -> C1 m cs x) -> cs x -> C1 m cs x
forall a b. (a -> b) -> a -> b
$ Rec (NativeRowG cs) -> cs x
forall k (a :: k -> *) (x :: k).
ToNativeG a =>
Rec (NativeRowG a) -> a x
toNative' Rec (NativeRowG cs)
Rec (NativeRowG (C1 m cs))
xs

instance ToNativeG G.U1 where
  toNative' :: Rec (NativeRowG U1) -> U1 x
toNative' Rec (NativeRowG U1)
_ = U1 x
forall k (p :: k). U1 p
G.U1

instance (KnownSymbol name) => ToNativeG (G.S1 ('G.MetaSel ('Just name) p s l) (G.Rec0 t)) where
  toNative' :: Rec (NativeRowG (S1 ('MetaSel ('Just name) p s l) (Rec0 t)))
-> S1 ('MetaSel ('Just name) p s l) (Rec0 t) x
toNative' Rec (NativeRowG (S1 ('MetaSel ('Just name) p s l) (Rec0 t)))
r = K1 R t x -> S1 ('MetaSel ('Just name) p s l) (Rec0 t) x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (K1 R t x -> S1 ('MetaSel ('Just name) p s l) (Rec0 t) x)
-> K1 R t x -> S1 ('MetaSel ('Just name) p s l) (Rec0 t) x
forall a b. (a -> b) -> a -> b
$ t -> K1 R t x
forall k i c (p :: k). c -> K1 i c p
G.K1 (t -> K1 R t x) -> t -> K1 R t x
forall a b. (a -> b) -> a -> b
$ Rec ('R '[ name ':-> t])
Rec (NativeRowG (S1 ('MetaSel ('Just name) p s l) (Rec0 t)))
r Rec ('R '[ name ':-> t])
-> Label name -> 'R '[ name ':-> t] .! name
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Rec r -> Label l -> r .! l
.! (Label name
forall (s :: Symbol). Label s
Label @name)

instance (ToNativeG l, ToNativeG r, Disjoint (NativeRowG l) (NativeRowG r))
    => ToNativeG (l G.:*: r) where
  toNative' :: Rec (NativeRowG (l :*: r)) -> (:*:) l r x
toNative' Rec (NativeRowG (l :*: r))
r = Rec (NativeRowG l) -> l x
forall k (a :: k -> *) (x :: k).
ToNativeG a =>
Rec (NativeRowG a) -> a x
toNative' Rec (NativeRowG l)
r1 l x -> r x -> (:*:) l r x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
G.:*: Rec (NativeRowG r) -> r x
forall k (a :: k -> *) (x :: k).
ToNativeG a =>
Rec (NativeRowG a) -> a x
toNative' Rec (NativeRowG r)
r2
    where
      (r1 :: Rec (NativeRowG l)) :+ (r2 :: Rec (NativeRowG r)) = Rec (NativeRowG l .+ NativeRowG r)
Rec (NativeRowG (l :*: r))
r

type ToNative t = (G.Generic t, ToNativeG (G.Rep t))

-- | Convert a record to an exactly matching native Haskell type.
toNative :: ToNative t => Rec (NativeRow t) -> t
toNative :: Rec (NativeRow t) -> t
toNative = Rep t Any -> t
forall a x. Generic a => Rep a x -> a
G.to (Rep t Any -> t)
-> (Rec (NativeRowG (Rep t)) -> Rep t Any)
-> Rec (NativeRowG (Rep t))
-> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec (NativeRowG (Rep t)) -> Rep t Any
forall k (a :: k -> *) (x :: k).
ToNativeG a =>
Rec (NativeRowG a) -> a x
toNative'



-- | Conversion helper to bring a record back into a Haskell type. Note that the
-- native Haskell type must be an instance of 'Generic'.
class ToNativeGeneralG a ρ where
  toNativeGeneral' :: Rec ρ -> a x

instance ToNativeGeneralG cs ρ => ToNativeGeneralG (G.D1 m cs) ρ where
  toNativeGeneral' :: Rec ρ -> D1 m cs x
toNativeGeneral' Rec ρ
xs = cs x -> D1 m cs x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (cs x -> D1 m cs x) -> cs x -> D1 m cs x
forall a b. (a -> b) -> a -> b
$ Rec ρ -> cs x
forall k (a :: k -> *) (ρ :: Row *) (x :: k).
ToNativeGeneralG a ρ =>
Rec ρ -> a x
toNativeGeneral' Rec ρ
xs

instance ToNativeGeneralG cs ρ => ToNativeGeneralG (G.C1 m cs) ρ where
  toNativeGeneral' :: Rec ρ -> C1 m cs x
toNativeGeneral' Rec ρ
xs = cs x -> C1 m cs x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (cs x -> C1 m cs x) -> cs x -> C1 m cs x
forall a b. (a -> b) -> a -> b
$ Rec ρ -> cs x
forall k (a :: k -> *) (ρ :: Row *) (x :: k).
ToNativeGeneralG a ρ =>
Rec ρ -> a x
toNativeGeneral' Rec ρ
xs

instance ToNativeGeneralG G.U1 ρ where
  toNativeGeneral' :: Rec ρ -> U1 x
toNativeGeneral' Rec ρ
_ = U1 x
forall k (p :: k). U1 p
G.U1

instance (KnownSymbol name, ρ .! name ≈ t)
    => ToNativeGeneralG (G.S1 ('G.MetaSel ('Just name) p s l) (G.Rec0 t)) ρ where
  toNativeGeneral' :: Rec ρ -> S1 ('MetaSel ('Just name) p s l) (Rec0 t) x
toNativeGeneral' Rec ρ
r = K1 R t x -> S1 ('MetaSel ('Just name) p s l) (Rec0 t) x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (K1 R t x -> S1 ('MetaSel ('Just name) p s l) (Rec0 t) x)
-> K1 R t x -> S1 ('MetaSel ('Just name) p s l) (Rec0 t) x
forall a b. (a -> b) -> a -> b
$ t -> K1 R t x
forall k i c (p :: k). c -> K1 i c p
G.K1 (t -> K1 R t x) -> t -> K1 R t x
forall a b. (a -> b) -> a -> b
$ Rec ρ
r Rec ρ -> Label name -> ρ .! name
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Rec r -> Label l -> r .! l
.! (Label name
forall (s :: Symbol). Label s
Label @name)

instance (ToNativeGeneralG l ρ, ToNativeGeneralG r ρ)
    => ToNativeGeneralG (l G.:*: r) ρ where
  toNativeGeneral' :: Rec ρ -> (:*:) l r x
toNativeGeneral' Rec ρ
r = Rec ρ -> l x
forall k (a :: k -> *) (ρ :: Row *) (x :: k).
ToNativeGeneralG a ρ =>
Rec ρ -> a x
toNativeGeneral' Rec ρ
r l x -> r x -> (:*:) l r x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
G.:*: Rec ρ -> r x
forall k (a :: k -> *) (ρ :: Row *) (x :: k).
ToNativeGeneralG a ρ =>
Rec ρ -> a x
toNativeGeneral' Rec ρ
r

type ToNativeGeneral t ρ = (G.Generic t, ToNativeGeneralG (G.Rep t) ρ)

-- | Convert a record to a native Haskell type.
toNativeGeneral :: ToNativeGeneral t ρ => Rec ρ -> t
toNativeGeneral :: Rec ρ -> t
toNativeGeneral = Rep t Any -> t
forall a x. Generic a => Rep a x -> a
G.to (Rep t Any -> t) -> (Rec ρ -> Rep t Any) -> Rec ρ -> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec ρ -> Rep t Any
forall k (a :: k -> *) (ρ :: Row *) (x :: k).
ToNativeGeneralG a ρ =>
Rec ρ -> a x
toNativeGeneral'


{--------------------------------------------------------------------
  Generic-lens compatibility
--------------------------------------------------------------------}

-- | Every field in a row-types based record has a 'HasField' instance.
instance {-# OVERLAPPING #-}
  ( KnownSymbol name
  , r' .! name ≈ b
  , r  .! name ≈ a
  , r' ~ Modify name b r
  , r  ~ Modify name a r')
  => HasField name (Rec r) (Rec r') a b where
  field :: (a -> f b) -> Rec r -> f (Rec r')
field = Label name -> (a -> f b) -> Rec r -> f (Rec r')
forall (l :: Symbol) (r' :: Row *) b (r :: Row *) a (f :: * -> *).
(KnownSymbol l, (r' .! l) ≈ b, (r .! l) ≈ a, r' ~ Modify l b r,
 r ~ Modify l a r', Functor f) =>
Label l -> (a -> f b) -> Rec r -> f (Rec r')
focus (Label name
forall (s :: Symbol). Label s
Label @name)
  {-# INLINE field #-}

instance {-# OVERLAPPING #-}
  ( KnownSymbol name
  , r .! name ≈ a
  , r ~ Modify name a r)
  => HasField' name (Rec r) a where
  field' :: (a -> f a) -> Rec r -> f (Rec r)
field' = Label name -> (a -> f a) -> Rec r -> f (Rec r)
forall (l :: Symbol) (r' :: Row *) b (r :: Row *) a (f :: * -> *).
(KnownSymbol l, (r' .! l) ≈ b, (r .! l) ≈ a, r' ~ Modify l b r,
 r ~ Modify l a r', Functor f) =>
Label l -> (a -> f b) -> Rec r -> f (Rec r')
focus (Label name
forall (s :: Symbol). Label s
Label @name)
  {-# INLINE field' #-}