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.

Types and constraints

data Label (s :: Symbol)

A label

Constructors

Label

Instances

x ≈ y => IsLabel x (Label y)

Defined in Data.Row.Internal

Methods

fromLabel :: Label y

Eq (Label s)

Defined in Data.Row.Internal

Methods

(==) :: Label s -> Label s -> Bool

(/=) :: Label s -> Label s -> Bool

KnownSymbol s => Show (Label s)

Defined in Data.Row.Internal

Methods

showsPrec :: Int -> Label s -> ShowS

show :: Label s -> String

showList :: [Label s] -> ShowS

class KnownSymbol (n :: Symbol)

This class gives the string associated with a type-level symbol. There are instances of the class for every concrete literal: "hello", etc.

Since: base-4.7.0.0

Minimal complete definition

symbolSing

type family AllUniqueLabels (r :: Row k) :: Constraint where ...

Are all of the labels in this Row unique?

Equations

AllUniqueLabels (R r) = AllUniqueLabelsR r

type WellBehaved ρ = (Forall ρ Unconstrained1, AllUniqueLabels ρ)

A convenient way to provide common, easy constraints

data Rec (r :: Row *)

A record with row r.

Instances

(KnownSymbol name, (r .! name) ≈ a, r ~ Modify name a r) => HasField' name (Rec r) a

Defined in Data.Row.Records

Methods

field' :: Lens (Rec r) (Rec r) a a

