Safe Haskell	None
Language	Haskell2010

Polysemy.ConstraintAbsorber

Contents

Absorb builder
Re-exports

Synopsis

absorbWithSem :: forall (p :: (Type -> Type) -> Constraint) (x :: (Type -> Type) -> Type -> Type -> Type) d r a. d -> (forall s. Reifies s d :- p (x (Sem r) s)) -> (p (Sem r) => Sem r a) -> Sem r a
class Reifies (s :: k) a | s -> a
newtype a :- b = Sub (a -> Dict b)
data Dict a where
- Dict :: forall a. a => Dict a
reflect :: Reifies s a => proxy s -> a
data Proxy (t :: k) :: forall k. k -> Type = Proxy

Absorb builder

absorbWithSem Source #

Arguments

:: forall (p :: (Type -> Type) -> Constraint) (x :: (Type -> Type) -> Type -> Type -> Type). d	Reified dictionary
-> (forall s. Reifies s d :- p (x (Sem r) s))	This parameter should always be `Sub Dict`
-> (p (Sem r) => Sem r a)
-> Sem r a

This function can be used to locally introduce typeclass instances for Sem. See MonadState for an example of how to use it.

Since: 0.3.0.0

Re-exports

class Reifies (s :: k) a | s -> a #

Minimal complete definition

reflect

Instances

KnownNat n => Reifies (n :: Nat) Integer
Instance details Defined in Data.Reflection Methods reflect :: proxy n -> Integer #
KnownSymbol n => Reifies (n :: Symbol) String
Instance details Defined in Data.Reflection Methods reflect :: proxy n -> String #
Reifies Z Int
Instance details Defined in Data.Reflection Methods reflect :: proxy Z -> Int #
Reifies n Int => Reifies (D n :: Type) Int
Instance details Defined in Data.Reflection Methods reflect :: proxy (D n) -> Int #
Reifies n Int => Reifies (SD n :: Type) Int
Instance details Defined in Data.Reflection Methods reflect :: proxy (SD n) -> Int #
Reifies n Int => Reifies (PD n :: Type) Int
Instance details Defined in Data.Reflection Methods reflect :: proxy (PD n) -> Int #
(B b0, B b1, B b2, B b3, B b4, B b5, B b6, B b7, w0 ~ W b0 b1 b2 b3, w1 ~ W b4 b5 b6 b7) => Reifies (Stable w0 w1 a :: Type) a
Instance details Defined in Data.Reflection Methods reflect :: proxy (Stable w0 w1 a) -> a #

newtype a :- b infixr 9 #

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.

Constructors

Sub (a -> Dict b)

Instances

