-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Open Records and Variants -- -- This package uses closed type families and type literals to implement -- open records and variants. The core is based off of the CTRex -- package, but it also includes polymorphic variants and a number of -- additional functions. That said, it is not a proper superset of CTRex -- as it specifically forbids records from having more than one element -- of the same label. @package row-types @version 1.0.1.2 -- | This module implements the internals of open records and variants. module Data.Row.Internal -- | 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. newtype Row 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. R :: [LT a] -> Row a -- | A label data Label (s :: Symbol) Label :: Label (s :: Symbol) -- | This class gives the string associated with a type-level symbol. There -- are instances of the class for every concrete literal: "hello", etc. class KnownSymbol (n :: Symbol) -- | The kind of elements of rows. Each element is a label and its -- associated type. data LT a (:->) :: Symbol -> a -> LT a -- | Type level version of empty type Empty = R '[] -- | Elements stored in a Row type are usually hidden. data HideType [HideType] :: a -> HideType -- | Type level Row extension type family Extend (l :: Symbol) (a :: k) (r :: Row k) :: Row k -- | Type level Row modification type family Modify (l :: Symbol) (a :: k) (r :: Row k) :: Row k -- | Type level row renaming type family Rename (l :: Symbol) (l' :: Symbol) (r :: Row k) :: Row k -- | A type level way to create a singleton Row. type (l :: Symbol) .== (a :: k) = Extend l a Empty infix 7 .== -- | Type level label fetching type family (r :: Row k) .! (t :: Symbol) :: k infixl 5 .! -- | Type level Row element removal type family (r :: Row k) .- (s :: Symbol) :: Row k infixl 6 .- -- | Type level Row difference. That is, l .\\ r is the row -- remaining after removing any matching elements of r from -- l. type family (l :: Row k) .\\ (r :: Row k) :: Row k infixl 6 .\\ -- | Type level Row append type family (l :: Row k) .+ (r :: Row k) :: Row k infixl 6 .+ -- | The minimum join of the two rows. type family (l :: Row k) .\/ (r :: Row k) infixl 6 .\/ -- | The overwriting union, where the left row overwrites the types of the -- right row where the labels overlap. type family (l :: Row k) .// (r :: Row k) infixl 6 .// -- | Alias for .\. It is a class rather than an alias, so that it -- can be partially applied. class Lacks (l :: Symbol) (r :: Row *) -- | Does the row lack (i.e. it does not have) the specified label? type family (r :: Row k) .\ (l :: Symbol) :: Constraint infixl 4 .\ -- | Alias for (r .! l) ≈ a. It is a class rather than an alias, -- so that it can be partially applied. class (r .! l ≈ a) => HasType l a r -- | Any structure over a row in which every element is similarly -- constrained can be metamorphized into another structure over the same -- row. class Forall (r :: Row k) (c :: k -> Constraint) -- | 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. metamorph :: forall (p :: * -> * -> *) (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *). (Forall r c, Bifunctor p) => Proxy (Proxy h, Proxy p) -> (f Empty -> g Empty) -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) => Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ)) -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ, AllUniqueLabels (Extend ℓ τ ρ)) => Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ)) -> f r -> g r -- | 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. class BiForall (r1 :: Row k1) (r2 :: Row k2) (c :: k1 -> k2 -> Constraint) -- | A metamorphism is an anamorphism (an unfold) followed by a -- catamorphism (a fold). biMetamorph :: forall (p :: * -> * -> *) (f :: Row k1 -> Row k2 -> *) (g :: Row k1 -> Row k2 -> *) (h :: k1 -> k2 -> *). (BiForall r1 r2 c, Bifunctor p) => Proxy (Proxy h, Proxy p) -> (f Empty Empty -> g Empty Empty) -> (forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, c τ1 τ2, HasType ℓ τ1 ρ1, HasType ℓ τ2 ρ2) => Label ℓ -> f ρ1 ρ2 -> p (f (ρ1 .- ℓ) (ρ2 .- ℓ)) (h τ1 τ2)) -> (forall ℓ τ1 τ2 ρ1 ρ2. (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 pair of constraints class (c1 x, c2 y) => BiConstraint c1 c2 x y -- | A null constraint class Unconstrained -- | A null constraint of one argument class Unconstrained1 a -- | A null constraint of two arguments class Unconstrained2 a b -- | A class wrapper for FrontExtendsDict. class FrontExtends l t r frontExtendsDict :: FrontExtends l t r => FrontExtendsDict l t r -- | 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. data FrontExtendsDict l t r FrontExtendsDict :: Dict (r ~ R ρ, R ((l :-> t) : ρ) ≈ Extend l t (R ρ), AllUniqueLabelsR ((l :-> t) : ρ)) -> FrontExtendsDict l t r -- | A convenient way to provide common, easy constraints type WellBehaved ρ = (Forall ρ Unconstrained1, AllUniqueLabels ρ) -- | Are all of the labels in this Row unique? type family AllUniqueLabels (r :: Row k) :: Constraint -- | Take two rows with the same labels, and apply the type operator from -- the first row to the type of the second. type family Ap (fs :: Row (a -> b)) (r :: Row a) :: Row b -- | Take a row of type operators and apply each to the second argument. type family ApSingle (fs :: Row (a -> b)) (x :: a) :: Row b -- | Zips two rows together to create a Row of the pairs. The two rows must -- have the same set of labels. type family Zip (r1 :: Row *) (r2 :: Row *) -- | Map a type level function over a Row. type family Map (f :: a -> b) (r :: Row a) :: Row b -- | Is the first row a subset of the second? Or, does the second row -- contain every binding that the first one does? type family Subset (r1 :: Row k) (r2 :: Row k) :: Constraint -- | A type synonym for disjointness. type Disjoint l r = (WellBehaved l, WellBehaved r, Subset l (l .+ r), Subset r (l .+ r), l .+ r .\\ l ≈ r, l .+ r .\\ r ≈ l) -- | The labels in a Row. type family Labels (r :: Row a) -- | Return a list of the labels in a row type. labels :: forall ρ c s. (IsString s, Forall ρ c) => [s] -- | Return a list of the labels in a row type and is specialized to the -- Unconstrained1 constraint. labels' :: forall ρ s. (IsString s, Forall ρ Unconstrained1) => [s] -- | A helper function for showing labels show' :: (IsString s, Show a) => a -> s -- | A helper function to turn a Label directly into Text. toKey :: forall s. KnownSymbol s => Label s -> Text -- | A lower fixity operator for type equality type a ≈ b = a ~ b infix 4 ≈ instance GHC.Classes.Eq (Data.Row.Internal.Label s) instance forall k (c :: k -> GHC.Types.Constraint). Data.Row.Internal.Forall ('Data.Row.Internal.R '[]) c instance forall (ℓ :: GHC.Types.Symbol) k (c :: k -> GHC.Types.Constraint) (τ :: k) (ρ :: [Data.Row.Internal.LT k]). (GHC.TypeLits.KnownSymbol ℓ, c τ, Data.Row.Internal.Forall ('Data.Row.Internal.R ρ) c, Data.Row.Internal.FrontExtends ℓ τ ('Data.Row.Internal.R ρ), Data.Row.Internal.AllUniqueLabels (Data.Row.Internal.Extend ℓ τ ('Data.Row.Internal.R ρ))) => Data.Row.Internal.Forall ('Data.Row.Internal.R ((ℓ 'Data.Row.Internal.:-> τ) : ρ)) c instance forall k1 k2 (c1 :: k1 -> k2 -> GHC.Types.Constraint). Data.Row.Internal.BiForall ('Data.Row.Internal.R '[]) ('Data.Row.Internal.R '[]) c1 instance forall k1 k2 (ℓ :: GHC.Types.Symbol) (c :: k1 -> k2 -> GHC.Types.Constraint) (τ1 :: k1) (τ2 :: k2) (ρ1 :: [Data.Row.Internal.LT k1]) (ρ2 :: [Data.Row.Internal.LT k2]). (GHC.TypeLits.KnownSymbol ℓ, c τ1 τ2, Data.Row.Internal.BiForall ('Data.Row.Internal.R ρ1) ('Data.Row.Internal.R ρ2) c, Data.Row.Internal.FrontExtends ℓ τ1 ('Data.Row.Internal.R ρ1), Data.Row.Internal.FrontExtends ℓ τ2 ('Data.Row.Internal.R ρ2), Data.Row.Internal.AllUniqueLabels (Data.Row.Internal.Extend ℓ τ1 ('Data.Row.Internal.R ρ1)), Data.Row.Internal.AllUniqueLabels (Data.Row.Internal.Extend ℓ τ2 ('Data.Row.Internal.R ρ2))) => Data.Row.Internal.BiForall ('Data.Row.Internal.R ((ℓ 'Data.Row.Internal.:-> τ1) : ρ1)) ('Data.Row.Internal.R ((ℓ 'Data.Row.Internal.:-> τ2) : ρ2)) c instance forall k (r :: Data.Row.Internal.Row k) (l :: GHC.Types.Symbol) (a :: k). ((r Data.Row.Internal..! l) Data.Row.Internal.≈ a) => Data.Row.Internal.HasType l a r instance forall k (r :: Data.Row.Internal.Row k) (ρ :: [Data.Row.Internal.LT k]) (l :: GHC.Types.Symbol) (t :: k). (r GHC.Types.~ 'Data.Row.Internal.R ρ, 'Data.Row.Internal.R ((l 'Data.Row.Internal.:-> t) : ρ) Data.Row.Internal.≈ Data.Row.Internal.Extend l t ('Data.Row.Internal.R ρ), Data.Row.Internal.AllUniqueLabelsR ((l 'Data.Row.Internal.:-> t) : ρ)) => Data.Row.Internal.FrontExtends l t r instance (x Data.Row.Internal.≈ y) => GHC.OverloadedLabels.IsLabel x (Data.Row.Internal.Label y) instance (r Data.Row.Internal..\ l) => Data.Row.Internal.Lacks l r instance forall k1 k2 (c1 :: k1 -> GHC.Types.Constraint) (x :: k1) (c2 :: k2 -> GHC.Types.Constraint) (y :: k2). (c1 x, c2 y) => Data.Row.Internal.BiConstraint c1 c2 x y instance forall k1 k2 (a :: k1) (b :: k2). Data.Row.Internal.Unconstrained2 a b instance forall k (a :: k). Data.Row.Internal.Unconstrained1 a instance Data.Row.Internal.Unconstrained instance GHC.TypeLits.KnownSymbol s => GHC.Show.Show (Data.Row.Internal.Label s) -- | This module exports various dictionaries that help the type-checker -- when dealing with row-types. -- -- For the various axioms, type variables are consistently in the -- following order: -- -- module Data.Row.Dictionaries -- | Map preserves uniqueness of labels. uniqueMap :: forall f r. Dict (AllUniqueLabels (Map f r) ≈ AllUniqueLabels r) -- | Ap preserves uniqueness of labels. uniqueAp :: forall fs r. Dict (AllUniqueLabels (Ap fs r) ≈ AllUniqueLabels r) -- | ApSingle preserves uniqueness of labels. uniqueApSingle :: forall x r. Dict (AllUniqueLabels (ApSingle r x) ≈ AllUniqueLabels r) -- | Zip preserves uniqueness of labels. uniqueZip :: forall r1 r2. Dict (AllUniqueLabels (Zip r1 r2) ≈ (AllUniqueLabels r1, AllUniqueLabels r2)) -- | If we know that r has been extended with l .== t, -- then we know that this extension at the label l must be -- t. extendHas :: forall l t r. Dict ((Extend l t r .! l) ≈ t) -- | This allows us to derive Map f r .! l ≈ f t from r .! l ≈ -- t mapHas :: forall f l t r. ((r .! l) ≈ t) :- ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l)) -- | This allows us to derive Ap ϕ ρ .! l ≈ f t from ϕ .! l ≈ -- f and ρ .! l ≈ t apHas :: forall l f ϕ t ρ. ((ϕ .! l) ≈ f, (ρ .! l) ≈ t) :- ((Ap ϕ ρ .! l) ≈ f t, (Ap ϕ ρ .- l) ≈ Ap (ϕ .- l) (ρ .- l)) -- | This allows us to derive ApSingle r x .! l ≈ f x from r -- .! l ≈ f apSingleHas :: forall x l f r. ((r .! l) ≈ f) :- ((ApSingle r x .! l) ≈ f x, (ApSingle r x .- l) ≈ ApSingle (r .- l) x) -- | Proof that the Map type family preserves labels and their -- ordering. mapExtendSwap :: forall f ℓ τ r. Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r)) -- | Proof that the Ap type family preserves labels and their -- ordering. apExtendSwap :: forall ℓ f fs τ r. Dict (Extend ℓ (f τ) (Ap fs r) ≈ Ap (Extend ℓ f fs) (Extend ℓ τ r)) -- | Proof that the ApSingle type family preserves labels and their -- ordering. apSingleExtendSwap :: forall τ ℓ f r. Dict (Extend ℓ (f τ) (ApSingle r τ) ≈ ApSingle (Extend ℓ f r) τ) -- | Proof that the Ap type family preserves labels and their -- ordering. zipExtendSwap :: forall ℓ τ1 r1 τ2 r2. Dict (Extend ℓ (τ1, τ2) (Zip r1 r2) ≈ Zip (Extend ℓ τ1 r1) (Extend ℓ τ2 r2)) -- | Map distributes over MinJoin mapMinJoin :: forall f r r'. Dict ((Map f r .\/ Map f r') ≈ Map f (r .\/ r')) -- | ApSingle distributes over MinJoin apSingleMinJoin :: forall r r' x. Dict ((ApSingle r x .\/ ApSingle r' x) ≈ ApSingle (r .\/ r') x) -- | FreeForall can be used when a Forall constraint is -- necessary but there is no particular constraint we care about. type FreeForall r = Forall r Unconstrained1 -- | FreeForall can be used when a BiForall constraint is -- necessary but there is no particular constraint we care about. type FreeBiForall r1 r2 = BiForall r1 r2 Unconstrained2 -- | Allow any Forall over a row-type, be usable for -- Unconstrained1. freeForall :: forall r c. Forall r c :- Forall r Unconstrained1 -- | This allows us to derive a Forall (Map f r) .. from a -- Forall r ... mapForall :: forall f ρ c. Forall ρ c :- Forall (Map f ρ) (IsA c f) -- | This allows us to derive a Forall (ApSingle f r) .. from a -- Forall f ... apSingleForall :: forall a fs c. Forall fs c :- Forall (ApSingle fs a) (ActsOn c a) -- | Two rows are subsets of a third if and only if their disjoint union is -- a subset of that third. subsetJoin :: forall r1 r2 s. Dict ((Subset r1 s, Subset r2 s) ≈ Subset (r1 .+ r2) s) -- | If two rows are each subsets of a third, their join is a subset of the -- third subsetJoin' :: forall r1 r2 s. Dict ((Subset r1 s, Subset r2 s) ≈ Subset (r1 .// r2) s) -- | If a row is a subset of another, then its restriction is also a subset -- of the other subsetRestrict :: forall r s l. Subset r s :- Subset (r .- l) s -- | Subset is transitive subsetTrans :: forall r1 r2 r3. (Subset r1 r2, Subset r2 r3) :- Subset r1 r3 -- | Map distributes over Difference mapDifference :: forall f r r'. Dict ((Map f r .\\ Map f r') ≈ Map f (r .\\ r')) -- | ApSingle distributes over Difference apSingleDifference :: forall r r' x. Dict ((ApSingle r x .\\ ApSingle r' x) ≈ ApSingle (r .\\ r') x) -- | A class to capture the idea of As so that it can be partially -- applied in a context. class IsA c f a as :: IsA c f a => As c f a -- | This data type is used to for its ability to existentially bind a type -- variable. Particularly, it says that for the type a, there -- exists a t such that a ~ f t and c t holds. data As c f a [As] :: forall c f a t. (a ~ f t, c t) => As c f a -- | A class to capture the idea of As' so that it can be partially -- applied in a context. class ActsOn c t a actsOn :: ActsOn c t a => As' c t a -- | Like As, but here we know the underlying value is some -- f applied to the given type a. data As' c t a [As'] :: forall c f a t. (a ~ f t, c f) => As' c t a -- | Values of type Dict p capture a dictionary for a -- constraint of type p. -- -- e.g. -- --
--   Dict :: Dict (Eq Int)
--   
-- -- captures a dictionary that proves we have an: -- --
--   instance Eq Int
--   
-- -- Pattern matching on the Dict constructor will bring this -- instance into scope. data Dict a [Dict] :: forall a. a => Dict a -- | This is the type of entailment. -- -- a :- b is read as a "entails" b. -- -- With this we can actually build a category for Constraint -- resolution. -- -- e.g. -- -- Because Eq a is a superclass of Ord a, -- we can show that Ord a entails Eq a. -- -- Because instance Ord a => Ord [a] exists, we -- can show that Ord a entails Ord [a] as -- well. -- -- This relationship is captured in the :- entailment type here. -- -- Since p :- p and entailment composes, :- forms -- the arrows of a Category of constraints. However, -- Category only became sufficiently general to support this -- instance in GHC 7.8, so prior to 7.8 this instance is unavailable. -- -- But due to the coherence of instance resolution in Haskell, this -- Category has some very interesting properties. Notably, in the -- absence of IncoherentInstances, this category is "thin", -- which is to say that between any two objects (constraints) there is at -- most one distinguishable arrow. -- -- This means that for instance, even though there are two ways to derive -- Ord a :- Eq [a], the answers from these -- two paths _must_ by construction be equal. This is a property that -- Haskell offers that is pretty much unique in the space of languages -- with things they call "type classes". -- -- What are the two ways? -- -- Well, we can go from Ord a :- Eq a via -- the superclass relationship, and then from Eq a :- -- Eq [a] via the instance, or we can go from Ord -- a :- Ord [a] via the instance then from -- Ord [a] :- Eq [a] through the superclass -- relationship and this diagram by definition must "commute". -- -- Diagrammatically, -- --
--          Ord a
--      ins /     \ cls
--         v       v
--   Ord [a]     Eq a
--      cls \     / ins
--           v   v
--          Eq [a]
--   
-- -- This safety net ensures that pretty much anything you can write with -- this library is sensible and can't break any assumptions on the behalf -- of library authors. newtype a :- b Sub :: (a => Dict b) -> (:-) a b infixr 9 :- -- | Witnesses that a value of type e contains evidence of the -- constraint c. -- -- Mainly intended to allow (\\) to be overloaded, since it's a -- useful operator. class HasDict c e | e -> c evidence :: HasDict c e => e -> Dict c -- | Operator version of withDict, with the arguments flipped (\\) :: HasDict c e => (c => r) -> e -> r infixl 1 \\ -- | From a Dict, takes a value in an environment where the instance -- witnessed by the Dict is in scope, and evaluates it. -- -- Essentially a deconstruction of a Dict into its -- continuation-style form. -- -- Can also be used to deconstruct an entailment, a :- b, -- using a context a. -- --
--   withDict :: Dict c -> (c => r) -> r
--   withDict :: a => (a :- c) -> (c => r) -> r
--   
withDict :: HasDict c e => e -> (c => r) -> r -- | A null constraint class Unconstrained -- | A null constraint of one argument class Unconstrained1 a -- | A null constraint of two arguments class Unconstrained2 a b instance forall k1 k2 (c :: (k1 -> k2) -> GHC.Types.Constraint) (f :: k1 -> k2) (t :: k1). c f => Data.Row.Dictionaries.ActsOn c t (f t) instance forall k1 k2 (c :: k1 -> GHC.Types.Constraint) (a :: k1) (f :: k1 -> k2). c a => Data.Row.Dictionaries.IsA c f (f a) -- | 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. module Data.Row.Records -- | A label data Label (s :: Symbol) Label :: Label (s :: Symbol) -- | This class gives the string associated with a type-level symbol. There -- are instances of the class for every concrete literal: "hello", etc. class KnownSymbol (n :: Symbol) -- | Are all of the labels in this Row unique? type family AllUniqueLabels (r :: Row k) :: Constraint -- | A convenient way to provide common, easy constraints type WellBehaved ρ = (Forall ρ Unconstrained1, AllUniqueLabels ρ) -- | A record with row r. data Rec (r :: Row *) -- | 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. data Row a -- | Type level version of empty type Empty = R '[] -- | A lower fixity operator for type equality type a ≈ b = a ~ b infix 4 ≈ -- | The empty record empty :: Rec Empty -- | A type level way to create a singleton Row. type (l :: Symbol) .== (a :: k) = Extend l a Empty infix 7 .== -- | The singleton record (.==) :: 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. pattern (:==) :: forall l a. KnownSymbol l => Label l -> a -> Rec (l .== a) infix 7 :== -- | Turns a singleton record into a pair of the label and value. unSingleton :: forall l a. KnownSymbol l => Rec (l .== a) -> (Label l, a) -- | Initialize a record with a default value at each label. default' :: forall c ρ. (Forall ρ c, AllUniqueLabels ρ) => (forall a. c a => a) -> Rec ρ -- | Initialize a record with a default value at each label; works over an -- Applicative. defaultA :: forall c f ρ. (Applicative f, Forall ρ c, AllUniqueLabels ρ) => (forall a. c a => f a) -> f (Rec ρ) -- | Initialize a record, where each value is determined by the given -- function over the label at that value. 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. This function works over an -- Applicative. 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 over a Map. 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 ρ)) -- | Record extension. The row may already contain the label, in which case -- the origin value can be obtained after restriction (.-) with -- the label. extend :: forall a l r. KnownSymbol l => Label l -> a -> Rec r -> Rec (Extend l a r) -- | Type level Row extension type family Extend (l :: Symbol) (a :: k) (r :: Row k) :: Row k -- | Alias for .\. It is a class rather than an alias, so that it -- can be partially applied. class Lacks (l :: Symbol) (r :: Row *) -- | Does the row lack (i.e. it does not have) the specified label? type family (r :: Row k) .\ (l :: Symbol) :: Constraint infixl 4 .\ -- | Type level Row element removal type family (r :: Row k) .- (s :: Symbol) :: Row k infixl 6 .- -- | Record restriction. Remove the label l from the record. (.-) :: KnownSymbol l => Rec r -> Label l -> Rec (r .- l) infixl 6 .- -- | 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. --
  3. It will keep the reference to the value alive, meaning that it -- will not get garbage collected.
  4. --