(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

Every field in a row-types based record has a HasField instance.

Defined in Data.Row.Records

Methods

field :: Lens (Rec r) (Rec r') a b

(Forall r Bounded, AllUniqueLabels r) => Bounded (Rec r)

Defined in Data.Row.Records

Methods

minBound :: Rec r

maxBound :: Rec r

Forall r Eq => Eq (Rec r)

Defined in Data.Row.Records

Methods

(==) :: Rec r -> Rec r -> Bool

(/=) :: Rec r -> Rec r -> Bool

(Forall r Eq, Forall r Ord) => Ord (Rec r)

Defined in Data.Row.Records

Methods

compare :: Rec r -> Rec r -> Ordering

(<) :: Rec r -> Rec r -> Bool

(<=) :: Rec r -> Rec r -> Bool

(>) :: Rec r -> Rec r -> Bool

(>=) :: Rec r -> Rec r -> Bool

max :: Rec r -> Rec r -> Rec r

min :: Rec r -> Rec r -> Rec r

Forall r Show => Show (Rec r)

Defined in Data.Row.Records

Methods

showsPrec :: Int -> Rec r -> ShowS

show :: Rec r -> String

showList :: [Rec r] -> ShowS

GenericRec r => Generic (Rec r)

Defined in Data.Row.Records

Associated Types

type Rep (Rec r) :: Type -> Type

Methods

from :: Rec r -> Rep (Rec r) x

to :: Rep (Rec r) x -> Rec r

Forall r NFData => NFData (Rec r)

Defined in Data.Row.Records

Methods

rnf :: Rec r -> ()

type Rep (Rec r)

Defined in Data.Row.Records

type Rep (Rec r)

data Row a

The kind of rows. This type is only used as a datakind. A row is a typelevel entity telling us which symbols are associated with which types.

type Empty = R '[]

Type level version of empty

type (≈) a b = a ~ b infix 4

A lower fixity operator for type equality

Construction

empty :: Rec Empty

The empty record

type (.==) (l :: Symbol) (a :: k) = Extend l a Empty infix 7

A type level way to create a singleton Row.

(.==) :: KnownSymbol l => Label l -> a -> Rec (l .== a) infix 7

The singleton record

pattern (:==) :: forall l a. KnownSymbol l => Label l -> a -> Rec (l .== a) infix 7

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.

unSingleton :: forall l a. KnownSymbol l => Rec (l .== a) -> (Label l, a)

Turns a singleton record into a pair of the label and value.

default' :: forall c ρ. (Forall ρ c, AllUniqueLabels ρ) => (forall a. c a => a) -> Rec ρ

Initialize a record with a default value at each label.

defaultA :: forall c f ρ. (Applicative f, Forall ρ c, AllUniqueLabels ρ) => (forall a. c a => f a) -> f (Rec ρ)

Initialize a record with a default value at each label; works over an Applicative.

fromLabels :: forall c ρ. (Forall ρ c, AllUniqueLabels ρ) => (forall l a. (KnownSymbol l, c a) => Label l -> a) -> Rec ρ

Initialize a record, where each value is determined by the given function over the label at that value.

fromLabelsA :: forall c f ρ. (Applicative f, Forall ρ c, AllUniqueLabels ρ) => (forall l a. (KnownSymbol l, c a) => Label l -> f a) -> f (Rec ρ)

Initialize a record, where each value is determined by the given function over the label at that value. This function works over an Applicative.

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

Initialize a record over a Map.

Extension

extend :: forall a l r. KnownSymbol l => Label l -> a -> Rec r -> Rec (Extend l a r)

Record extension. The row may already contain the label, in which case the origin value can be obtained after restriction (.-) with the label.

type family Extend (l :: Symbol) (a :: k) (r :: Row k) :: Row k where ...

Type level Row extension

Equations

Extend l a (R '[]) = R ((l :-> a) ': '[])

Extend l a (R x) = R (Inject (l :-> a) x)

class Lacks (l :: Symbol) (r :: Row *)

Alias for .\. It is a class rather than an alias, so that it can be partially applied.

Instances

r .\ l => Lacks l r

Defined in Data.Row.Internal

type family (r :: Row k) .\ (l :: Symbol) :: Constraint where ... infixl 4

Does the row lack (i.e. it does not have) the specified label?

Equations

(R '[]) .\ l = Unconstrained

(R r) .\ l = LacksR l r r

Restriction

type family (r :: Row k) .- (s :: Symbol) :: Row k where ... infixl 6

Type level Row element removal

Equations

(R r) .- l = R (Remove l r)

(.-) :: KnownSymbol l => Rec r -> Label l -> Rec (r .- l) infixl 6

Record restriction. Remove the label l from the record.

lazyRemove :: KnownSymbol l => Label l -> Rec r -> Rec (r .- l)

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.

type family Subset (r1 :: Row k) (r2 :: Row k) :: Constraint where ...

Is the first row a subset of the second? Or, does the second row contain every binding that the first one does?

Equations

Subset ('R '[]) r = Unconstrained

Subset ('R ((l :-> a) ': x)) r = ((r .! l) ≈ a, Subset ('R x) r)

restrict :: forall r r'. (FreeForall r, Subset r r') => Rec r' -> Rec r

Arbitrary record restriction. Turn a record into a subset of itself.

split :: forall s r. (Subset s r, FreeForall s) => Rec r -> (Rec s, Rec (r .\\ s))

Split a record into two sub-records.

Modification

update :: (KnownSymbol l, (r .! l) ≈ a) => Label l -> a -> Rec r -> Rec r

Update 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 on the value associated with the label.

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

Focus on a sub-record

type family Modify (l :: Symbol) (a :: k) (r :: Row k) :: Row k where ...

Type level Row modification

Equations

Modify l a (R ρ) = R (ModifyR l a ρ)

rename :: (KnownSymbol l, KnownSymbol l') => Label l -> Label l' -> Rec r -> Rec (Rename l l' r)

Rename a label.

type family Rename (l :: Symbol) (l' :: Symbol) (r :: Row k) :: Row k where ...

Type level row renaming

Equations

Rename l l' r = Extend l' (r .! l) (r .- l)

Query

class (r .! l) ≈ a => HasType l a r

Alias for (r .! l) ≈ a. It is a class rather than an alias, so that it can be partially applied.

Instances

(r .! l) ≈ a => HasType l (a :: k) (r :: Row k)

Defined in Data.Row.Internal

type family (r :: Row k) .! (t :: Symbol) :: k where ... infixl 5

Type level label fetching

Equations

(R r) .! l = Get l r

(.!) :: KnownSymbol l => Rec r -> Label l -> r .! l

Record selection

Combine

Disjoint union

type family (l :: Row k) .+ (r :: Row k) :: Row k where ... infixl 6

Type level Row append

Equations

x .+ (R '[]) = x

(R '[]) .+ y = y

x .+ (R '[l :-> a]) = Extend l a x

(R '[l :-> a]) .+ y = Extend l a y

(R l) .+ (R r) = R (Merge l r)

(.+) :: forall l r. FreeForall l => Rec l -> Rec r -> Rec (l .+ r) infixl 6

Record disjoint union (commutative)

type Disjoint l r = (WellBehaved l, WellBehaved r, Subset l (l .+ r), Subset r (l .+ r), ((l .+ r) .\\ l) ≈ r, ((l .+ r) .\\ r) ≈ l)

A type synonym for disjointness.

pattern (:+) :: forall l r. Disjoint l r => Rec l -> Rec r -> Rec (l .+ r) infixl 6

A pattern version of record union, for use in pattern matching.

Overwrite

type family (l :: Row k) .// (r :: Row k) where ... infixl 6

The overwriting union, where the left row overwrites the types of the right row where the labels overlap.

Equations

x .// (R '[]) = x

(R '[]) .// y = y

(R l) .// (R r) = R (ConstUnionR l r)

(.//) :: Rec r -> Rec r' -> Rec (r .// r') infixl 6

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

Application with functions

curryRec :: forall l t r x. KnownSymbol l => Label l -> (Rec ((l .== t) .+ r) -> x) -> t -> Rec r -> x

Kind of like curry for functions over records.

(.$) :: (KnownSymbol l, (r' .! l) ≈ t) => (Rec ((l .== t) .+ r) -> x) -> (Label l, Rec r') -> Rec r -> x 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!"

Native Conversion

The toNative and fromNative functions allow one to convert between Recs 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" }

fromNative :: FromNative t => t -> Rec (NativeRow t)

Convert a Haskell record to a row-types Rec.

toNative :: ToNative t => Rec (NativeRow t) -> t

Convert a record to an exactly matching native Haskell type.

toNativeGeneral :: ToNativeGeneral t ρ => Rec ρ -> t

Convert a record to a native Haskell type.

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

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

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

type family NativeRow t where ...

Equations

NativeRow t = NativeRowG (Rep t)

Dynamic Conversion

toDynamicMap :: Forall r Typeable => Rec r -> HashMap Text Dynamic

Converts a Rec into a HashMap of Dynamics.

fromDynamicMap :: (AllUniqueLabels r, Forall r Typeable) => HashMap Text Dynamic -> Maybe (Rec r)

Produces a Rec from a HashMap of Dynamics.

Row operations

Map

type family Map (f :: a -> b) (r :: Row a) :: Row b where ...

Map a type level function over a Row.

Equations

Map f (R r) = R (MapR f r)

map :: forall c f r. Forall r c => (forall a. c a => a -> f a) -> Rec r -> Rec (Map f r)

A function to map over a record given a constraint.

map' :: forall f r. FreeForall r => (forall a. a -> f a) -> Rec r -> Rec (Map f r)

A function to map over a record given no constraint.

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

A function to map over a Ap record given constraints.

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)

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 r f g. FreeForall r => (forall a. f a -> g a) -> Rec (Map f r) -> Rec (Map g r)

A version of transform for when there is no constraint.

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)

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

A version of zipTransform for when there is no constraint.

Fold

class BiForall (r1 :: Row k1) (r2 :: Row k2) (c :: k1 -> k2 -> Constraint)

Any structure over two rows in which the elements of each row satisfy some constraints can be metamorphized into another structure over both of the rows.

Minimal complete definition

biMetamorph

Instances

(KnownSymbol ℓ, c τ1 τ2, BiForall ('R ρ1) ('R ρ2) c, FrontExtends ℓ τ1 ('R ρ1), FrontExtends ℓ τ2 ('R ρ2), AllUniqueLabels (Extend ℓ τ1 ('R ρ1)), AllUniqueLabels (Extend ℓ τ2 ('R ρ2))) => BiForall ('R ((ℓ :-> τ1) ': ρ1) :: Row k1) ('R ((ℓ :-> τ2) ': ρ2) :: Row k2) (c :: k1 -> k2 -> Constraint)

Defined in Data.Row.Internal

Methods

biMetamorph :: forall p f g h. Bifunctor p => Proxy (Proxy h, Proxy p) -> (f Empty Empty -> g Empty Empty) -> (forall (ℓ0 :: Symbol) (τ10 :: k10) (τ20 :: k20) (ρ10 :: Row k10) (ρ20 :: Row k20). (KnownSymbol ℓ0, c τ10 τ20, HasType ℓ0 τ10 ρ10, HasType ℓ0 τ20 ρ20) => Label ℓ0 -> f ρ10 ρ20 -> p (f (ρ10 .- ℓ0) (ρ20 .- ℓ0)) (h τ10 τ20)) -> (forall (ℓ1 :: Symbol) (τ11 :: k10) (τ21 :: k20) (ρ11 :: Row k10) (ρ21 :: Row k20). (KnownSymbol ℓ1, c τ11 τ21, FrontExtends ℓ1 τ11 ρ11, FrontExtends ℓ1 τ21 ρ21, AllUniqueLabels (Extend ℓ1 τ11 ρ11), AllUniqueLabels (Extend ℓ1 τ21 ρ21)) => Label ℓ1 -> p (g ρ11 ρ21) (h τ11 τ21) -> g (Extend ℓ1 τ11 ρ11) (Extend ℓ1 τ21 ρ21)) -> f ('R ((ℓ :-> τ1) ': ρ1)) ('R ((ℓ :-> τ2) ': ρ2)) -> g ('R ((ℓ :-> τ1) ': ρ1)) ('R ((ℓ :-> τ2) ': ρ2))

BiForall ('R ('[] :: [LT k1]) :: Row k1) ('R ('[] :: [LT k2]) :: Row k2) (c1 :: k1 -> k2 -> Constraint)

Defined in Data.Row.Internal

Methods

biMetamorph :: forall p f g h. Bifunctor p => Proxy (Proxy h, Proxy p) -> (f Empty Empty -> g Empty Empty) -> (forall (ℓ :: Symbol) (τ1 :: k10) (τ2 :: k20) (ρ1 :: Row k10) (ρ2 :: Row k20). (KnownSymbol ℓ, c1 τ1 τ2, HasType ℓ τ1 ρ1, HasType ℓ τ2 ρ2) => Label ℓ -> f ρ1 ρ2 -> p (f (ρ1 .- ℓ) (ρ2 .- ℓ)) (h τ1 τ2)) -> (forall (ℓ :: Symbol) (τ1 :: k10) (τ2 :: k20) (ρ1 :: Row k10) (ρ2 :: Row k20). (KnownSymbol ℓ, c1 τ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 ('R '[]) ('R '[]) -> g ('R '[]) ('R '[])

class Forall (r :: Row k) (c :: k -> Constraint)

Any structure over a row in which every element is similarly constrained can be metamorphized into another structure over the same row.

Minimal complete definition

metamorph

Instances

(KnownSymbol ℓ, c τ, Forall ('R ρ) c, FrontExtends ℓ τ ('R ρ), AllUniqueLabels (Extend ℓ τ ('R ρ))) => Forall ('R ((ℓ :-> τ) ': ρ) :: Row k) (c :: k -> Constraint)

Defined in Data.Row.Internal

Methods

metamorph :: forall p f g h. Bifunctor p => Proxy (Proxy h, Proxy p) -> (f Empty -> g Empty) -> (forall (ℓ0 :: Symbol) (τ0 :: k0) (ρ0 :: Row k0). (KnownSymbol ℓ0, c τ0, HasType ℓ0 τ0 ρ0) => Label ℓ0 -> f ρ0 -> p (f (ρ0 .- ℓ0)) (h τ0)) -> (forall (ℓ1 :: Symbol) (τ1 :: k0) (ρ1 :: Row k0). (KnownSymbol ℓ1, c τ1, FrontExtends ℓ1 τ1 ρ1, AllUniqueLabels (Extend ℓ1 τ1 ρ1)) => Label ℓ1 -> p (g ρ1) (h τ1) -> g (Extend ℓ1 τ1 ρ1)) -> f ('R ((ℓ :-> τ) ': ρ)) -> g ('R ((ℓ :-> τ) ': ρ))

Forall ('R ('[] :: [LT k]) :: Row k) (c :: k -> Constraint)

Defined in Data.Row.Internal

Methods

metamorph :: forall p f g h. Bifunctor p => Proxy (Proxy h, Proxy p) -> (f Empty -> g Empty) -> (forall (ℓ :: Symbol) (τ :: k0) (ρ :: Row k0). (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) => Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ)) -> (forall (ℓ :: Symbol) (τ :: k0) (ρ :: Row k0). (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ, AllUniqueLabels (Extend ℓ τ ρ)) => Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ)) -> f ('R '[]) -> g ('R '[])

erase :: forall c ρ b. Forall ρ c => (forall a. c a => a -> b) -> Rec ρ -> [b]

A standard fold

eraseWithLabels :: forall c ρ s b. (Forall ρ c, IsString s) => (forall a. c a => a -> b) -> Rec ρ -> [(s, b)]

A fold with labels

eraseZip :: forall c ρ b. Forall ρ c => (forall a. c a => a -> a -> b) -> Rec ρ -> Rec ρ -> [b]

A fold over two row type structures at once

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

Turns a record into a HashMap from values representing the labels to the values of the record.

Zip

type family Zip (r1 :: Row *) (r2 :: Row *) where ...

Zips two rows together to create a Row of the pairs. The two rows must have the same set of labels.

Equations

Zip (R r1) (R r2) = R (ZipR r1 r2)

zip :: forall r1 r2. FreeBiForall r1 r2 => Rec r1 -> Rec r2 -> Rec (Zip r1 r2)

Zips together two records that have the same set of labels.

Applicative-like functions

traverse :: forall c f r. (Forall r c, Applicative f) => (forall a. c a => a -> f a) -> Rec r -> f (Rec r)

Traverse a function over a 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))

Traverse a function over a Mapped record. Note that the fields of the record will be accessed in lexicographic order by the labels.

sequence :: forall f r. (Applicative f, FreeForall r) => Rec (Map f r) -> f (Rec r)

Applicative sequencing over a record.

sequence' :: forall f r c. (Forall r c, Applicative f) => Rec (Map f r) -> f (Rec r)

A version of sequence in which the constraint for Forall can be chosen.

distribute :: forall f r. (FreeForall r, Functor f) => f (Rec r) -> Rec (Map f r)

This function acts as the inversion of sequence, allowing one to move a functor level into a record.

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

compose :: forall f g r. FreeForall r => Rec (Map f (Map g r)) -> Rec (Map (Compose f g) r)

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.

uncompose :: forall f g r. FreeForall r => Rec (Map (Compose f g) r) -> Rec (Map f (Map g r))

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.

compose' :: forall c f g r. Forall r c => Rec (Map f (Map g r)) -> Rec (Map (Compose f g) r)

A version of compose 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))

A version of uncompose in which the constraint for Forall can be chosen.

Labels

labels :: forall ρ c s. (IsString s, Forall ρ c) => [s]

Return a list of the labels in a row type.

labels' :: forall ρ s. (IsString s, Forall ρ Unconstrained1) => [s]

Return a list of the labels in a row type and is specialized to the Unconstrained1 constraint.

Coerce

coerceRec :: forall r1 r2. BiForall r1 r2 Coercible => Rec r1 -> Rec r2

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