Modulerow-types-1.0.1.2Haskell2010

Data.Row.Internal

This module implements the internals of open records and variants.

Contents

Rows
Row Operations
Row Constraints
Helper functions

Synopsis

newtype Row
data Label
class KnownSymbol
data LT
type Empty
data HideType
family Extend
family Modify
family Rename
type .==
family .!
family .-
family .\\
family .+
family .\/
family .//
class Lacks
family .\
class HasType
class Forall
class BiForall
class BiConstraint
class Unconstrained
class Unconstrained1
class Unconstrained2
class FrontExtends
data FrontExtendsDict
type WellBehaved
family AllUniqueLabels
family Ap
family ApSingle
family Zip
family Map
family Subset
type Disjoint
family Labels
value labels
value labels'
value show'
value toKey
type ≈

Packagerow-types-1.0.1.2
Exports41
LanguageHaskell2010
LicenceMIT
SourceInternal.hs

Rows

newtypenewtype Row a

Source#

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.

Constructors

R [LT a]
A row is a list of symbol-to-type pairs that should always be sorted lexically by the symbol. The constructor is exported here (because this is an internal module) but should not be exported elsewhere.

datadata Label (s :: Symbol)

Source#

A label

Label

Instances3IsLabel, Eq, Show

x ≈ y => IsLabel x (Label y)Defined in row-types-1.0.1.2 · Data.Row.Internal
Eq (Label s)Defined in row-types-1.0.1.2 · Data.Row.Internal
KnownSymbol s => Show (Label s)Defined in row-types-1.0.1.2 · Data.Row.Internal

classclass KnownSymbol (n :: Symbol) where

Source#

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

datadata LT a

Source#

The kind of elements of rows. Each element is a label and its associated type.

Constructors

Symbol :-> a

Instances16BiForall, Forall, GenericRec, GenericVar, RepRec, RepVar, …