Category (:-)	Possible since GHC 7.8, when `Category` was made polykinded.
Instance details Defined in Data.Constraint Methods id :: a :- a # (.) :: (b :- c) -> (a :- b) -> a :- c #
() :=> (Eq (a :- b))
Instance details Defined in Data.Constraint Methods ins :: () :- Eq (a :- b) #
() :=> (Ord (a :- b))
Instance details Defined in Data.Constraint Methods ins :: () :- Ord (a :- b) #
() :=> (Show (a :- b))
Instance details Defined in Data.Constraint Methods ins :: () :- Show (a :- b) #
Eq (a :- b)	Assumes `IncoherentInstances` doesn't exist.
Instance details Defined in Data.Constraint Methods (==) :: (a :- b) -> (a :- b) -> Bool # (/=) :: (a :- b) -> (a :- b) -> Bool #
(Typeable p, Typeable q, p, q) => Data (p :- q)
Instance details 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 :: (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 `IncoherentInstances` doesn't exist.
Instance details Defined in Data.Constraint Methods compare :: (a :- b) -> (a :- b) -> Ordering # (<) :: (a :- b) -> (a :- b) -> Bool # (<=) :: (a :- b) -> (a :- b) -> Bool # (>) :: (a :- b) -> (a :- b) -> Bool # (>=) :: (a :- b) -> (a :- b) -> Bool # max :: (a :- b) -> (a :- b) -> a :- b # min :: (a :- b) -> (a :- b) -> a :- b #
Show (a :- b)
Instance details Defined in Data.Constraint Methods showsPrec :: Int -> (a :- b) -> ShowS # show :: (a :- b) -> String # showList :: [a :- b] -> ShowS #
a => NFData (a :- b)
Instance details Defined in Data.Constraint Methods rnf :: (a :- b) -> () #

data Dict a where #

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.

Constructors

Dict :: forall a. a => Dict a

Instances

a :=> (Read (Dict a))
Instance details Defined in Data.Constraint Methods ins :: a :- Read (Dict a) #
a :=> (Monoid (Dict a))
Instance details Defined in Data.Constraint Methods ins :: a :- Monoid (Dict a) #
a :=> (Enum (Dict a))
Instance details Defined in Data.Constraint Methods ins :: a :- Enum (Dict a) #
a :=> (Bounded (Dict a))
Instance details Defined in Data.Constraint Methods ins :: a :- Bounded (Dict a) #
() :=> (Eq (Dict a))
Instance details Defined in Data.Constraint Methods ins :: () :- Eq (Dict a) #
() :=> (Ord (Dict a))
Instance details Defined in Data.Constraint Methods ins :: () :- Ord (Dict a) #
() :=> (Show (Dict a))
Instance details Defined in Data.Constraint Methods ins :: () :- Show (Dict a) #
() :=> (Semigroup (Dict a))
Instance details Defined in Data.Constraint Methods ins :: () :- Semigroup (Dict a) #
a => Bounded (Dict a)
Instance details Defined in Data.Constraint Methods minBound :: Dict a # maxBound :: Dict a #
a => Enum (Dict a)
Instance details Defined in Data.Constraint Methods succ :: Dict a -> Dict a # pred :: Dict a -> Dict a # toEnum :: Int -> Dict a # fromEnum :: Dict a -> Int # enumFrom :: Dict a -> [Dict a] # enumFromThen :: Dict a -> Dict a -> [Dict a] # enumFromTo :: Dict a -> Dict a -> [Dict a] # enumFromThenTo :: Dict a -> Dict a -> Dict a -> [Dict a] #
Eq (Dict a)
Instance details Defined in Data.Constraint Methods (==) :: Dict a -> Dict a -> Bool # (/=) :: Dict a -> Dict a -> Bool #
(Typeable p, p) => Data (Dict p)
Instance details 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 :: (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)
Instance details Defined in Data.Constraint Methods compare :: Dict a -> Dict a -> Ordering # (<) :: Dict a -> Dict a -> Bool # (<=) :: Dict a -> Dict a -> Bool # (>) :: Dict a -> Dict a -> Bool # (>=) :: Dict a -> Dict a -> Bool # max :: Dict a -> Dict a -> Dict a # min :: Dict a -> Dict a -> Dict a #
a => Read (Dict a)
Instance details Defined in Data.Constraint Methods readsPrec :: Int -> ReadS (Dict a) # readList :: ReadS [Dict a] # readPrec :: ReadPrec (Dict a) # readListPrec :: ReadPrec [Dict a] #
Show (Dict a)
Instance details Defined in Data.Constraint Methods showsPrec :: Int -> Dict a -> ShowS # show :: Dict a -> String # showList :: [Dict a] -> ShowS #
Semigroup (Dict a)
Instance details Defined in Data.Constraint Methods (<>) :: Dict a -> Dict a -> Dict a # sconcat :: NonEmpty (Dict a) -> Dict a # stimes :: Integral b => b -> Dict a -> Dict a #
a => Monoid (Dict a)
Instance details Defined in Data.Constraint Methods mempty :: Dict a # mappend :: Dict a -> Dict a -> Dict a # mconcat :: [Dict a] -> Dict a #
NFData (Dict c)
Instance details Defined in Data.Constraint Methods rnf :: Dict c -> () #

reflect :: Reifies s a => proxy s -> a #

Recover a value inside a reify context, given a proxy for its reified type.

data Proxy (t :: k) :: forall k. k -> Type #

Proxy is a type that holds no data, but has a phantom parameter of arbitrary type (or even kind). Its use is to provide type information, even though there is no value available of that type (or it may be too costly to create one).

Historically, Proxy :: Proxy a is a safer alternative to the 'undefined :: a' idiom.

>>> Proxy :: Proxy (Void, Int -> Int)
Proxy

Proxy can even hold types of higher kinds,

>>> Proxy :: Proxy Either
Proxy

>>> Proxy :: Proxy Functor
Proxy

>>> Proxy :: Proxy complicatedStructure
Proxy

Constructors

Proxy

Instances

Generic1 (Proxy :: k -> Type)
Instance details Defined in GHC.Generics Associated Types type Rep1 Proxy :: k -> Type # Methods from1 :: Proxy a -> Rep1 Proxy a # to1 :: Rep1 Proxy a -> Proxy a #
Monad (Proxy :: Type -> Type)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods (>>=) :: Proxy a -> (a -> Proxy b) -> Proxy b # (>>) :: Proxy a -> Proxy b -> Proxy b # return :: a -> Proxy a # fail :: String -> Proxy a #
Functor (Proxy :: Type -> Type)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods fmap :: (a -> b) -> Proxy a -> Proxy b # (<$) :: a -> Proxy b -> Proxy a #
Applicative (Proxy :: Type -> Type)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods pure :: a -> Proxy a # (<>) :: Proxy (a -> b) -> Proxy a -> Proxy b # liftA2 :: (a -> b -> c) -> Proxy a -> Proxy b -> Proxy c # (>) :: Proxy a -> Proxy b -> Proxy b # (<*) :: Proxy a -> Proxy b -> Proxy a #
Foldable (Proxy :: Type -> Type)	Since: base-4.7.0.0
Instance details Defined in Data.Foldable Methods fold :: Monoid m => Proxy m -> m # foldMap :: Monoid m => (a -> m) -> Proxy a -> m # foldr :: (a -> b -> b) -> b -> Proxy a -> b # foldr' :: (a -> b -> b) -> b -> Proxy a -> b # foldl :: (b -> a -> b) -> b -> Proxy a -> b # foldl' :: (b -> a -> b) -> b -> Proxy a -> b # foldr1 :: (a -> a -> a) -> Proxy a -> a # foldl1 :: (a -> a -> a) -> Proxy a -> a # toList :: Proxy a -> [a] # null :: Proxy a -> Bool # length :: Proxy a -> Int # elem :: Eq a => a -> Proxy a -> Bool # maximum :: Ord a => Proxy a -> a # minimum :: Ord a => Proxy a -> a # sum :: Num a => Proxy a -> a # product :: Num a => Proxy a -> a #
Traversable (Proxy :: Type -> Type)	Since: base-4.7.0.0
Instance details Defined in Data.Traversable Methods traverse :: Applicative f => (a -> f b) -> Proxy a -> f (Proxy b) # sequenceA :: Applicative f => Proxy (f a) -> f (Proxy a) # mapM :: Monad m => (a -> m b) -> Proxy a -> m (Proxy b) # sequence :: Monad m => Proxy (m a) -> m (Proxy a) #
Alternative (Proxy :: Type -> Type)	Since: base-4.9.0.0
Instance details Defined in Data.Proxy Methods empty :: Proxy a # (<\|>) :: Proxy a -> Proxy a -> Proxy a # some :: Proxy a -> Proxy [a] # many :: Proxy a -> Proxy [a] #
MonadPlus (Proxy :: Type -> Type)	Since: base-4.9.0.0
Instance details Defined in Data.Proxy Methods mzero :: Proxy a # mplus :: Proxy a -> Proxy a -> Proxy a #
Bounded (Proxy t)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods minBound :: Proxy t # maxBound :: Proxy t #
Enum (Proxy s)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods succ :: Proxy s -> Proxy s # pred :: Proxy s -> Proxy s # toEnum :: Int -> Proxy s # fromEnum :: Proxy s -> Int # enumFrom :: Proxy s -> [Proxy s] # enumFromThen :: Proxy s -> Proxy s -> [Proxy s] # enumFromTo :: Proxy s -> Proxy s -> [Proxy s] # enumFromThenTo :: Proxy s -> Proxy s -> Proxy s -> [Proxy s] #
Eq (Proxy s)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods (==) :: Proxy s -> Proxy s -> Bool # (/=) :: Proxy s -> Proxy s -> Bool #
Ord (Proxy s)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods compare :: Proxy s -> Proxy s -> Ordering # (<) :: Proxy s -> Proxy s -> Bool # (<=) :: Proxy s -> Proxy s -> Bool # (>) :: Proxy s -> Proxy s -> Bool # (>=) :: Proxy s -> Proxy s -> Bool # max :: Proxy s -> Proxy s -> Proxy s # min :: Proxy s -> Proxy s -> Proxy s #
Read (Proxy t)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods readsPrec :: Int -> ReadS (Proxy t) # readList :: ReadS [Proxy t] # readPrec :: ReadPrec (Proxy t) # readListPrec :: ReadPrec [Proxy t] #
Show (Proxy s)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods showsPrec :: Int -> Proxy s -> ShowS # show :: Proxy s -> String # showList :: [Proxy s] -> ShowS #
Ix (Proxy s)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods range :: (Proxy s, Proxy s) -> [Proxy s] # index :: (Proxy s, Proxy s) -> Proxy s -> Int # unsafeIndex :: (Proxy s, Proxy s) -> Proxy s -> Int inRange :: (Proxy s, Proxy s) -> Proxy s -> Bool # rangeSize :: (Proxy s, Proxy s) -> Int # unsafeRangeSize :: (Proxy s, Proxy s) -> Int
Generic (Proxy t)
Instance details Defined in GHC.Generics Associated Types type Rep (Proxy t) :: Type -> Type # Methods from :: Proxy t -> Rep (Proxy t) x # to :: Rep (Proxy t) x -> Proxy t #
Semigroup (Proxy s)	Since: base-4.9.0.0
Instance details Defined in Data.Proxy Methods (<>) :: Proxy s -> Proxy s -> Proxy s # sconcat :: NonEmpty (Proxy s) -> Proxy s # stimes :: Integral b => b -> Proxy s -> Proxy s #
Monoid (Proxy s)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods mempty :: Proxy s # mappend :: Proxy s -> Proxy s -> Proxy s # mconcat :: [Proxy s] -> Proxy s #
type Rep1 (Proxy :: k -> Type)	Since: base-4.6.0.0
Instance details Defined in GHC.Generics type Rep1 (Proxy :: k -> Type) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) (U1 :: k -> Type))
type Rep (Proxy t)	Since: base-4.6.0.0
Instance details Defined in GHC.Generics type Rep (Proxy t) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) (U1 :: Type -> Type))