Safe Haskell | None |
---|---|

Language | Haskell98 |

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.

- data Label (s :: Symbol) = Label
- class KnownSymbol (n :: Symbol)
- type family AllUniqueLabels (r :: Row *) :: Constraint where ...
- type WellBehaved ρ = (Forall ρ Unconstrained1, AllUniqueLabels ρ)
- data Rec (r :: Row *)
- data Row a
- type Empty = R '[]
- type (≈) a b = a ~ b
- empty :: Rec Empty
- type (.==) (l :: Symbol) (a :: *) = Extend l a Empty
- (.==) :: KnownSymbol l => Label l -> a -> Rec (l .== a)
- pattern (:==) :: forall l a. KnownSymbol l => Label l -> a -> Rec (l .== a)
- unSingleton :: forall l a. KnownSymbol l => Rec (l .== a) -> (Label l, a)
- default' :: forall c ρ. (Forall ρ c, AllUniqueLabels ρ) => (forall a. c a => a) -> Rec ρ
- defaultA :: forall c f ρ. (Applicative f, Forall ρ c, AllUniqueLabels ρ) => (forall a. c a => f a) -> f (Rec ρ)
- fromLabels :: forall c ρ. (Forall ρ c, AllUniqueLabels ρ) => (forall l a. (KnownSymbol l, c a) => Label l -> a) -> Rec ρ
- fromLabelsA :: forall c f ρ. (Applicative f, Forall ρ c, AllUniqueLabels ρ) => (forall l a. (KnownSymbol l, c a) => Label l -> f a) -> f (Rec ρ)
- 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 ρ))
- extend :: forall a l r. KnownSymbol l => Label l -> a -> Rec r -> Rec (Extend l a r)
- type family Extend (l :: Symbol) (a :: *) (r :: Row *) :: Row * where ...
- class Lacks (l :: Symbol) (r :: Row *)
- type family (r :: Row *) .\ (l :: Symbol) :: Constraint where ...
- type family (r :: Row *) .- (s :: Symbol) :: Row * where ...
- (.-) :: KnownSymbol l => Rec r -> Label l -> Rec (r .- l)
- restrict :: forall r r'. (Forall r Unconstrained1, Subset r r') => Rec r' -> Rec r
- split :: forall s r. (Forall s Unconstrained1, Subset s r) => Rec r -> (Rec s, Rec (r .\\ s))
- update :: (KnownSymbol l, (r .! l) ≈ a) => Label l -> a -> Rec r -> Rec r
- focus :: (Functor f, KnownSymbol l) => Label l -> ((r .! l) -> f a) -> Rec r -> f (Rec (Modify l a r))
- 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))
- type family Modify (l :: Symbol) (a :: *) (r :: Row *) :: Row * where ...
- rename :: (KnownSymbol l, KnownSymbol l') => Label l -> Label l' -> Rec r -> Rec (Rename l l' r)
- type family Rename (l :: Symbol) (l' :: Symbol) (r :: Row *) :: Row * where ...
- class (r .! l) ≈ a => HasType l a r
- type family (r :: Row *) .! (t :: Symbol) :: * where ...
- (.!) :: KnownSymbol l => Rec r -> Label l -> r .! l
- type family (l :: Row *) .+ (r :: Row *) :: Row * where ...
- (.+) :: Rec l -> Rec r -> Rec (l .+ r)
- type Disjoint l r = (WellBehaved l, WellBehaved r, Subset l (l .+ r), Subset r (l .+ r), ((l .+ r) .\\ l) ≈ r, ((l .+ r) .\\ r) ≈ l)
- pattern (:+) :: forall l r. Disjoint l r => Rec l -> Rec r -> Rec (l .+ r)
- type family Map (f :: a -> b) (r :: Row a) :: Row b where ...
- map :: forall c f r. Forall r c => (forall a. c a => a -> f a) -> Rec r -> Rec (Map f r)
- map' :: forall f r. Forall r Unconstrained1 => (forall a. a -> f a) -> Rec r -> Rec (Map f r)
- 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 r f g. Forall r Unconstrained1 => (forall a. f a -> g a) -> Rec (Map f r) -> Rec (Map g r)
- class Forall (r :: Row *) (c :: * -> Constraint)
- erase :: forall c ρ b. Forall ρ c => (forall a. c a => a -> b) -> Rec ρ -> [b]
- eraseWithLabels :: forall c ρ s b. (Forall ρ c, IsString s) => (forall a. c a => a -> b) -> Rec ρ -> [(s, b)]
- eraseZip :: forall c ρ b. Forall ρ c => (forall a. c a => a -> a -> b) -> Rec ρ -> Rec ρ -> [b]
- 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
- type family Zip (r1 :: Row *) (r2 :: Row *) where ...
- zip :: forall r1 r2. Forall2 r1 r2 Unconstrained1 => Rec r1 -> Rec r2 -> Rec (Zip r1 r2)
- sequence :: forall f r. (Forall r Unconstrained1, Applicative f) => Rec (Map f r) -> f (Rec r)
- compose :: forall (f :: * -> *) g r. Forall r Unconstrained1 => Rec (Map f (Map g r)) -> Rec (Map (Compose f g) r)
- uncompose :: forall (f :: * -> *) g r. Forall r Unconstrained1 => Rec (Map (Compose f g) r) -> Rec (Map f (Map g r))
- labels :: forall ρ c s. (IsString s, Forall ρ c) => [s]
- unsafeRemove :: KnownSymbol l => Label l -> Rec r -> Rec (r .- l)
- unsafeInjectFront :: KnownSymbol l => Label l -> a -> Rec (R r) -> Rec (R ((l :-> a) ': r))

# Types and constraints

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*

symbolSing

type family AllUniqueLabels (r :: Row *) :: Constraint where ... Source #

Are all of the labels in this Row unique?

AllUniqueLabels (R r) = AllUniqueLabelsR r |

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

A convenient way to provide common, easy constraints

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.

# Construction

type (.==) (l :: Symbol) (a :: *) = Extend l a Empty infix 7 Source #

A type level way to create a singleton Row.

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

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

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

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

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

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 ρ Source #

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

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

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

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 ... Source #

Type level Row extension

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

Alias for `.\`

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

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

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

## Restriction

type family (r :: Row *) .- (s :: Symbol) :: Row * where ... infixl 6 Source #

Type level Row element removal

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

Record restriction. Remove the label l from the record.

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

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

Split a record into two sub-records.

## Modification

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

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

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

Focus on a sub-record

type family Modify (l :: Symbol) (a :: *) (r :: Row *) :: Row * where ... Source #

Type level Row modification

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

Rename a label.

type family Rename (l :: Symbol) (l' :: Symbol) (r :: Row *) :: Row * where ... Source #

Type level row renaming

# Query

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

Alias for `(r .! l) ≈ a`

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

# Combine

## Disjoint union

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

A type synonym for disjointness.

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

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 ... Source #

Map a type level function over a Row.

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

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

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

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

A version of `transform`

for when there is no constraint.

## Fold

class Forall (r :: Row *) (c :: * -> Constraint) Source #

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

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

A standard fold

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

A fold with labels

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

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 Source #

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 ... Source #

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

zip :: forall r1 r2. Forall2 r1 r2 Unconstrained1 => Rec r1 -> Rec r2 -> Rec (Zip r1 r2) Source #

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

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

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

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] Source #

Return a list of the labels in a row type.

## UNSAFE operations

unsafeRemove :: KnownSymbol l => Label l -> Rec r -> Rec (r .- l) Source #

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

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`

.