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

Language | Haskell98 |

This module implements the internals of open records and variants.

- newtype Row a = R [LT a]
- data Label (s :: Symbol) = Label
- class KnownSymbol (n :: Symbol)
- data LT a = Symbol :-> a
- type Empty = R '[]
- data HideType where
- type family Extend (l :: Symbol) (a :: *) (r :: Row *) :: Row * where ...
- type family Modify (l :: Symbol) (a :: *) (r :: Row *) :: Row * where ...
- type family Rename (l :: Symbol) (l' :: Symbol) (r :: Row *) :: Row * where ...
- type family (r :: Row *) .\ (l :: Symbol) :: Constraint where ...
- type family (r :: Row *) .! (t :: Symbol) :: * where ...
- type family (r :: Row *) .- (s :: Symbol) :: Row * where ...
- type family (l :: Row *) .+ (r :: Row *) :: Row * where ...
- type family (l :: Row *) .\\ (r :: Row *) :: Row * where ...
- type (.==) (l :: Symbol) (a :: *) = Extend l a Empty
- class Lacks (l :: Symbol) (r :: Row *)
- class (r .! l) ≈ a => HasType l a r
- type family Labels (r :: Row a) where ...
- labels :: forall ρ c s. (IsString s, Forall ρ c) => [s]
- class Forall (r :: Row *) (c :: * -> Constraint) where
- class Forall2 (r1 :: Row *) (r2 :: Row *) (c :: * -> Constraint) where
- class Unconstrained1 a
- show' :: (IsString s, Show a) => a -> s
- toKey :: forall s. KnownSymbol s => Label s -> Text
- type (≈) a b = a ~ b
- type WellBehaved ρ = (Forall ρ Unconstrained1, AllUniqueLabels ρ)
- type family AllUniqueLabels (r :: Row *) :: Constraint where ...
- type family Zip (r1 :: Row *) (r2 :: Row *) where ...
- type family Map (f :: a -> b) (r :: Row a) :: Row b where ...
- type family Subset (r1 :: Row *) (r2 :: Row *) :: Constraint where ...
- type Disjoint l r = (WellBehaved l, WellBehaved r, Subset l (l .+ r), Subset r (l .+ r), ((l .+ r) .\\ l) ≈ r, ((l .+ r) .\\ r) ≈ l)
- mapForall :: forall f c ρ. Forall ρ c :- Forall (Map f ρ) (IsA c f)
- uniqueMap :: forall f ρ. AllUniqueLabels ρ :- AllUniqueLabels (Map f ρ)
- class IsA c f a where
- data As c f a where

# Rows

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.

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

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

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

Forall (R * ([] (LT *))) c Source # | |

(KnownSymbol ℓ, c τ1, c τ2, Forall2 (R * ρ1) (R * ρ2) c) => Forall2 (R * ((:) (LT *) ((:->) * ℓ τ1) ρ1)) (R * ((:) (LT *) ((:->) * ℓ τ2) ρ2)) c Source # | |

Forall2 (R * ([] (LT *))) (R * ([] (LT *))) c Source # | |

(KnownSymbol l, Switch (R * v) (R * r) b) => Switch (R * ((:) (LT *) ((:->) * l a) v)) (R * ((:) (LT *) ((:->) * l (a -> b)) r)) b Source # | |

Switch (R * ([] (LT *))) (R * ([] (LT *))) x Source # | |

Elements stored in a Row type are usually hidden.

# Row Operations

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

Type level Row extension

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

Type level Row modification

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

Type level row renaming

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

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

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

Type level Row element removal

type family (l :: Row *) .\\ (r :: Row *) :: Row * where ... infixl 6 Source #

Type level Row difference. That is, `l .\\ r`

is the row remaining after
removing any matching elements of `r`

from `l`

.

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

A type level way to create a singleton Row.

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

Alias for `.\`

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

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.

# Row Classes

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

Return a list of the labels in a row type.

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

:: forall (f :: Row * -> *) (g :: Row * -> *) (h :: * -> *). Proxy h | |

-> (f Empty -> g Empty) | The way to transform the empty element |

-> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> f (R ((ℓ :-> τ) ': ρ)) -> (h τ, f (R ρ))) | The unfold |

-> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ) => Label ℓ -> h τ -> g (R ρ) -> g (R ((ℓ :-> τ) ': ρ))) | The fold |

-> f r | The input structure |

-> g r |

A metamorphism is an unfold followed by a fold. This one is for product-like row-types (e.g. Rec).

:: forall (f :: Row * -> *) (g :: Row * -> *) (h :: * -> *). Proxy h | |

-> (f Empty -> g Empty) | The way to transform the empty element |

-> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> f (R ((ℓ :-> τ) ': ρ)) -> Either (h τ) (f (R ρ))) | The unfold |

-> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ) => Label ℓ -> Either (h τ) (g (R ρ)) -> g (R ((ℓ :-> τ) ': ρ))) | The fold |

-> f r | The input structure |

-> g r |

A metamorphism is an unfold followed by a fold. This one is for sum-like row-types (e.g. Var).

class Forall2 (r1 :: Row *) (r2 :: Row *) (c :: * -> Constraint) where Source #

Any structure over two rows in which every element of both rows satisfies the given constraint can be metamorphized into another structure over both of the rows. TODO: Perhaps it should be over two constraints? But this hasn't seemed necessary in practice.

metamorph2 :: forall (f :: Row * -> *) (g :: Row * -> *) (h :: Row * -> Row * -> *) (f' :: * -> *) (g' :: * -> *). Proxy f' -> Proxy g' -> (f Empty -> g Empty -> h Empty Empty) -> (forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, c τ1, c τ2) => Label ℓ -> f (R ((ℓ :-> τ1) ': ρ1)) -> g (R ((ℓ :-> τ2) ': ρ2)) -> ((f' τ1, f (R ρ1)), (g' τ2, g (R ρ2)))) -> (forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, c τ1, c τ2) => Label ℓ -> f' τ1 -> g' τ2 -> h (R ρ1) (R ρ2) -> h (R ((ℓ :-> τ1) ': ρ1)) (R ((ℓ :-> τ2) ': ρ2))) -> f r1 -> g r2 -> h r1 r2 Source #

A metamorphism is a fold followed by an unfold. Here, we fold both of the inputs.

# Helper functions

toKey :: forall s. KnownSymbol s => Label s -> Text Source #

A helper function to turn a Label directly into `Text`

.

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

A convenient way to provide common, easy constraints

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

Are all of the labels in this Row unique?

AllUniqueLabels (R r) = AllUniqueLabelsR r |

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.

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

Map a type level function over a Row.

type family Subset (r1 :: Row *) (r2 :: Row *) :: Constraint where ... Source #

Is the first row a subset of the second?

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.

mapForall :: forall f c ρ. Forall ρ c :- Forall (Map f ρ) (IsA c f) Source #

This allows us to derive a `Forall (Map f r) ..` from a `Forall r ..`.

uniqueMap :: forall f ρ. AllUniqueLabels ρ :- AllUniqueLabels (Map f ρ) Source #

Map preserves uniqueness of labels.