OK, so the writer monad allows you to write stuff to [usually] some kind of container, and get that container back at the end. In most implementations, the "container" can actually be any monoid.
Now, there is also a "reader" monad. This, you might think, would offer the dual operation - incrementally reading from some kind of container, one item at a time. In fact, this is not the functionality that the usual reader monad provides. (Instead, it merely offers easy access to a semi-global constant.)
To actually write a monad which is dual to the usual writer monad, we would need some kind of structure which is dual to a monoid.
The Reader monad (also called the Environment monad). Represents a computation, which can read values from a shared environment, pass values from function to function, and execute sub-computations in a modified environment. Using Reader monad for such computations is often clearer and easier than using the State monad.
The Writer monad is a programming design pattern which makes it possible to compose functions which return their result values paired with a log string. The final result of a composed function yields both a value, and a concatenation of the logs from each component function application.
Strictly speaking, Either cannot be a monad, as it has kind Type -> Type -> Type ; Either String can be (and is), because it has kind Type -> Type .
Lifting is a concept which allows you to transform a function into a corresponding function within another (usually more general) setting.
The dual of a monoid is a comonoid. Recall that a monoid is defined as (something isomorphic to)
class Monoid m where
create :: () -> m
combine :: (m,m) -> m
with these laws
combine (create (),x) = x
combine (x,create ()) = x
combine (combine (x,y),z) = combine (x,combine (y,z))
thus
class Comonoid m where
delete :: m -> ()
split :: m -> (m,m)
some standard operations are needed
first :: (a -> b) -> (a,c) -> (b,c)
second :: (c -> d) -> (a,c) -> (a,d)
idL :: ((),x) -> x
idR :: (x,()) -> x
assoc :: ((x,y),z) -> (x,(y,z))
with laws like
idL $ first delete $ (split x) = x
idR $ second delete $ (split x) = x
assoc $ first split (split x) = second split (split x)
This typeclass looks weird for a reason. It has an instance
instance Comonoid m where
split x = (x,x)
delete x = ()
in Haskell, this is the only instance. We can recast reader as the exact dual of writer, but since there is only one instance for comonoid, we get something isomorphic to the standard reader type.
Having all types be comonoids is what makes the category "Cartesian" in "Cartesian Closed Category." "Monoidal Closed Categories" are like CCCs but without this property, and are related to substructural type systems. Part of the appeal of linear logic is the increased symmetry that this is an example of. While, having substructural types allows you to define comonoids with more interesting properties (supporting things like resource management). In fact, this provides a framework for understand the role of copy constructors and destructors in C++ (although C++ does not enforce the important properties because of the existence of pointers).
EDIT: Reader from comonoids
newtype Reader r x = Reader {runReader :: r -> x}
forget :: Comonoid m => (m,a) -> a
forget = idL . first delete
instance Comonoid r => Monad (Reader r) where
return x = Reader $ \r -> forget (r,x)
m >>= f = \r -> let (r1,r2) = split r in runReader (f (runReader m r1)) r2
ask :: Comonoid r => Reader r r
ask = Reader id
note that in the above code every variable is used exactly once after binding (so these would all type with linear types). The monad law proofs are trivial, and only require the comonoid laws to work. Hence, Reader
really is dual to Writer
.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With