-- -- 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. lazyRemove :: KnownSymbol l => Label l -> Rec r -> Rec (r .- l) -- | Is the first row a subset of the second? Or, does the second row -- contain every binding that the first one does? type family Subset (r1 :: Row k) (r2 :: Row k) :: Constraint -- | Arbitrary record restriction. Turn a record into a subset of itself. restrict :: forall r r'. (FreeForall r, Subset r r') => Rec r' -> Rec r -- | Split a record into two sub-records. split :: forall s r. (Subset s r, FreeForall s) => Rec r -> (Rec s, Rec (r .\\ s)) -- | Update the value associated with the label. update :: (KnownSymbol l, (r .! l) ≈ a) => Label l -> a -> Rec r -> Rec r -- | Focus on 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 a sub-record 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 level Row modification type family Modify (l :: Symbol) (a :: k) (r :: Row k) :: Row k -- | Rename a label. rename :: (KnownSymbol l, KnownSymbol l') => Label l -> Label l' -> Rec r -> Rec (Rename l l' r) -- | Type level row renaming type family Rename (l :: Symbol) (l' :: Symbol) (r :: Row k) :: Row k -- | Alias for (r .! l) ≈ a. It is a class rather than an alias, -- so that it can be partially applied. class (r .! l ≈ a) => HasType l a r -- | Type level label fetching type family (r :: Row k) .! (t :: Symbol) :: k infixl 5 .! -- | Record selection (.!) :: KnownSymbol l => Rec r -> Label l -> r .! l -- | Type level Row append type family (l :: Row k) .+ (r :: Row k) :: Row k infixl 6 .+ -- | Record disjoint union (commutative) (.+) :: forall l r. FreeForall l => Rec l -> Rec r -> Rec (l .+ r) infixl 6 .+ -- | A type synonym for disjointness. 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 pattern version of record union, for use in pattern matching. pattern (:+) :: forall l r. Disjoint l r => Rec l -> Rec r -> Rec (l .+ r) infixl 6 :+ -- | The overwriting union, where the left row overwrites the types of the -- right row where the labels overlap. type family (l :: Row k) .// (r :: Row k) infixl 6 .// -- | Record overwrite. -- -- The operation r .// r' creates a new record such that: -- -- -- -- This can be thought of as r "overwriting" r'. (.//) :: Rec r -> Rec r' -> Rec (r .// r') infixl 6 .// -- | Kind of like curry for functions over records. curryRec :: forall l t r x. KnownSymbol l => Label l -> (Rec ((l .== t) .+ r) -> x) -> t -> Rec r -> x -- | 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!"
--   
(.$) :: (KnownSymbol l, (r' .! l) ≈ t) => (Rec ((l .== t) .+ r) -> x) -> (Label l, Rec r') -> Rec r -> x infixl 2 .$ -- | Convert a Haskell record to a row-types Rec. fromNative :: FromNative t => t -> Rec (NativeRow t) -- | Convert a record to an exactly matching native Haskell type. toNative :: ToNative t => Rec (NativeRow t) -> t -- | Convert a record to a native Haskell type. toNativeGeneral :: ToNativeGeneral t ρ => Rec ρ -> t 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 -- | Converts a Rec into a HashMap of Dynamics. toDynamicMap :: Forall r Typeable => Rec r -> HashMap Text Dynamic -- | Produces a Rec from a HashMap of Dynamics. fromDynamicMap :: (AllUniqueLabels r, Forall r Typeable) => HashMap Text Dynamic -> Maybe (Rec r) -- | Map a type level function over a Row. type family Map (f :: a -> b) (r :: Row a) :: Row b -- | A function to map over a record given a constraint. 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 no constraint. map' :: forall f r. FreeForall r => (forall a. a -> f a) -> Rec r -> Rec (Map f r) -- | A function to map over a Ap record given constraints. 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 ρ)) -- | 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 c r f g. Forall r c => (forall a. c a => f a -> g a) -> Rec (Map f r) -> Rec (Map g r) -- | A version of transform for when there is no constraint. transform' :: forall r f g. FreeForall r => (forall a. f a -> g a) -> Rec (Map f r) -> Rec (Map g 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 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) -- | A version of zipTransform for when there is no constraint. 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) -- | 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. class BiForall (r1 :: Row k1) (r2 :: Row k2) (c :: k1 -> k2 -> Constraint) -- | Any structure over a row in which every element is similarly -- constrained can be metamorphized into another structure over the same -- row. class Forall (r :: Row k) (c :: k -> Constraint) -- | A standard fold erase :: forall c ρ b. Forall ρ c => (forall a. c a => a -> b) -> Rec ρ -> [b] -- | A fold with labels eraseWithLabels :: forall c ρ s b. (Forall ρ c, IsString s) => (forall a. c a => a -> b) -> Rec ρ -> [(s, b)] -- | A fold over two row type structures at once eraseZip :: forall c ρ b. Forall ρ c => (forall a. c a => a -> a -> b) -> Rec ρ -> Rec ρ -> [b] -- | Turns a record into a HashMap from values representing the -- labels to the values of the record. 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 -- | Zips two rows together to create a Row of the pairs. The two rows must -- have the same set of labels. type family Zip (r1 :: Row *) (r2 :: Row *) -- | Zips together two records that have the same set of labels. zip :: forall r1 r2. FreeBiForall r1 r2 => Rec r1 -> Rec r2 -> Rec (Zip r1 r2) -- | Traverse a function over a record. Note that the fields of the record -- will be accessed in lexicographic order by the labels. 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 Mapped 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)) -- | Applicative sequencing over a record. sequence :: forall f r. (Applicative f, FreeForall r) => Rec (Map f r) -> f (Rec r) -- | A version of sequence in which the constraint for Forall -- can be chosen. sequence' :: forall f r c. (Forall r c, Applicative f) => Rec (Map f r) -> f (Rec r) -- | This function acts as the inversion of sequence, allowing one -- to move a functor level into a record. distribute :: forall f r. (FreeForall r, Functor f) => f (Rec r) -> Rec (Map f 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. compose :: forall f g r. FreeForall r => Rec (Map f (Map g r)) -> Rec (Map (Compose f 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. uncompose :: forall f g r. FreeForall r => Rec (Map (Compose f g) r) -> Rec (Map f (Map g r)) -- | A version of compose in which the constraint for Forall -- can be chosen. compose' :: forall c f g r. Forall r c => Rec (Map f (Map g r)) -> Rec (Map (Compose f g) r) -- | A version of uncompose 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)) -- | Return a list of the labels in a row type. labels :: forall ρ c s. (IsString s, Forall ρ c) => [s] -- | Return a list of the labels in a row type and is specialized to the -- Unconstrained1 constraint. labels' :: forall ρ s. (IsString s, Forall ρ Unconstrained1) => [s] -- | 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
--   
coerceRec :: forall r1 r2. BiForall r1 r2 Coercible => Rec r1 -> Rec r2 instance forall k (cs :: k -> *) (ρ :: Data.Row.Internal.Row *) (m :: GHC.Generics.Meta). Data.Row.Records.ToNativeGeneralG cs ρ => Data.Row.Records.ToNativeGeneralG (GHC.Generics.D1 m cs) ρ instance forall k (cs :: k -> *) (ρ :: Data.Row.Internal.Row *) (m :: GHC.Generics.Meta). Data.Row.Records.ToNativeGeneralG cs ρ => Data.Row.Records.ToNativeGeneralG (GHC.Generics.C1 m cs) ρ instance Data.Row.Records.ToNativeGeneralG GHC.Generics.U1 ρ instance (GHC.TypeLits.KnownSymbol name, (ρ Data.Row.Internal..! name) Data.Row.Internal.≈ t) => Data.Row.Records.ToNativeGeneralG (GHC.Generics.S1 ('GHC.Generics.MetaSel ('GHC.Maybe.Just name) p s l) (GHC.Generics.Rec0 t)) ρ instance forall k (l :: k -> *) (ρ :: Data.Row.Internal.Row *) (r :: k -> *). (Data.Row.Records.ToNativeGeneralG l ρ, Data.Row.Records.ToNativeGeneralG r ρ) => Data.Row.Records.ToNativeGeneralG (l GHC.Generics.:*: r) ρ instance forall k (cs :: k -> *) (m :: GHC.Generics.Meta). Data.Row.Records.ToNativeG cs => Data.Row.Records.ToNativeG (GHC.Generics.D1 m cs) instance forall k (cs :: k -> *) (m :: GHC.Generics.Meta). Data.Row.Records.ToNativeG cs => Data.Row.Records.ToNativeG (GHC.Generics.C1 m cs) instance Data.Row.Records.ToNativeG GHC.Generics.U1 instance GHC.TypeLits.KnownSymbol name => Data.Row.Records.ToNativeG (GHC.Generics.S1 ('GHC.Generics.MetaSel ('GHC.Maybe.Just name) p s l) (GHC.Generics.Rec0 t)) instance forall k (l :: k -> *) (r :: k -> *). (Data.Row.Records.ToNativeG l, Data.Row.Records.ToNativeG r, Data.Row.Internal.Disjoint (Data.Row.Records.NativeRowG l) (Data.Row.Records.NativeRowG r)) => Data.Row.Records.ToNativeG (l GHC.Generics.:*: r) instance forall k (cs :: k -> *) (m :: GHC.Generics.Meta). Data.Row.Records.FromNativeG cs => Data.Row.Records.FromNativeG (GHC.Generics.D1 m cs) instance forall k (cs :: k -> *) (m :: GHC.Generics.Meta). Data.Row.Records.FromNativeG cs => Data.Row.Records.FromNativeG (GHC.Generics.C1 m cs) instance Data.Row.Records.FromNativeG GHC.Generics.U1 instance GHC.TypeLits.KnownSymbol name => Data.Row.Records.FromNativeG (GHC.Generics.S1 ('GHC.Generics.MetaSel ('GHC.Maybe.Just name) p s l) (GHC.Generics.Rec0 t)) instance forall k (l :: k -> *) (r :: k -> *). (Data.Row.Records.FromNativeG l, Data.Row.Records.FromNativeG r, Data.Row.Dictionaries.FreeForall (Data.Row.Records.NativeRowG l)) => Data.Row.Records.FromNativeG (l GHC.Generics.:*: r) instance Data.Row.Records.GenericRec r => GHC.Generics.Generic (Data.Row.Records.Rec r) instance Data.Row.Records.GenericRec Data.Row.Internal.Empty instance GHC.TypeLits.KnownSymbol name => Data.Row.Records.GenericRec ('Data.Row.Internal.R '[ name 'Data.Row.Internal.:-> t]) instance (r GHC.Types.~ ((name' 'Data.Row.Internal.:-> t') : r'), Data.Row.Records.GenericRec ('Data.Row.Internal.R r), GHC.TypeLits.KnownSymbol name, Data.Row.Internal.Extend name t ('Data.Row.Internal.R r) Data.Row.Internal.≈ 'Data.Row.Internal.R ((name 'Data.Row.Internal.:-> t) : r)) => Data.Row.Records.GenericRec ('Data.Row.Internal.R ((name 'Data.Row.Internal.:-> t) : (name' 'Data.Row.Internal.:-> t') : r')) instance Data.Row.Internal.Forall r GHC.Show.Show => GHC.Show.Show (Data.Row.Records.Rec r) instance Data.Row.Internal.Forall r GHC.Classes.Eq => GHC.Classes.Eq (Data.Row.Records.Rec r) instance (Data.Row.Internal.Forall r GHC.Classes.Eq, Data.Row.Internal.Forall r GHC.Classes.Ord) => GHC.Classes.Ord (Data.Row.Records.Rec r) instance (Data.Row.Internal.Forall r GHC.Enum.Bounded, Data.Row.Internal.AllUniqueLabels r) => GHC.Enum.Bounded (Data.Row.Records.Rec r) instance Data.Row.Internal.Forall r Control.DeepSeq.NFData => Control.DeepSeq.NFData (Data.Row.Records.Rec r) instance (GHC.TypeLits.KnownSymbol name, (r' Data.Row.Internal..! name) Data.Row.Internal.≈ b, (r Data.Row.Internal..! name) Data.Row.Internal.≈ a, r' GHC.Types.~ Data.Row.Internal.Modify name b r, r GHC.Types.~ Data.Row.Internal.Modify name a r') => Data.Generics.Product.Fields.HasField name (Data.Row.Records.Rec r) (Data.Row.Records.Rec r') a b instance (GHC.TypeLits.KnownSymbol name, (r Data.Row.Internal..! name) Data.Row.Internal.≈ a, r GHC.Types.~ Data.Row.Internal.Modify name a r) => Data.Generics.Product.Fields.HasField' name (Data.Row.Records.Rec r) a -- | This module implements extensible variants using closed type families. module Data.Row.Variants -- | A label data Label (s :: Symbol) Label :: Label (s :: Symbol) -- | This class gives the string associated with a type-level symbol. There -- are instances of the class for every concrete literal: "hello", etc. class KnownSymbol (n :: Symbol) -- | Are all of the labels in this Row unique? type family AllUniqueLabels (r :: Row k) :: Constraint -- | A convenient way to provide common, easy constraints type WellBehaved ρ = (Forall ρ Unconstrained1, AllUniqueLabels ρ) -- | The variant type. data Var (r :: Row *) -- | 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. data Row a -- | Type level version of empty type Empty = R '[] -- | A lower fixity operator for type equality type a ≈ b = a ~ b infix 4 ≈ -- | Alias for (r .! l) ≈ a. It is a class rather than an alias, -- so that it can be partially applied. class (r .! l ≈ a) => HasType l a r -- | A pattern for variants; can be used to both destruct a variant when in -- a pattern position or construct one in an expression position. pattern IsJust :: forall l r. (AllUniqueLabels r, KnownSymbol l) => Label l -> (r .! l) -> Var r -- | A quick constructor to create a singleton variant. singleton :: KnownSymbol l => Label l -> a -> Var (l .== a) -- | A quick destructor for singleton variants. unSingleton :: forall l a. KnownSymbol l => Var (l .== a) -> (Label l, a) -- | Initialize a variant from a producer function that accepts labels. If -- this function returns more than one possibility, then one is chosen -- arbitrarily to be the value in the variant. fromLabels :: forall c ρ f. (Alternative f, Forall ρ c, AllUniqueLabels ρ) => (forall l a. (KnownSymbol l, c a) => Label l -> f a) -> f (Var ρ) -- | Initialize a variant over a Map. fromLabelsMap :: forall c f g ρ. (Alternative f, Forall ρ c, AllUniqueLabels ρ) => (forall l a. (KnownSymbol l, c a) => Label l -> f (g a)) -> f (Var (Map g ρ)) -- | Does the row lack (i.e. it does not have) the specified label? type family (r :: Row k) .\ (l :: Symbol) :: Constraint infixl 4 .\ -- | Alias for .\. It is a class rather than an alias, so that it -- can be partially applied. class Lacks (l :: Symbol) (r :: Row *) -- | The minimum join of the two rows. type family (l :: Row k) .\/ (r :: Row k) infixl 6 .\/ -- | Make the variant arbitrarily more diverse. diversify :: forall r' r. Var r -> Var (r .\/ r') -- | A weaker version of diversify, but it's helpful for -- metamorph as it explicitly uses Extend. extend :: forall a l r. KnownSymbol l => Label l -> Var r -> Var (Extend l a r) -- | Type level Row append type family (l :: Row k) .+ (r :: Row k) :: Row k infixl 6 .+ -- | If the variant exists at the given label, update it to the given -- value. Otherwise, do nothing. update :: (KnownSymbol l, (r .! l) ≈ a) => Label l -> a -> Var r -> Var r -- | If the variant exists at the given label, focus on the value -- associated with it. Otherwise, do nothing. focus :: forall l r r' a b p f. (AllUniqueLabels r, AllUniqueLabels r', KnownSymbol l, (r .! l) ≈ a, (r' .! l) ≈ b, r' ≈ ((r .- l) .\/ (l .== b)), Applicative f, Choice p) => Label l -> p a (f b) -> p (Var r) (f (Var r')) -- | Type level Row modification type family Modify (l :: Symbol) (a :: k) (r :: Row k) :: Row k -- | Rename the given label. rename :: (KnownSymbol l, KnownSymbol l') => Label l -> Label l' -> Var r -> Var (Rename l l' r) -- | Type level row renaming type family Rename (l :: Symbol) (l' :: Symbol) (r :: Row k) :: Row k -- | A Variant with no options is uninhabited. impossible :: Var Empty -> a -- | Convert a variant into either the value at the given label or a -- variant without that label. This is the basic variant destructor. trial :: KnownSymbol l => Var r -> Label l -> Either (Var (r .- l)) (r .! l) -- | A version of trial that ignores the leftover variant. trial' :: KnownSymbol l => Var r -> Label l -> Maybe (r .! l) -- | A trial over multiple types multiTrial :: forall x y. (AllUniqueLabels x, FreeForall x) => Var y -> Either (Var (y .\\ x)) (Var x) -- | A convenient function for using view patterns when dispatching -- variants. For example: -- --
--   myShow :: Var ("y" '::= String :| "x" '::= Int :| Empty) -> String
--   myShow (view x -> Just n) = "Int of "++show n
--   myShow (view y -> Just s) = "String of "++s
--   
view :: KnownSymbol l => Label l -> Var r -> Maybe (r .! l) -- | Is the first row a subset of the second? Or, does the second row -- contain every binding that the first one does? type family Subset (r1 :: Row k) (r2 :: Row k) :: Constraint -- | Arbitrary variant restriction. Turn a variant into a subset of itself. restrict :: forall r r'. (WellBehaved r, Subset r r') => Var r' -> Maybe (Var r) -- | Split a variant into two sub-variants. split :: forall s r. (WellBehaved s, Subset s r) => Var r -> Either (Var (r .\\ s)) (Var s) -- | Type level label fetching type family (r :: Row k) .! (t :: Symbol) :: k infixl 5 .! -- | Type level Row element removal type family (r :: Row k) .- (s :: Symbol) :: Row k infixl 6 .- -- | Type level Row difference. That is, l .\\ r is the row -- remaining after removing any matching elements of r from -- l. type family (l :: Row k) .\\ (r :: Row k) :: Row k infixl 6 .\\ -- | A type level way to create a singleton Row. type (l :: Symbol) .== (a :: k) = Extend l a Empty infix 7 .== -- | Convert a variant to a native Haskell type. toNative :: ToNative t => Var (NativeRow t) -> t -- | Convert a Haskell variant to a row-types Var. fromNative :: FromNative t => t -> Var (NativeRow t) -- | Convert a Haskell variant to a row-types Var. fromNativeGeneral :: FromNativeGeneral t ρ => t -> Var ρ type ToNative t = (Generic t, ToNativeG (Rep t)) type FromNative t = (Generic t, FromNativeG (Rep t)) type FromNativeGeneral t ρ = (Generic t, FromNativeGeneralG (Rep t) ρ) type family NativeRow t -- | Map a type level function over a Row. type family Map (f :: a -> b) (r :: Row a) :: Row b -- | A function to map over a variant given a constraint. map :: forall c f r. Forall r c => (forall a. c a => a -> f a) -> Var r -> Var (Map f r) -- | A function to map over a variant given no constraint. map' :: forall f r. FreeForall r => (forall a. a -> f a) -> Var r -> Var (Map f r) -- | Lifts a natrual transformation over a variant. In other words, it acts -- as a variant transformer to convert a variant of f a values -- to a variant of g a values. If no constraint is needed, -- instantiate the first type argument with Unconstrained1. transform :: forall c r f g. Forall r c => (forall a. c a => f a -> g a) -> Var (Map f r) -> Var (Map g r) -- | A form of transformC that doesn't have a constraint on -- a transform' :: forall r f g. FreeForall r => (forall a. f a -> g a) -> Var (Map f r) -> Var (Map g r) -- | Any structure over a row in which every element is similarly -- constrained can be metamorphized into another structure over the same -- row. class Forall (r :: Row k) (c :: k -> Constraint) -- | A standard fold erase :: forall c ρ b. Forall ρ c => (forall a. c a => a -> b) -> Var ρ -> b -- | A fold with labels eraseWithLabels :: forall c ρ s b. (Forall ρ c, IsString s) => (forall a. c a => a -> b) -> Var ρ -> (s, b) -- | A fold over two variants at once. A call eraseZipGeneral f x -- y will return f (Left (show l, a, b)) when x -- and y both have values at the same label l and will -- return f (Right ((show l1, a), (show l2, b))) when they have -- values at different labels l1 and l2 respectively. eraseZipGeneral :: forall c ρ b s. (Forall ρ c, IsString s) => (forall x y. (c x, c y) => Either (s, x, x) ((s, x), (s, y)) -> b) -> Var ρ -> Var ρ -> b -- | A simpler fold over two variants at once eraseZip :: forall c ρ b. Forall ρ c => (forall a. c a => a -> a -> b) -> Var ρ -> Var ρ -> Maybe b -- | Traverse a function over a variant. traverse :: forall c f r. (Forall r c, Functor f) => (forall a. c a => a -> f a) -> Var r -> f (Var r) -- | Traverse a function over a Mapped variant. traverseMap :: forall c f g h r. (Forall r c, Functor f) => (forall a. c a => g a -> f (h a)) -> Var (Map g r) -> f (Var (Map h r)) -- | Applicative sequencing over a variant sequence :: forall f r. (FreeForall r, Functor f) => Var (Map f r) -> f (Var r) -- | Convert from a variant where two functors have been mapped over the -- types to one where the composition of the two functors is mapped over -- the types. compose :: forall f g r. FreeForall r => Var (Map f (Map g r)) -> Var (Map (Compose f g) r) -- | Convert from a variant 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. uncompose :: forall f g r. FreeForall r => Var (Map (Compose f g) r) -> Var (Map f (Map g r)) -- | Return a list of the labels in a row type. labels :: forall ρ c s. (IsString s, Forall ρ c) => [s] -- | A version of erase that works even when the row-type of the -- variant argument is of the form ApSingle fs x. eraseSingle :: forall c fs x y. Forall fs c => (forall f. c f => f x -> y) -> Var (ApSingle fs x) -> y -- | Performs a functorial-like map over an ApSingle variant. In -- other words, it acts as a variant transformer to convert a variant of -- f x values to a variant of f y values. If no -- constraint is needed, instantiate the first type argument with -- Unconstrained1. mapSingle :: forall c fs x y. Forall fs c => (forall f. c f => f x -> f y) -> Var (ApSingle fs x) -> Var (ApSingle fs y) -- | Like mapSingle, but works over a functor. mapSingleA :: forall c fs g x y. (Forall fs c, Functor g) => (forall f. c f => f x -> g (f y)) -> Var (ApSingle fs x) -> g (Var (ApSingle fs y)) -- | A version of eraseZip that works even when the row-types of the -- variant arguments are of the form ApSingle fs x. eraseZipSingle :: forall c fs x y z. Forall fs c => (forall f. c f => f x -> f y -> z) -> Var (ApSingle fs x) -> Var (ApSingle fs y) -> Maybe z -- | Coerce a variant to a coercible representation. The BiForall in -- the context indicates that the type of any option in r1 can -- be coerced to the type of the corresponding option in r2. -- -- Internally, this is implemented just with unsafeCoerce, but we -- provide the following implementation as a proof: -- --
--   newtype ConstV a b = ConstV { unConstV :: Var a }
--   newtype ConstV a b = FlipConstV { unFlipConstV :: Var b }
--   coerceVar :: forall r1 r2. BiForall r1 r2 Coercible => Var r1 -> Var r2
--   coerceVar = unFlipConstV . biMetamorph @_ @_ @r1 @r2 @Coercible @Either @ConstV @FlipConstV @Const Proxy doNil doUncons doCons . ConstV
--     where
--       doNil = impossible . unConstV
--       doUncons l = bimap ConstV Const . flip trial l . unConstV
--       doCons :: forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, Coercible τ1 τ2, AllUniqueLabels (Extend ℓ τ2 ρ2))
--              => Label ℓ -> Either (FlipConstV ρ1 ρ2) (Const τ1 τ2)
--              -> FlipConstV (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2)
--       doCons l (Left (FlipConstV v)) = FlipConstV $ extend @τ2 l v
--       doCons l (Right (Const x)) = FlipConstV $ IsJust l (coerce @τ1 @τ2 x)
--         \\ extendHas @ρ2 @ℓ @τ2
--   
coerceVar :: forall r1 r2. BiForall r1 r2 Coercible => Var r1 -> Var r2 instance forall k (cs :: k -> *) (ρ :: Data.Row.Internal.Row *) (m :: GHC.Generics.Meta). Data.Row.Variants.FromNativeGeneralG cs ρ => Data.Row.Variants.FromNativeGeneralG (GHC.Generics.D1 m cs) ρ instance Data.Row.Variants.FromNativeGeneralG GHC.Generics.V1 ρ instance (GHC.TypeLits.KnownSymbol name, (ρ Data.Row.Internal..! name) Data.Row.Internal.≈ t, Data.Row.Internal.AllUniqueLabels ρ) => Data.Row.Variants.FromNativeGeneralG (GHC.Generics.C1 ('GHC.Generics.MetaCons name fixity sels) (GHC.Generics.S1 m (GHC.Generics.Rec0 t))) ρ instance forall k (l :: k -> *) (ρ :: Data.Row.Internal.Row *) (r :: k -> *). (Data.Row.Variants.FromNativeGeneralG l ρ, Data.Row.Variants.FromNativeGeneralG r ρ) => Data.Row.Variants.FromNativeGeneralG (l GHC.Generics.:+: r) ρ instance forall k (cs :: k -> *) (m :: GHC.Generics.Meta). Data.Row.Variants.FromNativeG cs => Data.Row.Variants.FromNativeG (GHC.Generics.D1 m cs) instance Data.Row.Variants.FromNativeG GHC.Generics.V1 instance GHC.TypeLits.KnownSymbol name => Data.Row.Variants.FromNativeG (GHC.Generics.C1 ('GHC.Generics.MetaCons name fixity sels) (GHC.Generics.S1 m (GHC.Generics.Rec0 t))) instance forall k (l :: k -> *) (r :: k -> *). (Data.Row.Variants.FromNativeG l, Data.Row.Variants.FromNativeG r) => Data.Row.Variants.FromNativeG (l GHC.Generics.:+: r) instance forall k (cs :: k -> *) (m :: GHC.Generics.Meta). Data.Row.Variants.ToNativeG cs => Data.Row.Variants.ToNativeG (GHC.Generics.D1 m cs) instance Data.Row.Variants.ToNativeG GHC.Generics.V1 instance GHC.TypeLits.KnownSymbol name => Data.Row.Variants.ToNativeG (GHC.Generics.C1 ('GHC.Generics.MetaCons name fixity sels) (GHC.Generics.S1 m (GHC.Generics.Rec0 t))) instance forall k (l :: k -> *) (r :: k -> *). (Data.Row.Variants.ToNativeG l, Data.Row.Variants.ToNativeG r, ((Data.Row.Variants.NativeRowG l Data.Row.Internal..+ Data.Row.Variants.NativeRowG r) Data.Row.Internal..\\ Data.Row.Variants.NativeRowG r) Data.Row.Internal.≈ Data.Row.Variants.NativeRowG l, Data.Row.Internal.AllUniqueLabels (Data.Row.Variants.NativeRowG r), Data.Row.Dictionaries.FreeForall (Data.Row.Variants.NativeRowG r)) => Data.Row.Variants.ToNativeG (l GHC.Generics.:+: r) instance Data.Row.Variants.GenericVar r => GHC.Generics.Generic (Data.Row.Variants.Var r) instance Data.Row.Variants.GenericVar Data.Row.Internal.Empty instance GHC.TypeLits.KnownSymbol name => Data.Row.Variants.GenericVar ('Data.Row.Internal.R '[ name 'Data.Row.Internal.:-> t]) instance (Data.Row.Variants.GenericVar ('Data.Row.Internal.R ((name' 'Data.Row.Internal.:-> t') : r')), GHC.TypeLits.KnownSymbol name, Data.Row.Internal.Extend name t ('Data.Row.Internal.R ((name' 'Data.Row.Internal.:-> t') : r')) Data.Row.Internal.≈ 'Data.Row.Internal.R ((name 'Data.Row.Internal.:-> t) : (name' 'Data.Row.Internal.:-> t') : r'), Data.Row.Internal.AllUniqueLabels ('Data.Row.Internal.R ((name 'Data.Row.Internal.:-> t) : (name' 'Data.Row.Internal.:-> t') : r'))) => Data.Row.Variants.GenericVar ('Data.Row.Internal.R ((name 'Data.Row.Internal.:-> t) : (name' 'Data.Row.Internal.:-> t') : r')) instance Data.Row.Internal.Forall r GHC.Show.Show => GHC.Show.Show (Data.Row.Variants.Var r) instance Data.Row.Internal.Forall r GHC.Classes.Eq => GHC.Classes.Eq (Data.Row.Variants.Var r) instance (Data.Row.Internal.Forall r GHC.Classes.Eq, Data.Row.Internal.Forall r GHC.Classes.Ord) => GHC.Classes.Ord (Data.Row.Variants.Var r) instance Data.Row.Internal.Forall r Control.DeepSeq.NFData => Control.DeepSeq.NFData (Data.Row.Variants.Var r) instance (Data.Row.Internal.AllUniqueLabels r, Data.Row.Internal.AllUniqueLabels r', GHC.TypeLits.KnownSymbol name, (r Data.Row.Internal..! name) Data.Row.Internal.≈ a, (r' Data.Row.Internal..! name) Data.Row.Internal.≈ b, r' Data.Row.Internal.≈ ((r Data.Row.Internal..- name) Data.Row.Internal..\/ (name Data.Row.Internal..== b))) => Data.Generics.Sum.Constructors.AsConstructor name (Data.Row.Variants.Var r) (Data.Row.Variants.Var r') a b instance (Data.Row.Internal.AllUniqueLabels r, GHC.TypeLits.KnownSymbol name, (r Data.Row.Internal..! name) Data.Row.Internal.≈ a, r Data.Row.Internal.≈ ((r Data.Row.Internal..- name) Data.Row.Internal..\/ (name Data.Row.Internal..== a))) => Data.Generics.Sum.Constructors.AsConstructor' name (Data.Row.Variants.Var r) a -- | This module provides the ability to discharge a polymorphic variant -- using a record that has matching fields. module Data.Row.Switch -- | A simple class that we use to provide a constraint for function -- application. class AppliesTo r f x | r x -> f, f r -> x applyTo :: AppliesTo r f x => f -> x -> r -- | A Var and a Rec can combine if their rows line up -- properly. Given a Variant along with a Record of functions from each -- possible value of the variant to a single output type, apply the -- correct function to the value in the variant. switch :: forall v r x. BiForall r v (AppliesTo x) => Var v -> Rec r -> x -- | The same as switch but with the argument order reversed caseon :: forall v r x. BiForall r v (AppliesTo x) => Rec r -> Var v -> x instance Data.Row.Switch.AppliesTo r (x -> r) x -- | This module includes a set of common functions for Records and -- Variants. It includes: -- -- -- -- It specifically excludes: -- -- -- -- If these particular functions are needed, they should be brought in -- qualified from one of the Data.Row.*** modules directly. module Data.Row -- | A label data Label (s :: Symbol) Label :: Label (s :: Symbol) -- | This class gives the string associated with a type-level symbol. There -- are instances of the class for every concrete literal: "hello", etc. class KnownSymbol (n :: Symbol) -- | Are all of the labels in this Row unique? type family AllUniqueLabels (r :: Row k) :: Constraint -- | A convenient way to provide common, easy constraints type WellBehaved ρ = (Forall ρ Unconstrained1, AllUniqueLabels ρ) -- | The variant type. data Var (r :: Row *) -- | A record with row r. data Rec (r :: Row *) -- | 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. data Row a -- | Type level version of empty type Empty = R '[] -- | A lower fixity operator for type equality type a ≈ b = a ~ b infix 4 ≈ -- | Alias for (r .! l) ≈ a. It is a class rather than an alias, -- so that it can be partially applied. class (r .! l ≈ a) => HasType l a r -- | Is the first row a subset of the second? Or, does the second row -- contain every binding that the first one does? type family Subset (r1 :: Row k) (r2 :: Row k) :: Constraint -- | Alias for .\. It is a class rather than an alias, so that it -- can be partially applied. class Lacks (l :: Symbol) (r :: Row *) -- | Does the row lack (i.e. it does not have) the specified label? type family (r :: Row k) .\ (l :: Symbol) :: Constraint infixl 4 .\ -- | Type level Row append type family (l :: Row k) .+ (r :: Row k) :: Row k infixl 6 .+ -- | The minimum join of the two rows. type family (l :: Row k) .\/ (r :: Row k) infixl 6 .\/ -- | Type level Row difference. That is, l .\\ r is the row -- remaining after removing any matching elements of r from -- l. type family (l :: Row k) .\\ (r :: Row k) :: Row k infixl 6 .\\ -- | The overwriting union, where the left row overwrites the types of the -- right row where the labels overlap. type family (l :: Row k) .// (r :: Row k) infixl 6 .// -- | 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. class BiForall (r1 :: Row k1) (r2 :: Row k2) (c :: k1 -> k2 -> Constraint) -- | Any structure over a row in which every element is similarly -- constrained can be metamorphized into another structure over the same -- row. class Forall (r :: Row k) (c :: k -> Constraint) -- | FreeForall can be used when a Forall constraint is -- necessary but there is no particular constraint we care about. type FreeForall r = Forall r Unconstrained1 -- | FreeForall can be used when a BiForall constraint is -- necessary but there is no particular constraint we care about. type FreeBiForall r1 r2 = BiForall r1 r2 Unconstrained2 -- | A Var and a Rec can combine if their rows line up -- properly. Given a Variant along with a Record of functions from each -- possible value of the variant to a single output type, apply the -- correct function to the value in the variant. switch :: forall v r x. BiForall r v (AppliesTo x) => Var v -> Rec r -> x -- | The same as switch but with the argument order reversed caseon :: forall v r x. BiForall r v (AppliesTo x) => Rec r -> Var v -> x -- | The empty record empty :: Rec Empty -- | A type level way to create a singleton Row. type (l :: Symbol) .== (a :: k) = Extend l a Empty infix 7 .== -- | The singleton record (.==) :: 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. pattern (:==) :: forall l a. KnownSymbol l => Label l -> a -> Rec (l .== a) infix 7 :== -- | Type level Row element removal type family (r :: Row k) .- (s :: Symbol) :: Row k infixl 6 .- -- | Record restriction. Remove the label l from the record. (.-) :: KnownSymbol l => Rec r -> Label l -> Rec (r .- l) infixl 6 .- -- | Type level label fetching type family (r :: Row k) .! (t :: Symbol) :: k infixl 5 .! -- | Record selection (.!) :: KnownSymbol l => Rec r -> Label l -> r .! l -- | Record disjoint union (commutative) (.+) :: forall l r. FreeForall l => Rec l -> Rec r -> Rec (l .+ r) infixl 6 .+ -- | A type synonym for disjointness. 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 pattern version of record union, for use in pattern matching. pattern (:+) :: forall l r. Disjoint l r => Rec l -> Rec r -> Rec (l .+ r) infixl 6 :+ -- | Record overwrite. -- -- The operation r .// r' creates a new record such that: -- -- -- -- This can be thought of as r "overwriting" r'. (.//) :: Rec r -> Rec r' -> Rec (r .// r') infixl 6 .// -- | A pattern for variants; can be used to both destruct a variant when in -- a pattern position or construct one in an expression position. pattern IsJust :: forall l r. (AllUniqueLabels r, KnownSymbol l) => Label l -> (r .! l) -> Var r -- | Make the variant arbitrarily more diverse. diversify :: forall r' r. Var r -> Var (r .\/ r') -- | A Variant with no options is uninhabited. impossible :: Var Empty -> a -- | Convert a variant into either the value at the given label or a -- variant without that label. This is the basic variant destructor. trial :: KnownSymbol l => Var r -> Label l -> Either (Var (r .- l)) (r .! l) -- | A version of trial that ignores the leftover variant. trial' :: KnownSymbol l => Var r -> Label l -> Maybe (r .! l) -- | A trial over multiple types multiTrial :: forall x y. (AllUniqueLabels x, FreeForall x) => Var y -> Either (Var (y .\\ x)) (Var x) -- | Return a list of the labels in a row type. labels :: forall ρ c s. (IsString s, Forall ρ c) => [s]