Data.Row.Records

This module implements extensible records using closed type famillies.

See Examples.hs 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

(≈) Symbol x y => IsLabel x (Label y)

Methods

fromLabel :: Label y

KnownSymbol s => Show (Label s)

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: 4.7.0.0

Minimal complete definition

symbolSing

type family AllUniqueLabels (r :: Row *) :: 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

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

Methods

minBound :: Rec r

maxBound :: Rec r

Forall r Eq => Eq (Rec r)

Methods

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

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

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

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)

Methods

showsPrec :: Int -> Rec r -> ShowS

show :: Rec r -> String

showList :: [Rec r] -> ShowS

Forall r NFData => NFData (Rec r)

Methods

rnf :: 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 :: *) = 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 that is produced by 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 :: *) (r :: Row *) :: Row * where ...

Type level Row extension

Equations

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

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

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

Equations

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

Restriction

type family (r :: Row *) .- (s :: Symbol) :: Row * 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.

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

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

split :: forall s r. (Forall s Unconstrained1, Subset s r) => 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 :: (Functor f, KnownSymbol l) => Label l -> ((r .! l) -> f a) -> Rec r -> f (Rec (Modify l a 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 :: *) (r :: Row *) :: Row * 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 *) :: Row * 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 r

type family (r :: Row *) .! (t :: Symbol) :: * 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 *) .+ (r :: Row *) :: Row * where ... infixl 6

Type level Row append

Equations

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

(.+) :: 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.

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

A function to map over a record given no constraint.

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

A version of transform for when there is no constraint.

Fold

class Forall (r :: Row *) (c :: * -> 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, metamorph'

Instances

(KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ, Forall (R * ρ) c) => Forall (R * ((:) (LT *) ((:->) * ℓ τ) ρ)) c

Methods

metamorph :: Proxy (* -> *) h -> (f (Empty *) -> g (Empty *)) -> (forall (a :: Symbol) b (d :: [LT *]). (KnownSymbol a, c b) => Label a -> f (R * ((LT * ': (* :-> a) b) d)) -> (h b, f (R * d))) -> (forall (a :: Symbol) b (d :: [LT *]). (KnownSymbol a, c b, FoldStep a b d) => Label a -> h b -> g (R * d) -> g (R * ((LT * ': (* :-> a) b) d))) -> f (R * ((LT * ': (* :-> ℓ) τ) ρ)) -> g (R * ((LT * ': (* :-> ℓ) τ) ρ))

metamorph' :: Proxy (* -> *) h -> (f (Empty *) -> g (Empty *)) -> (forall (a :: Symbol) b (d :: [LT *]). (KnownSymbol a, c b) => Label a -> f (R * ((LT * ': (* :-> a) b) d)) -> Either (h b) (f (R * d))) -> (forall (a :: Symbol) b (d :: [LT *]). (KnownSymbol a, c b, FoldStep a b d) => Label a -> Either (h b) (g (R * d)) -> g (R * ((LT * ': (* :-> a) b) d))) -> f (R * ((LT * ': (* :-> ℓ) τ) ρ)) -> g (R * ((LT * ': (* :-> ℓ) τ) ρ))

Forall (R * ([] (LT *))) c

Methods

metamorph :: Proxy (* -> *) h -> (f (Empty *) -> g (Empty *)) -> (forall (ℓ :: Symbol) τ (ρ :: [LT *]). (KnownSymbol ℓ, c τ) => Label ℓ -> f (R * ((LT * ': (* :-> ℓ) τ) ρ)) -> (h τ, f (R * ρ))) -> (forall (ℓ :: Symbol) τ (ρ :: [LT *]). (KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ) => Label ℓ -> h τ -> g (R * ρ) -> g (R * ((LT * ': (* :-> ℓ) τ) ρ))) -> f (R * [LT *]) -> g (R * [LT *])

metamorph' :: Proxy (* -> *) h -> (f (Empty *) -> g (Empty *)) -> (forall (ℓ :: Symbol) τ (ρ :: [LT *]). (KnownSymbol ℓ, c τ) => Label ℓ -> f (R * ((LT * ': (* :-> ℓ) τ) ρ)) -> Either (h τ) (f (R * ρ))) -> (forall (ℓ :: Symbol) τ (ρ :: [LT *]). (KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ) => Label ℓ -> Either (h τ) (g (R * ρ)) -> g (R * ((LT * ': (* :-> ℓ) τ) ρ))) -> f (R * [LT *]) -> g (R * [LT *])

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. Forall2 r1 r2 Unconstrained1 => Rec r1 -> Rec r2 -> Rec (Zip r1 r2)

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

Sequence

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

Applicative sequencing over 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. Forall r Unconstrained1 => 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. Forall r Unconstrained1 => 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.

Labels

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

Return a list of the labels in a row type.

UNSAFE operations

unsafeRemove :: 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 should only be used when either: the record will never be merged with another record again, or a new value will soon be placed into the record at this label (as in, an update that is split over two commands).

If the resulting record is then merged (with .+) with another record that contains a value at that label, an "impossible" error will occur.

unsafeInjectFront :: KnownSymbol l => Label l -> a -> Rec (R r) -> Rec (R ((l :-> a) ': r))

A helper function for unsafely adding an element to the front of a record. This can cause the resulting record to be malformed, for instance, if the record already contains labels that are lexicographically before the given label. Realistically, this function should only be used when writing calls to metamorph.