Capability.Writer

Writer capability

An instance should fulfill the following laws. At this point these laws are not definitive, see https://github.com/haskell/mtl/issues/5.

prop> listen @t (pure a) = pure (a, mempty)

prop> listen @t (tell @t w) = tell @t w >> pure (w, w)

prop> listen @t (m >>= k) = listen @t m >>= \(a, w1) -> listen @t (k a) >>= \(b, w2) -> pure (b, w1 `mappend` w2)

prop> pass @t (tell @t w >> pure (a, f)) = tell @t (f w) >> pure a

prop> writer @t (a, w) = tell @t w >> pure a

A note on the HasSink super class.

HasSink offers one yield method with the same signature as tell. Many people's intuition, however, wouldn't connect the two: yielding tosses the value down some black-box chute, while telling grows and accumulation via the monoid. The connection is since the chute is opaque, the tosser cannot rule out there being such an accumulation at the chutes other end.

Formally, we reach the same conclusion. HasSink has no laws, indicating the user can make no assumptions beyond the signature of yield. HasWriter, with tell defined as yield, is thus always compatable regardless of whatever additional methods it provides and laws by which it abides.

writer @tag (a, w) lifts a pure writer action (a, w) to a monadic action in an arbitrary monad m with capability HasWriter.

Appends w to the output of the writer capability tag and returns the value a.

tell @tag w appends w to the output of the writer capability tag.

listen @tag m executes the action m and returns the output of m in the writer capability tag along with result of m. Appends the output of m to the output of the writer capability tag.

pass @tag m executes the action m. Assuming m returns (a, f) and appends w to the output of the writer capability tag. pass @tag m instead appends w' = f w to the output and returns a.

censor @tag f m is an action that executes the action m and applies the function f to the output of the writer capability tag, leaving the return value unchanged.

Type synonym using the TypeOf type family to specify HasWriter constraints without having to specify the type associated to a tag.

Type family associating a tag to the corresponding type. It is intended to simplify constraint declarations, by removing the need to redundantly specify the type associated to a tag.

It is poly-kinded, which allows users to define their own kind of tags. Standard haskell types can also be used as tags by specifying the Type kind when defining the type family instance.

Defining TypeOf instances for GHC.TypeLits.Symbols (typelevel string literals) is discouraged. Since symbols all belong to the same global namespace, such instances could conflict with others defined in external libraries. More generally, as for typeclasses, TypeOf instances should always be defined in the same module as the tag type to prevent issues due to orphan instances.

Example:

    import Capability.Reader

    data Foo
    data Bar
    type instance TypeOf Type Foo = Int
    type instance TypeOf Type Bar = String

    -- Same as: foo :: HasReader Foo Int M => …
    foo :: HasReader' Foo m => …
    foo = …

Accumulate sunk values with their own monoid.

Reified tag capability m

Defines the dictionary type for the methods of capability under tag in the monad m. Refer to interpret_ for an example use-case.

For example, the Capability.Sink.HasSink capability has the method Capability.Sink.yield :: a -> m (). The corresponding dictionary type is defined as follows.

>>> :{  data instance Reified tag (HasSink tag a) m =    ReifiedSink { _yield :: forall a. a -> m () }  :}

Superclass dictionaries are represented as nested records. For example, the Capability.State.HasState capability has the superclasses Capability.Source.HasSource and Capability.Sink.HasSink and the method Capability.State.state :: (s -> (a, s)) -> m a. The corresponding dictionary type is defined as follows.

>>> :{  data instance Reified tag (HasState tag s) m =    ReifiedState      { _stateSource :: Reified tag (HasSource tag s) m,        _stateSink :: Reified tag (HasSink tag s) m,        _state :: forall a. (s -> (a, s)) -> m a      }  :}