BiForall ('R '[]) ('R '[]) c1Defined in row-types-1.0.1.2 · Data.Row.Internal
(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)) ('R ((ℓ ':-> τ2) ': ρ2)) cDefined in row-types-1.0.1.2 · Data.Row.Internal
Forall ('R '[]) cDefined in row-types-1.0.1.2 · Data.Row.Internal
(KnownSymbol ℓ, c τ, Forall ('R ρ) c, FrontExtends ℓ τ ('R ρ), AllUniqueLabels (Extend ℓ τ ('R ρ))) => Forall ('R ((ℓ ':-> τ) ': ρ)) cDefined in row-types-1.0.1.2 · Data.Row.Internal
GenericRec EmptyDefined in row-types-1.0.1.2 · Data.Row.Records
GenericVar EmptyDefined in row-types-1.0.1.2 · Data.Row.Variants
KnownSymbol name => GenericRec ('R '[name ':-> t])Defined in row-types-1.0.1.2 · Data.Row.Records
(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'))Defined in row-types-1.0.1.2 · Data.Row.Records
KnownSymbol name => GenericVar ('R '[name ':-> t])Defined in row-types-1.0.1.2 · Data.Row.Variants
(GenericVar ('R ((name' ':-> t') ': r')), KnownSymbol name, Extend name t ('R ((name' ':-> t') ': r')) ≈ 'R ((name ':-> t) ': (name' ':-> t') ': r'), AllUniqueLabels ('R ((name ':-> t) ': (name' ':-> t') ': r'))) => GenericVar ('R ((name ':-> t) ': (name' ':-> t') ': r'))Defined in row-types-1.0.1.2 · Data.Row.Variants
type RepRec ('R '[name ':-> t]) = S1 ('MetaSel ('Just name) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)Defined in row-types-1.0.1.2 · Data.Row.Records
type RepRec ('R '[]) = U1Defined in row-types-1.0.1.2 · Data.Row.Records
type RepRec ('R ((name ':-> t) ': (name' ':-> t') ': r')) = S1 ('MetaSel ('Just name) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t) :*: RepRec ('R ((name' ':-> t') ': r'))Defined in row-types-1.0.1.2 · Data.Row.Records
type RepVar Empty = V1Defined in row-types-1.0.1.2 · Data.Row.Variants
type RepVar ('R '[name ':-> t]) = C1 ('MetaCons name 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t))Defined in row-types-1.0.1.2 · Data.Row.Variants
type RepVar ('R ((name ':-> t) ': (name' ':-> t') ': r')) = C1 ('MetaCons name 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: RepVar ('R ((name' ':-> t') ': r'))Defined in row-types-1.0.1.2 · Data.Row.Variants

typetype Empty = 'R '[]

Source#

Type level version of empty

datadata HideType where

Source#

Elements stored in a Row type are usually hidden.

Constructors

HideType :: a -> HideType

Row Operations

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

Source#

Type level Row extension

Equations

Extend l a2 ('R '[]) = 'R '[l ':-> a2]
Extend l a2 ('R x) = 'R (Inject (l ':-> a2) x)

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

Source#

Type level Row modification

Equations

Modify l a2 ('R ρ) = 'R (ModifyR l a2 ρ)

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

Source#

Type level row renaming

Equations

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

typetype (.==) (l :: Symbol) (a :: k) = Extend l a Empty

Source#

A type level way to create a singleton Row.

familytype family (.!) (r :: Row k) (t :: Symbol) :: k where

Source#

Type level label fetching

Equations

(.!) ('R r) l = Get l r

familytype family (.-) (r :: Row k) (s :: Symbol) :: Row k where

Source#

Type level Row element removal

Equations

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

familytype family (.\\) (l :: Row k) (r :: Row k) :: Row k where

Source#

Type level Row difference. That is, l .\\ r is the row remaining after removing any matching elements of r from l.

Equations

(.\\) ('R l) ('R r) = 'R (Diff l r)

Various row-type merges

The difference between .+ (read "append"), .\/ (read "min-join"), and .\\ (read "const-union") comes down to how duplicates are handled. In .+, the two given row-types must be entirely unique. Even the same entry in both row-types is forbidden. In .\/, this final restriction is relaxed, allowing two row-types that have no conflicts to be merged in the logical way. The .\\ operator is the most liberal, allowing any two row-types to be merged together, and whenever there is a conflict, favoring the left argument.

As examples of use:

.+ is used when appending two records, assuring that those two records are entirely disjoint.
.\/ is used when diversifying a variant, allowing some extension to the row-type so long as no original types have changed.
.// is used when doing record overwrite, allowing data in a record to totally overwrite what was previously there.

familytype family (.+) (l :: Row k) (r :: Row k) :: Row k where

Source#

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)

familytype family (.\/) (l :: Row k) (r :: Row k) :: Row k where

Source#

The minimum join of the two rows.

Equations

(.\/) x ('R '[]) = x
(.\/) ('R '[]) y = y
(.\/) ('R l) ('R r) = 'R (MinJoinR l r)

familytype family (.//) (l :: Row k) (r :: Row k) :: Row k where

Source#

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)

Row Constraints

classclass Lacks (l :: Symbol) (r :: Row Type)

Source#

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

Instances1Lacks

r .\ l => Lacks l rDefined in row-types-1.0.1.2 · Data.Row.Internal

familytype family (.\) (r :: Row k) (l :: Symbol) :: Constraint where

Source#

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

Equations

(.\) ('R '[]) l = Unconstrained
(.\) ('R r) l = LacksR l r r

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

Source#

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

Instances1HasType

(r .! l) ≈ a => HasType l a rDefined in row-types-1.0.1.2 · Data.Row.Internal

classclass Forall (r :: Row k) (c :: k -> Constraint) where

Source#

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

Methods

metamorph :: 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
A metamorphism is an anamorphism (an unfold) followed by a catamorphism (a fold). The parameter p describes the output of the unfold and the input of the fold. For records, p = (,), because every entry in the row will unfold to a value paired with the rest of the record. For variants, p = Either, because there will either be a value or future types to explore. Const can be useful when the types in the row are unnecessary.

Instances2Forall

Forall ('R '[]) cDefined in row-types-1.0.1.2 · Data.Row.Internal
(KnownSymbol ℓ, c τ, Forall ('R ρ) c, FrontExtends ℓ τ ('R ρ), AllUniqueLabels (Extend ℓ τ ('R ρ))) => Forall ('R ((ℓ ':-> τ) ': ρ)) cDefined in row-types-1.0.1.2 · Data.Row.Internal

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

Source#

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.

Methods

biMetamorph :: 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
A metamorphism is an anamorphism (an unfold) followed by a catamorphism (a fold).

Instances2BiForall

BiForall ('R '[]) ('R '[]) c1Defined in row-types-1.0.1.2 · Data.Row.Internal
(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)) ('R ((ℓ ':-> τ2) ': ρ2)) cDefined in row-types-1.0.1.2 · Data.Row.Internal

classclass (c1 x, c2 y) => BiConstraint (c1 :: k -> Constraint) (c2 :: k1 -> Constraint) (x :: k) (y :: k1)

Source#

A pair of constraints

Instances1BiConstraint

(c1 x, c2 y) => BiConstraint c1 c2 x yDefined in row-types-1.0.1.2 · Data.Row.Internal

classclass Unconstrained

Source#

A null constraint

Instances1Unconstrained

UnconstrainedDefined in row-types-1.0.1.2 · Data.Row.Internal

classclass Unconstrained1 (a :: k)

Source#

A null constraint of one argument

Instances1Unconstrained1

Unconstrained1 aDefined in row-types-1.0.1.2 · Data.Row.Internal

classclass Unconstrained2 (a :: k) (b :: k1)

Source#

A null constraint of two arguments

Instances1Unconstrained2

Unconstrained2 a bDefined in row-types-1.0.1.2 · Data.Row.Internal

classclass FrontExtends (l :: Symbol) (t :: k) (r :: Row k) where

Source#

A class wrapper for FrontExtendsDict.

Methods

frontExtendsDict :: FrontExtendsDict l t r

Instances1FrontExtends

(r ~ 'R ρ, 'R ((l ':-> t) ': ρ) ≈ Extend l t ('R ρ), AllUniqueLabelsR ((l ':-> t) ': ρ)) => FrontExtends l t rDefined in row-types-1.0.1.2 · Data.Row.Internal

datadata FrontExtendsDict (l :: Symbol) (t :: k) (r :: Row k)

Source#

A dictionary of information that proves that extending a row-type r with a label l will necessarily put it to the front of the underlying row-type list. This is quite internal and should not generally be necessary.

Constructors

forall ρ. FrontExtendsDict (Dict (r ~ 'R ρ, 'R ((l ':-> t) ': ρ) ≈ Extend l t ('R ρ), AllUniqueLabelsR ((l ':-> t) ': ρ)))

typetype WellBehaved (ρ :: Row k) = (Forall ρ Unconstrained1, AllUniqueLabels ρ)

Source#

A convenient way to provide common, easy constraints

familytype family AllUniqueLabels (r :: Row k) :: Constraint where

Source#

Are all of the labels in this Row unique?

Equations

AllUniqueLabels ('R r) = AllUniqueLabelsR r

familytype family Ap (fs :: Row (a -> b)) (r :: Row a) :: Row b where

Source#

Take two rows with the same labels, and apply the type operator from the first row to the type of the second.

Equations

Ap ('R fs) ('R r) = 'R (ApR fs r)

familytype family ApSingle (fs :: Row (a -> b)) (x :: a) :: Row b where

Source#

Take a row of type operators and apply each to the second argument.

Equations

ApSingle ('R fs) x = 'R (ApSingleR fs x)

familytype family Zip (r1 :: Row Type) (r2 :: Row Type) :: Row Type where

Source#

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)

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

Source#

Map a type level function over a Row.

Equations

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

familytype family Subset (r1 :: Row k) (r2 :: Row k) :: Constraint where

Source#

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)

type

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