Safe Haskell | None |
---|---|
Language | Haskell2010 |
This module implements extensible variants using closed type families.
Synopsis
- data Label (s :: Symbol) = Label
- class KnownSymbol (n :: Symbol)
- type family AllUniqueLabels (r :: Row k) :: Constraint where ...
- type WellBehaved ρ = (Forall ρ Unconstrained1, AllUniqueLabels ρ)
- data Var (r :: Row *)
- data Row a
- type Empty = R '[]
- type (≈) a b = a ~ b
- class (r .! l) ≈ a => HasType l a r
- pattern IsJust :: forall l r. (AllUniqueLabels r, KnownSymbol l) => Label l -> (r .! l) -> Var r
- singleton :: KnownSymbol l => Label l -> a -> Var (l .== a)
- unSingleton :: forall l a. KnownSymbol l => Var (l .== a) -> (Label l, a)
- fromLabels :: forall c ρ f. (Alternative f, Forall ρ c, AllUniqueLabels ρ) => (forall l a. (KnownSymbol l, c a) => Label l -> f a) -> f (Var ρ)
- 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 ρ))
- type family (r :: Row k) .\ (l :: Symbol) :: Constraint where ...
- class Lacks (l :: Symbol) (r :: Row *)
- type family (l :: Row k) .\/ (r :: Row k) where ...
- diversify :: forall r' r. Var r -> Var (r .\/ r')
- extend :: forall a l r. KnownSymbol l => Label l -> Var r -> Var (Extend l a r)
- type family (l :: Row k) .+ (r :: Row k) :: Row k where ...
- update :: (KnownSymbol l, (r .! l) ≈ a) => Label l -> a -> Var r -> Var r
- 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 family Modify (l :: Symbol) (a :: k) (r :: Row k) :: Row k where ...
- rename :: (KnownSymbol l, KnownSymbol l') => Label l -> Label l' -> Var r -> Var (Rename l l' r)
- type family Rename (l :: Symbol) (l' :: Symbol) (r :: Row k) :: Row k where ...
- impossible :: Var Empty -> a
- trial :: KnownSymbol l => Var r -> Label l -> Either (Var (r .- l)) (r .! l)
- trial' :: KnownSymbol l => Var r -> Label l -> Maybe (r .! l)
- multiTrial :: forall x y. (AllUniqueLabels x, Forall (y .\\ x) Unconstrained1) => Var y -> Either (Var (y .\\ x)) (Var x)
- view :: KnownSymbol l => Label l -> Var r -> Maybe (r .! l)
- restrict :: forall r r'. (WellBehaved r, Subset r r') => Var r' -> Maybe (Var r)
- split :: forall s r. (WellBehaved s, Subset s r) => Var r -> Either (Var (r .\\ s)) (Var s)
- type family (r :: Row k) .! (t :: Symbol) :: k where ...
- type family (r :: Row k) .- (s :: Symbol) :: Row k where ...
- type family (l :: Row k) .\\ (r :: Row k) :: Row k where ...
- type (.==) (l :: Symbol) (a :: k) = Extend l a Empty
- toNative :: ToNative t => Var (NativeRow t) -> t
- fromNative :: FromNative t => t -> Var (NativeRow t)
- 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 where ...
- 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) -> Var r -> Var (Map f r)
- map' :: forall f r. FreeForall r => (forall a. a -> f a) -> Var r -> Var (Map f r)
- 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)
- transform' :: forall r (f :: * -> *) (g :: * -> *). FreeForall r => (forall a. f a -> g a) -> Var (Map f r) -> Var (Map g r)
- class Forall (r :: Row k) (c :: k -> Constraint)
- erase :: forall c ρ b. Forall ρ c => (forall a. c a => a -> b) -> Var ρ -> b
- eraseWithLabels :: forall c ρ s b. (Forall ρ c, IsString s) => (forall a. c a => a -> b) -> Var ρ -> (s, b)
- 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
- eraseZip :: forall c ρ b. Forall ρ c => (forall a. c a => a -> a -> b) -> Var ρ -> Var ρ -> Maybe b
- traverse :: forall c f r. (Forall r c, Applicative f) => (forall a. c a => a -> f a) -> Var r -> f (Var r)
- traverseMap :: forall c (f :: * -> *) (g :: * -> *) (h :: * -> *) r. (Forall r c, Applicative f) => (forall a. c a => g a -> f (h a)) -> Var (Map g r) -> f (Var (Map h r))
- sequence :: forall f r. (FreeForall r, Applicative f) => Var (Map f r) -> f (Var r)
- compose :: forall (f :: * -> *) (g :: * -> *) r. FreeForall r => Var (Map f (Map g r)) -> Var (Map (Compose f g) r)
- uncompose :: forall (f :: * -> *) (g :: * -> *) r. FreeForall r => Var (Map (Compose f g) r) -> Var (Map f (Map g r))
- labels :: forall ρ c s. (IsString s, Forall ρ c) => [s]
- eraseSingle :: forall (c :: (* -> *) -> Constraint) (fs :: Row (* -> *)) (x :: *) (y :: *). Forall fs c => (forall f. c f => f x -> y) -> Var (ApSingle fs x) -> y
- mapSingle :: forall (c :: (* -> *) -> Constraint) (fs :: Row (* -> *)) (x :: *) (y :: *). Forall fs c => (forall f. c f => f x -> f y) -> Var (ApSingle fs x) -> Var (ApSingle fs y)
- 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
- coerceVar :: forall r1 r2. BiForall r1 r2 Coercible => Var r1 -> Var r2
Types and constraints
data Label (s :: Symbol) Source #
A label
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: base-4.7.0.0
symbolSing
type family AllUniqueLabels (r :: Row k) :: 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
data Var (r :: Row *) Source #
The variant type.
Instances
(AllUniqueLabels r, KnownSymbol name, (r .! name) ≈ a, r ≈ ((r .- name) .\/ (name .== a))) => AsConstructor' name (Var r) a Source # | |
(AllUniqueLabels r, AllUniqueLabels r', KnownSymbol name, (r .! name) ≈ a, (r' .! name) ≈ b, r' ≈ ((r .- name) .\/ (name .== b))) => AsConstructor name (Var r) (Var r') a b Source # | Every possibility of a row-types based variant has an |
Forall r Eq => Eq (Var r) Source # | |
(Forall r Eq, Forall r Ord) => Ord (Var r) Source # | |
Forall r Show => Show (Var r) Source # | |
GenericVar r => Generic (Var r) Source # | |
Forall r NFData => NFData (Var r) Source # | |
Defined in Data.Row.Variants | |
type Rep (Var r) Source # | |
Defined in Data.Row.Variants |
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
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.
pattern IsJust :: forall l r. (AllUniqueLabels r, KnownSymbol l) => Label l -> (r .! l) -> Var r Source #
A pattern for variants; can be used to both destruct a variant when in a pattern position or construct one in an expression position.
singleton :: KnownSymbol l => Label l -> a -> Var (l .== a) Source #
A quick constructor to create a singleton variant.
unSingleton :: forall l a. KnownSymbol l => Var (l .== a) -> (Label l, a) Source #
A quick destructor for singleton variants.
fromLabels :: forall c ρ f. (Alternative f, Forall ρ c, AllUniqueLabels ρ) => (forall l a. (KnownSymbol l, c a) => Label l -> f a) -> f (Var ρ) Source #
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.
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 ρ)) Source #
Initialize a variant over a Map
.
Extension
type family (r :: Row k) .\ (l :: Symbol) :: Constraint where ... infixl 4 Source #
Does the row lack (i.e. it does not have) the specified label?
class Lacks (l :: Symbol) (r :: Row *) Source #
Alias for .\
. It is a class rather than an alias, so that
it can be partially applied.
Instances
r .\ l => Lacks l r Source # | |
Defined in Data.Row.Internal |
type family (l :: Row k) .\/ (r :: Row k) where ... infixl 6 Source #
The minimum join of the two rows.
diversify :: forall r' r. Var r -> Var (r .\/ r') Source #
Make the variant arbitrarily more diverse.
Modification
update :: (KnownSymbol l, (r .! l) ≈ a) => Label l -> a -> Var r -> Var r Source #
If the variant exists at the given label, update it to the given value. 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')) Source #
If the variant exists at the given label, focus on the value associated with it. Otherwise, do nothing.
type family Modify (l :: Symbol) (a :: k) (r :: Row k) :: Row k where ... Source #
Type level Row modification
rename :: (KnownSymbol l, KnownSymbol l') => Label l -> Label l' -> Var r -> Var (Rename l l' r) Source #
Rename the given label.
type family Rename (l :: Symbol) (l' :: Symbol) (r :: Row k) :: Row k where ... Source #
Type level row renaming
Destruction
impossible :: Var Empty -> a Source #
A Variant with no options is uninhabited.
trial :: KnownSymbol l => Var r -> Label l -> Either (Var (r .- l)) (r .! l) Source #
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 -> Maybe (r .! l) Source #
A version of trial
that ignores the leftover variant.
multiTrial :: forall x y. (AllUniqueLabels x, Forall (y .\\ x) Unconstrained1) => Var y -> Either (Var (y .\\ x)) (Var x) Source #
A trial over multiple types
view :: KnownSymbol l => Label l -> Var r -> Maybe (r .! l) Source #
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
restrict :: forall r r'. (WellBehaved r, Subset r r') => Var r' -> Maybe (Var r) Source #
Arbitrary variant restriction. Turn a variant into a subset of itself.
split :: forall s r. (WellBehaved s, Subset s r) => Var r -> Either (Var (r .\\ s)) (Var s) Source #
Split a variant into two sub-variants.
Types for destruction
type family (r :: Row k) .- (s :: Symbol) :: Row k where ... infixl 6 Source #
Type level Row element removal
type family (l :: Row k) .\\ (r :: Row k) :: Row k where ... infixl 6 Source #
Type level Row difference. That is, l
is the row remaining after
removing any matching elements of .\\
rr
from l
.
type (.==) (l :: Symbol) (a :: k) = Extend l a Empty infix 7 Source #
A type level way to create a singleton Row.
Native Conversion
The toNative
and fromNative
functions allow one to convert between
Var
s and regular Haskell data types ("native" types) that have the same
number of constructors such that each constructor has one field and the same
name as one of the options of the Var
, which has the same type as that field.
As expected, they compose to form the identity. Alternatively, one may use
fromNativeGeneral
, which allows a variant with excess options to still be
transformed to a native type. Because of this, fromNativeGeneral
requires a type
application (although fromNative
does not). The only requirement is that
the native Haskell data type be an instance of Generic
.
For example, consider the following simple data type:
>>>
data Pet = Dog {age :: Int} | Cat {age :: Int} deriving (Generic, Show)
Then, we have the following:
>>>
toNative $ IsJust (Label @"Dog") 3 :: Pet
Dog {age = 3}>>>
V.fromNative $ Dog 3 :: Var ("Dog" .== Int .+ "Cat" .== Int)
{Dog=3}
toNative :: ToNative t => Var (NativeRow t) -> t Source #
Convert a variant to a native Haskell type.
fromNative :: FromNative t => t -> Var (NativeRow t) Source #
Convert a Haskell variant to a row-types Var.
fromNativeGeneral :: FromNativeGeneral t ρ => t -> Var ρ Source #
Convert a Haskell variant to a row-types Var.
type FromNative t = (Generic t, FromNativeG (Rep t)) Source #
type FromNativeGeneral t ρ = (Generic t, FromNativeGeneralG (Rep t) ρ) Source #
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) -> Var r -> Var (Map f r) Source #
A function to map over a variant given a constraint.
map' :: forall f r. FreeForall r => (forall a. a -> f a) -> Var r -> Var (Map f r) Source #
A function to map over a variant given no constraint.
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) Source #
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 r (f :: * -> *) (g :: * -> *). FreeForall r => (forall a. f a -> g a) -> Var (Map f r) -> Var (Map g r) Source #
A form of transformC
that doesn't have a constraint on a
Fold
class Forall (r :: Row k) (c :: k -> Constraint) Source #
Any structure over a row in which every element is similarly constrained can be metamorphized into another structure over the same row.
Instances
(KnownSymbol ℓ, c τ, Forall (R ρ) c, FrontExtends ℓ τ (R ρ), AllUniqueLabels (Extend ℓ τ (R ρ))) => Forall (R ((ℓ :-> τ) ': ρ) :: Row k) (c :: k -> Constraint) Source # | |
Defined in Data.Row.Internal metamorph :: Bifunctor p => Proxy (Proxy h, Proxy p) -> (f Empty -> g Empty) -> (forall (ℓ0 :: Symbol) (τ0 :: k0) (ρ0 :: Row k0). (KnownSymbol ℓ0, c τ0, HasType ℓ0 τ0 ρ0) => Label ℓ0 -> f ρ0 -> p (f (ρ0 .- ℓ0)) (h τ0)) -> (forall (ℓ1 :: Symbol) (τ1 :: k0) (ρ1 :: Row k0). (KnownSymbol ℓ1, c τ1, FrontExtends ℓ1 τ1 ρ1, AllUniqueLabels (Extend ℓ1 τ1 ρ1)) => Label ℓ1 -> p (g ρ1) (h τ1) -> g (Extend ℓ1 τ1 ρ1)) -> f (R ((ℓ :-> τ) ': ρ)) -> g (R ((ℓ :-> τ) ': ρ)) Source # | |
Forall (R ([] :: [LT k]) :: Row k) (c :: k -> Constraint) Source # | |
Defined in Data.Row.Internal metamorph :: Bifunctor p => Proxy (Proxy h, Proxy p) -> (f Empty -> g Empty) -> (forall (ℓ :: Symbol) (τ :: k0) (ρ :: Row k0). (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) => Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ)) -> (forall (ℓ :: Symbol) (τ :: k0) (ρ :: Row k0). (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ, AllUniqueLabels (Extend ℓ τ ρ)) => Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ)) -> f (R []) -> g (R []) Source # |
erase :: forall c ρ b. Forall ρ c => (forall a. c a => a -> b) -> Var ρ -> b Source #
A standard fold
eraseWithLabels :: forall c ρ s b. (Forall ρ c, IsString s) => (forall a. c a => a -> b) -> Var ρ -> (s, b) Source #
A fold with labels
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 Source #
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.
eraseZip :: forall c ρ b. Forall ρ c => (forall a. c a => a -> a -> b) -> Var ρ -> Var ρ -> Maybe b Source #
A simpler fold over two variants at once
Applicative-like functions
traverse :: forall c f r. (Forall r c, Applicative f) => (forall a. c a => a -> f a) -> Var r -> f (Var r) Source #
Traverse a function over a variant.
traverseMap :: forall c (f :: * -> *) (g :: * -> *) (h :: * -> *) r. (Forall r c, Applicative f) => (forall a. c a => g a -> f (h a)) -> Var (Map g r) -> f (Var (Map h r)) Source #
Traverse a function over a Mapped variant.
sequence :: forall f r. (FreeForall r, Applicative f) => Var (Map f r) -> f (Var r) Source #
Applicative sequencing over a variant
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. FreeForall r => Var (Map f (Map g r)) -> Var (Map (Compose f g) r) Source #
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.
uncompose :: forall (f :: * -> *) (g :: * -> *) r. FreeForall r => Var (Map (Compose f g) r) -> Var (Map f (Map g r)) Source #
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.
labels
labels :: forall ρ c s. (IsString s, Forall ρ c) => [s] Source #
Return a list of the labels in a row type.
ApSingle functions
eraseSingle :: forall (c :: (* -> *) -> Constraint) (fs :: Row (* -> *)) (x :: *) (y :: *). Forall fs c => (forall f. c f => f x -> y) -> Var (ApSingle fs x) -> y Source #
A version of erase
that works even when the row-type of the variant argument
is of the form ApSingle fs x
.
mapSingle :: forall (c :: (* -> *) -> Constraint) (fs :: Row (* -> *)) (x :: *) (y :: *). Forall fs c => (forall f. c f => f x -> f y) -> Var (ApSingle fs x) -> Var (ApSingle fs y) Source #
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
.
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 Source #
A version of eraseZip
that works even when the row-types of the variant
arguments are of the form ApSingle fs x
.
Coerce
coerceVar :: forall r1 r2. BiForall r1 r2 Coercible => Var r1 -> Var r2 Source #
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