Safe Haskell | None |
---|---|
Language | Haskell2010 |
Control.Monad.Dep.Advice
Description
This package provices the Advice
datatype, along for functions for creating,
manipulating, composing and applying values of that type.
Advice
s represent generic transformations on DepT
-effectful functions of
any number of arguments.
>>>
:{
foo0 :: DepT NilEnv IO (Sum Int) foo0 = pure (Sum 5) foo1 :: Bool -> DepT NilEnv IO (Sum Int) foo1 _ = foo0 foo2 :: Char -> Bool -> DepT NilEnv IO (Sum Int) foo2 _ = foo1 :}
They work for DepT
-actions of zero arguments:
>>>
advise (printArgs @Top stdout "foo0") foo0 `runDepT` NilEnv
foo0: Sum {getSum = 5}
And for functions of one or more arguments, provided they end on a DepT
-action:
>>>
advise (printArgs @Top stdout "foo1") foo1 False `runDepT` NilEnv
foo1: False Sum {getSum = 5}
>>>
advise (printArgs @Top stdout "foo2") foo2 'd' False `runDepT` NilEnv
foo2: 'd' False Sum {getSum = 5}
Advice
s can also tweak the result value of functions:
>>>
advise (returnMempty @Top @Top2) foo2 'd' False `runDepT` NilEnv
Sum {getSum = 0}
And they can be combined using Advice
's Monoid
instance before being applied
(although that might require harmonizing their constraint parameters):
>>>
advise (printArgs stdout "foo2" <> returnMempty) foo2 'd' False `runDepT` NilEnv
foo2: 'd' False Sum {getSum = 0}
Synopsis
- data Advice ca cem cr
- makeAdvice :: forall u ca cem cr. (forall as e m. (All ca as, cem e m, Monad m) => NP I as -> DepT e m (u, NP I as)) -> (forall e m r. (cem e m, Monad m, cr r) => u -> DepT e m r -> DepT e m r) -> Advice ca cem cr
- makeArgsAdvice :: forall ca cem cr. (forall as e m. (All ca as, cem e m, Monad m) => NP I as -> DepT e m (NP I as)) -> Advice ca cem cr
- makeExecutionAdvice :: forall ca cem cr. (forall e m r. (cem e m, Monad m, cr r) => DepT e m r -> DepT e m r) -> Advice ca cem cr
- advise :: forall ca cem cr as e m r advisee. (Multicurryable as e m r advisee, All ca as, cem e m, Monad m, cr r) => Advice ca cem cr -> advisee -> advisee
- class c (e (DepT e m)) (DepT e m) => Ensure c e m
- class Top2 e m
- class (f e m, g e m) => And2 f g e m
- class c m => MonadConstraint c e m
- class c e => EnvConstraint c e m
- class x ~ y => MustBe x y
- class (e' ~ e, m' ~ m) => MustBe2 e' m' e m
- restrictArgs :: forall more less cem cr. (forall r. more r :- less r) -> Advice less cem cr -> Advice more cem cr
- restrictEnv :: forall more ca less cr. (forall e m. more e m :- less e m) -> Advice ca less cr -> Advice ca more cr
- restrictResult :: forall more ca cem less. (forall r. more r :- less r) -> Advice ca cem less -> Advice ca cem more
- runFinalDepT :: forall as e m r curried. Multicurryable as e m r curried => m (e (DepT e m)) -> curried -> BaseMonadAtTheTip as e m r curried
- runFromEnv :: forall as e m r curried. (Multicurryable as e m r curried, Monad m) => m (e (DepT e m)) -> (e (DepT e m) -> curried) -> BaseMonadAtTheTip as e m r curried
- class Top (x :: k)
- class (f x, g x) => And (f :: k -> Constraint) (g :: k -> Constraint) (x :: k)
- class (AllF c xs, SListI xs) => All (c :: k -> Constraint) (xs :: [k])
- data NP (a :: k -> Type) (b :: [k]) where
- newtype I a = I a
- cfoldMap_NP :: forall k c (xs :: [k]) m proxy f. (All c xs, Monoid m) => proxy c -> (forall (a :: k). c a => f a -> m) -> NP f xs -> m
- newtype a :- b = Sub (a => Dict b)
- data Dict a where
The Advice type
data Advice ca cem cr Source #
A generic transformation of a DepT
-effectful function of any number of
arguments, provided the function satisfies certain constraints on the
arguments, the environment type constructor and base monad, and the return type.
It is parameterized by three constraints:
ca
of kindType -> Constraint
, the constraint required of each argument (usually something likeShow
).cem
of kind((Type -> Type) -> Type) -> (Type -> Type) -> Constraint
, a two-place constraint required of the environment type constructor / base monad combination. Note that the environment type constructor remains unapplied. That is, for a givencem
,cem NilEnv IO
kind-checks butcem (NilEnv IO) IO
doesn't. See alsoEnsure
.cr
of kindType -> Constraint
, the constraint required of the return type.
We can define Advice
s that work with concrete types by using MustBe
in
the case of ca
and cr
, and MustBe2
in the case of cem
.
Advice
s that don't care about a particular constraint can leave it
polymorphic, and this facilitates composition, but the constraint must be
given some concrete value (Top
in the case of ca
and cr
, Top2
in
the case of cem
) through type application at the moment of calling
advise
.
See Control.Monad.Dep.Advice.Basic for examples.
Instances
Semigroup (Advice ca cem cr) Source # | Aspects compose "sequentially" when tweaking the arguments, and
"concentrically" when tweaking the final The first |
Monoid (Advice ca cem cr) Source # | |
Creating Advice values
Arguments
:: forall u ca cem cr. (forall as e m. (All ca as, cem e m, Monad m) => NP I as -> DepT e m (u, NP I as)) | The function that tweaks the arguments. |
-> (forall e m r. (cem e m, Monad m, cr r) => u -> DepT e m r -> DepT e m r) | The function that tweaks the execution. |
-> Advice ca cem cr |
The most general (and complex) way of constructing Advice
s.
Advice
s work in two phases. First, the arguments of the transformed
function are collected into an n-ary product NP
, and passed to the
first argument of makeAdvice
, which produces a (possibly transformed)
product of arguments, along with some summary value of type u
. Use ()
as the summary value if you don't care about it.
In the second phase, the monadic action produced by the function once all
arguments have been given is transformed using the second argument of
makeAdvice
. This second argument also receives the summary value of
type u
calculated earlier.
>>>
:{
doesNothing :: forall ca cem cr. Advice ca cem cr doesNothing = makeAdvice @() (\args -> pure (pure args)) (\() action -> action) :}
IMPORTANT! When invoking makeAdvice
, you must always give the
type of the existential u
through a type application. Otherwise you'll
get weird "u is untouchable" errors.
Arguments
:: forall ca cem cr. (forall as e m. (All ca as, cem e m, Monad m) => NP I as -> DepT e m (NP I as)) | The function that tweaks the arguments. |
-> Advice ca cem cr |
Create an advice which only tweaks and/or analyzes the function arguments.
Notice that there's no u
parameter, unlike with makeAdvice
.
>>>
:{
doesNothing :: forall ca cem cr. Advice ca cem cr doesNothing = makeArgsAdvice pure :}
Arguments
:: forall ca cem cr. (forall e m r. (cem e m, Monad m, cr r) => DepT e m r -> DepT e m r) | The function that tweaks the execution. |
-> Advice ca cem cr |
Create an advice which only tweaks the execution of the final monadic action.
Notice that there's no u
parameter, unlike with makeAdvice
.
>>>
:{
doesNothing :: forall ca cem cr. Advice ca cem cr doesNothing = makeExecutionAdvice id :}
Applying Advices
Arguments
:: forall ca cem cr as e m r advisee. (Multicurryable as e m r advisee, All ca as, cem e m, Monad m, cr r) | |
=> Advice ca cem cr | The advice to apply. |
-> advisee | A function to be adviced. |
-> advisee |
Apply an Advice
to some compatible function. The function must have its
effects in DepT
, and satisfy the constraints required by the Advice
.
IMPORTANT! If the ca
, cem
or cr
constraints of the supplied
Advice
remain polymorphic, they must be given types by means of type
applications:
>>>
:{
foo :: Int -> DepT NilEnv IO String foo _ = pure "foo" advisedFoo1 = advise (returnMempty @Top @Top2) foo advisedFoo2 = advise @Top @Top2 returnMempty foo advisedFoo3 = advise (printArgs @Top stdout "args: ") foo advisedFoo4 = advise @_ @_ @Top (printArgs stdout "args: ") foo :}
Constraint helpers
Some class synonyms
to help create the constraints that parameterize the Advice
type.
This library also re-exports the Top
, And
and All
helpers from "sop-core":
Top
is the "always satisfied" constraint, useful when whe don't want to require anything specific inca
orcr
(cem
requiresTop2
).And
combines constraints forca
orcr
(cem
requiresAnd2
).All
says that some constraint is satisfied by all the components of anNP
product. In this library, it's used to stipulate constraints on the arguments of advised functions.
class c (e (DepT e m)) (DepT e m) => Ensure c e m Source #
Ensure
is a helper for lifting typeclass definitions of the form:
>>>
:{
type HasLogger :: Type -> (Type -> Type) -> Constraint class HasLogger em m | em -> m where logger :: em -> String -> m () :}
To work as the cem
constraint, like this:
>>>
type FooAdvice = Advice Top (Ensure HasLogger) Top
Why is it necessary? Two-place HasX
-style constraints receive the "fully
applied" type of the record-of-functions. That is: NilEnv IO
instead of
simply NilEnv
. This allows them to also work with monomorphic
environments (like those in RIO) whose type isn't parameterized by any monad.
But the cem
constraint works with the type constructor of the environment
record, of kind (Type -> Type) -> Type
, and not with the fully applied
type of kind Type
.
A two-place constraint which requires nothing of the environment and the base monad.
Useful as the cem
type application argument of advise
and restrictEnv
.
For similar behavior with the ar
and cr
type arguments of advise
and
restrictEnv
, use Top
from "sop-core".
>>>
type UselessAdvice = Advice Top Top2 Top
Instances
Top2 e m Source # | |
Defined in Control.Monad.Dep.Advice |
class (f e m, g e m) => And2 f g e m infixl 7 Source #
Combines two two-place constraints on the environment / monad pair.
For example, an advice which requires both Ensure HasLogger
and Ensure
HasRepository
might use this.
Useful to build the cem
type application argument of advise
and
restrictEnv
.
For similar behavior with the ar
and cr
type arguments of advise
and
restrictEnv
, use And
from "sop-core".
Instances
(f e m, g e m) => And2 f g e m Source # | |
Defined in Control.Monad.Dep.Advice |
class c m => MonadConstraint c e m Source #
Require a constraint only on the base monad, for example a base moonad with MonadIO
.
Useful to build cem
type application argument of advise
and restrictEnv
.
>>>
type FooAdvice = Advice Top (MonadConstraint MonadIO) Top
>>>
type FooAdvice = Advice Top (MonadConstraint (MonadReader Int)) Top
Instances
c m => MonadConstraint c e m Source # | |
Defined in Control.Monad.Dep.Advice |
class c e => EnvConstraint c e m Source #
Require a constraint only on the unapplied environment type constructor, which has kind (Type -> Type) -> Type
.
Can be used to build cem
type application argument of advise
and restrictEnv
.
Most of the time this is not what you want. One exception is when
pinning the environment with a MustBe
equality constraint, while
leaving the base monad free:
>>>
type FooAdvice = Advice Top (EnvConstraint (MustBe NilEnv)) Top
If what you want is to lift a two-parameter HasX
-style typeclass to cem
, use Ensure
instead.
Instances
c e => EnvConstraint c e m Source # | |
Defined in Control.Monad.Dep.Advice |
class x ~ y => MustBe x y Source #
A class synonym for (~)
, the type equality constraint.
Poly-kinded, so it can be applied both to type constructors (like monads) and to concrete types.
It this library it will be used partially applied:
>>>
type FooAdvice = Advice Top (MonadConstraint (MustBe IO)) Top
>>>
type FooAdvice = Advice Top Top2 (MustBe String)
Instances
x ~ y => MustBe (x :: k) (y :: k) Source # | |
Defined in Control.Monad.Dep.Advice |
class (e' ~ e, m' ~ m) => MustBe2 e' m' e m Source #
Pins both the environment type constructor and the base monad. Sometimes we don't want to advise functions in some generic environment, but in a concrete environment having access to all the fields, and in a concrete base monad.
Useful to build the cem
type application argument of advise
and
restricEnv
.
For similar behavior with the ar
and cr
type arguments of advise
and restrictEnv
, use MustBe
.
It this library it will be used partially applied:
>>>
type FooAdvice = Advice Top (MustBe2 NilEnv IO) Top
Instances
(e' ~ e, m' ~ m) => MustBe2 e' m' e m Source # | |
Defined in Control.Monad.Dep.Advice |
Combining Advices by harmonizing their constraints
Advice
values can be composed using the Monoid
instance, but only if
the have the same constraint parameters. It's unfortunate that—unlike with
normal functions—Advice
constaints aren't automatically "collected"
during composition.
We need to harmonize the constraints on each Advice
by turning them
into the combination of all constraints. The functions in this section
help with that.
These functions take as parameter evidence of entailment between
constraints, using the type (:-)
from the "constraints" package. But
how to construct such evidence? By using the Sub
and the Dict
constructors, with either an explicit type signature:
>>>
:{
returnMempty' :: Advice ca cem (Monoid `And` Show) returnMempty' = restrictResult (Sub Dict) returnMempty :}
or with a type application to the restriction function:
>>>
:{
returnMempty'' :: Advice ca cem (Monoid `And` Show) returnMempty'' = restrictResult @(Monoid `And` Show) (Sub Dict) returnMempty :}
Another example:
>>>
:{
type HasLogger :: Type -> (Type -> Type) -> Constraint class HasLogger em m | em -> m where logger :: em -> String -> m () doLogging :: Advice Show (Ensure HasLogger) cr doLogging = undefined type EnsureLoggerAndWriter :: ((Type -> Type) -> Type) -> (Type -> Type) -> Constraint type EnsureLoggerAndWriter = Ensure HasLogger `And2` MonadConstraint MonadIO doLogging':: Advice Show EnsureLoggerAndWriter cr doLogging'= restrictEnv (Sub Dict) doLogging doLogging'' = restrictEnv @EnsureLoggerAndWriter (Sub Dict) doLogging :}
Arguments
:: forall more less cem cr. (forall r. more r :- less r) | Evidence that one constraint implies the other. |
-> Advice less cem cr | Advice with less restrictive constraint on the args. |
-> Advice more cem cr | Advice with more restrictive constraint on the args. |
Makes the constraint on the arguments more restrictive.
Arguments
:: forall more ca less cr. (forall e m. more e m :- less e m) | Evidence that one constraint implies the other. |
-> Advice ca less cr | Advice with less restrictive constraint on the environment and base monad. |
-> Advice ca more cr | Advice with more restrictive constraint on the environment and base monad. |
Makes the constraint on the environment / monad more restrictive.
Arguments
:: forall more ca cem less. (forall r. more r :- less r) | Evidence that one constraint implies the other. |
-> Advice ca cem less | Advice with less restrictive constraint on the result. |
-> Advice ca cem more | Advice with more restrictive constraint on the result. |
Makes the constraint on the result more restrictive.
Invocation helpers
There functions are helpers for running DepT
computations, beyond what runDepT
provides.
They aren't directly related to Advice
s, but they require some of the same machinery, and that's why they are here.
Arguments
:: forall as e m r curried. (Multicurryable as e m r curried, Monad m) | |
=> m (e (DepT e m)) | action that gets hold of the environment |
-> (e (DepT e m) -> curried) | gets a function from the environment with effects in |
-> BaseMonadAtTheTip as e m r curried | a new function with effects in the base monad |
Given a base monad m
action that gets hold of the DepT
environment,
and a function capable of extracting a curried function from the
environment, run the DepT
transformer at the tip of the resulting curried
function.
Why put the environment behind the m
action? Well, since getting to the
end of the curried function takes some work, it's a good idea to have some
flexibility once we arrive there. For example, the environment could be
stored in a Data.IORef and change in response to events, perhaps with
advices being added or removed.
>>>
:{
type MutableEnv :: (Type -> Type) -> Type data MutableEnv m = MutableEnv { _foo :: Int -> m (Sum Int) } :}
>>>
:{
do envRef <- newIORef (MutableEnv (pure . Sum)) let foo' = runFromEnv (readIORef envRef) _foo do r <- foo' 7 print r modifyIORef envRef (\e -> e { _foo = advise @Top @Top2 returnMempty (_foo e) }) do r <- foo' 7 print r :} Sum {getSum = 7} Sum {getSum = 0}
"sop-core" re-exports
Some useful definitions re-exported the from "sop-core" package.
NP
is an n-ary product used to represent the arguments of advised functions.
I
is an identity functor. The arguments processed by an Advice
come wrapped in it.
cfoldMap_NP
is useful to construct homogeneous lists out of the NP
product, for example:
>>>
cfoldMap_NP (Proxy @Show) (\(I a) -> [show a]) (I False :* I (1::Int) :* Nil)
["False","1"]
A constraint that can always be satisfied.
Since: sop-core-0.2
Instances
Top (x :: k) | |
Defined in Data.SOP.Constraint |
class (f x, g x) => And (f :: k -> Constraint) (g :: k -> Constraint) (x :: k) infixl 7 #
Pairing of constraints.
Since: sop-core-0.2
Instances
(f x, g x) => And (f :: k -> Constraint) (g :: k -> Constraint) (x :: k) | |
Defined in Data.SOP.Constraint |
class (AllF c xs, SListI xs) => All (c :: k -> Constraint) (xs :: [k]) #
Require a constraint for every element of a list.
If you have a datatype that is indexed over a type-level
list, then you can use All
to indicate that all elements
of that type-level list must satisfy a given constraint.
Example: The constraint
All Eq '[ Int, Bool, Char ]
is equivalent to the constraint
(Eq Int, Eq Bool, Eq Char)
Example: A type signature such as
f :: All Eq xs => NP I xs -> ...
means that f
can assume that all elements of the n-ary
product satisfy Eq
.
Note on superclasses: ghc cannot deduce superclasses from All
constraints.
You might expect the following to compile
class (Eq a) => MyClass a foo :: (All Eq xs) => NP f xs -> z foo = [..] bar :: (All MyClass xs) => NP f xs -> x bar = foo
but it will fail with an error saying that it was unable to
deduce the class constraint
(or similar) in the
definition of AllF
Eq
xsbar
.
In cases like this you can use Dict
from Data.SOP.Dict
to prove conversions between constraints.
See this answer on SO for more details.
Minimal complete definition
Instances
All (c :: k -> Constraint) ('[] :: [k]) | |
Defined in Data.SOP.Constraint Methods cpara_SList :: proxy c -> r '[] -> (forall (y :: k0) (ys :: [k0]). (c y, All c ys) => r ys -> r (y ': ys)) -> r '[] # | |
(c x, All c xs) => All (c :: a -> Constraint) (x ': xs :: [a]) | |
Defined in Data.SOP.Constraint Methods cpara_SList :: proxy c -> r '[] -> (forall (y :: k) (ys :: [k]). (c y, All c ys) => r ys -> r (y ': ys)) -> r (x ': xs) # |
data NP (a :: k -> Type) (b :: [k]) where #
An n-ary product.
The product is parameterized by a type constructor f
and
indexed by a type-level list xs
. The length of the list
determines the number of elements in the product, and if the
i
-th element of the list is of type x
, then the i
-th
element of the product is of type f x
.
The constructor names are chosen to resemble the names of the list constructors.
Two common instantiations of f
are the identity functor I
and the constant functor K
. For I
, the product becomes a
heterogeneous list, where the type-level list describes the
types of its components. For
, the product becomes a
homogeneous list, where the contents of the type-level list are
ignored, but its length still specifies the number of elements.K
a
In the context of the SOP approach to generic programming, an n-ary product describes the structure of the arguments of a single data constructor.
Examples:
I 'x' :* I True :* Nil :: NP I '[ Char, Bool ] K 0 :* K 1 :* Nil :: NP (K Int) '[ Char, Bool ] Just 'x' :* Nothing :* Nil :: NP Maybe '[ Char, Bool ]
Constructors
Nil :: forall k (a :: k -> Type). NP a ('[] :: [k]) | |
(:*) :: forall k (a :: k -> Type) (x :: k) (xs :: [k]). a x -> NP a xs -> NP a (x ': xs) infixr 5 |
Instances
HTrans (NP :: (k1 -> Type) -> [k1] -> Type) (NP :: (k2 -> Type) -> [k2] -> Type) | |
Defined in Data.SOP.NP Methods htrans :: forall c (xs :: l1) (ys :: l2) proxy f g. AllZipN (Prod NP) c xs ys => proxy c -> (forall (x :: k10) (y :: k20). c x y => f x -> g y) -> NP f xs -> NP g ys # hcoerce :: forall (f :: k10 -> Type) (g :: k20 -> Type) (xs :: l1) (ys :: l2). AllZipN (Prod NP) (LiftedCoercible f g) xs ys => NP f xs -> NP g ys # | |
HPure (NP :: (k -> Type) -> [k] -> Type) | |
HAp (NP :: (k -> Type) -> [k] -> Type) | |
HCollapse (NP :: (k -> Type) -> [k] -> Type) | |
Defined in Data.SOP.NP | |
HTraverse_ (NP :: (k -> Type) -> [k] -> Type) | |
Defined in Data.SOP.NP Methods hctraverse_ :: forall c (xs :: l) g proxy f. (AllN NP c xs, Applicative g) => proxy c -> (forall (a :: k0). c a => f a -> g ()) -> NP f xs -> g () # htraverse_ :: forall (xs :: l) g f. (SListIN NP xs, Applicative g) => (forall (a :: k0). f a -> g ()) -> NP f xs -> g () # | |
HSequence (NP :: (k -> Type) -> [k] -> Type) | |
Defined in Data.SOP.NP Methods hsequence' :: forall (xs :: l) f (g :: k0 -> Type). (SListIN NP xs, Applicative f) => NP (f :.: g) xs -> f (NP g xs) # hctraverse' :: forall c (xs :: l) g proxy f f'. (AllN NP c xs, Applicative g) => proxy c -> (forall (a :: k0). c a => f a -> g (f' a)) -> NP f xs -> g (NP f' xs) # htraverse' :: forall (xs :: l) g f f'. (SListIN NP xs, Applicative g) => (forall (a :: k0). f a -> g (f' a)) -> NP f xs -> g (NP f' xs) # | |
All (Compose Eq f) xs => Eq (NP f xs) | |
(All (Compose Eq f) xs, All (Compose Ord f) xs) => Ord (NP f xs) | |
All (Compose Show f) xs => Show (NP f xs) | |
All (Compose Semigroup f) xs => Semigroup (NP f xs) | Since: sop-core-0.4.0.0 |
(All (Compose Monoid f) xs, All (Compose Semigroup f) xs) => Monoid (NP f xs) | Since: sop-core-0.4.0.0 |
All (Compose NFData f) xs => NFData (NP f xs) | Since: sop-core-0.2.5.0 |
Defined in Data.SOP.NP | |
type AllZipN (NP :: (k -> Type) -> [k] -> Type) (c :: a -> b -> Constraint) | |
Defined in Data.SOP.NP | |
type Same (NP :: (k1 -> Type) -> [k1] -> Type) | |
type Prod (NP :: (k -> Type) -> [k] -> Type) | |
type UnProd (NP :: (k -> Type) -> [k] -> Type) | |
type SListIN (NP :: (k -> Type) -> [k] -> Type) | |
Defined in Data.SOP.NP | |
type CollapseTo (NP :: (k -> Type) -> [k] -> Type) a | |
Defined in Data.SOP.NP | |
type AllN (NP :: (k -> Type) -> [k] -> Type) (c :: k -> Constraint) | |
Defined in Data.SOP.NP |
The identity type functor.
Like Identity
, but with a shorter name.
Constructors
I a |
Instances
Monad I | |
Functor I | |
Applicative I | |
Foldable I | |
Defined in Data.SOP.BasicFunctors Methods fold :: Monoid m => I m -> m # foldMap :: Monoid m => (a -> m) -> I a -> m # foldMap' :: Monoid m => (a -> m) -> I a -> m # foldr :: (a -> b -> b) -> b -> I a -> b # foldr' :: (a -> b -> b) -> b -> I a -> b # foldl :: (b -> a -> b) -> b -> I a -> b # foldl' :: (b -> a -> b) -> b -> I a -> b # foldr1 :: (a -> a -> a) -> I a -> a # foldl1 :: (a -> a -> a) -> I a -> a # elem :: Eq a => a -> I a -> Bool # maximum :: Ord a => I a -> a # | |
Traversable I | |
Eq1 I | Since: sop-core-0.2.4.0 |
Ord1 I | Since: sop-core-0.2.4.0 |
Defined in Data.SOP.BasicFunctors | |
Read1 I | Since: sop-core-0.2.4.0 |
Defined in Data.SOP.BasicFunctors | |
Show1 I | Since: sop-core-0.2.4.0 |
NFData1 I | Since: sop-core-0.2.5.0 |
Defined in Data.SOP.BasicFunctors | |
Eq a => Eq (I a) | |
Ord a => Ord (I a) | |
Read a => Read (I a) | |
Show a => Show (I a) | |
Generic (I a) | |
Semigroup a => Semigroup (I a) | Since: sop-core-0.4.0.0 |
Monoid a => Monoid (I a) | Since: sop-core-0.4.0.0 |
NFData a => NFData (I a) | Since: sop-core-0.2.5.0 |
Defined in Data.SOP.BasicFunctors | |
type Rep (I a) | |
Defined in Data.SOP.BasicFunctors |
cfoldMap_NP :: forall k c (xs :: [k]) m proxy f. (All c xs, Monoid m) => proxy c -> (forall (a :: k). c a => f a -> m) -> NP f xs -> m #
Specialization of hcfoldMap
.
Since: sop-core-0.3.2.0
"constraints" re-exports
Some useful definitions re-exported the from "constraints" package.
Dict
and (:-)
are GADTs used to capture and transform constraints. Used in the restrictArgs
, restrictEnv
and restrictResult
functions.
This is the type of entailment.
a
is read as :-
ba
"entails" b
.
With this we can actually build a category for Constraint
resolution.
e.g.
Because
is a superclass of Eq
a
, we can show that Ord
a
entails Ord
a
.Eq
a
Because instance
exists, we can show that Ord
a => Ord
[a]
entails Ord
a
as well.Ord
[a]
This relationship is captured in the :-
entailment type here.
Since p
and entailment composes, :-
p:-
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
, 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".Ord
a :-
Eq
[a]
What are the two ways?
Well, we can go from
via the
superclass relationship, and then from Ord
a :-
Eq
a
via the
instance, or we can go from Eq
a :-
Eq
[a]
via the instance
then from Ord
a :-
Ord
[a]
through the superclass relationship
and this diagram by definition must "commute".Ord
[a] :-
Eq
[a]
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.
Instances
Category (:-) | Possible since GHC 7.8, when |
() :=> (Eq (a :- b)) | |
() :=> (Ord (a :- b)) | |
() :=> (Show (a :- b)) | |
a => HasDict b (a :- b) | |
Defined in Data.Constraint | |
Eq (a :- b) | Assumes |
(Typeable p, Typeable q, p, q) => Data (p :- q) | |
Defined in Data.Constraint Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> (p :- q) -> c (p :- q) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (p :- q) # toConstr :: (p :- q) -> Constr # dataTypeOf :: (p :- q) -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (p :- q)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (p :- q)) # gmapT :: (forall b. Data b => b -> b) -> (p :- q) -> p :- q # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (p :- q) -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (p :- q) -> r # gmapQ :: (forall d. Data d => d -> u) -> (p :- q) -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> (p :- q) -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> (p :- q) -> m (p :- q) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (p :- q) -> m (p :- q) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (p :- q) -> m (p :- q) # | |
Ord (a :- b) | Assumes |
Defined in Data.Constraint | |
Show (a :- b) | |
a => NFData (a :- b) | |
Defined in Data.Constraint |
Values of type
capture a dictionary for a constraint of type Dict
pp
.
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.
Instances
HasDict a (Dict a) | |
Defined in Data.Constraint | |
a :=> (Read (Dict a)) | |
a :=> (Monoid (Dict a)) | |
a :=> (Enum (Dict a)) | |
a :=> (Bounded (Dict a)) | |
() :=> (Eq (Dict a)) | |
() :=> (Ord (Dict a)) | |
() :=> (Show (Dict a)) | |
() :=> (Semigroup (Dict a)) | |
a => Bounded (Dict a) | |
a => Enum (Dict a) | |
Defined in Data.Constraint | |
Eq (Dict a) | |
(Typeable p, p) => Data (Dict p) | |
Defined in Data.Constraint Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Dict p -> c (Dict p) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Dict p) # toConstr :: Dict p -> Constr # dataTypeOf :: Dict p -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Dict p)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Dict p)) # gmapT :: (forall b. Data b => b -> b) -> Dict p -> Dict p # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Dict p -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Dict p -> r # gmapQ :: (forall d. Data d => d -> u) -> Dict p -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Dict p -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Dict p -> m (Dict p) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Dict p -> m (Dict p) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Dict p -> m (Dict p) # | |
Ord (Dict a) | |
a => Read (Dict a) | |
Show (Dict a) | |
Semigroup (Dict a) | |
a => Monoid (Dict a) | |
NFData (Dict c) | |
Defined in Data.Constraint |