Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

The "reader" monad

Tags:

haskell

monads

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.

  1. Does anybody have any idea what this dual structure might be?
  2. Has anybody written this monad? Is there a well-known name for it?
like image 432
MathematicalOrchid Avatar asked Mar 14 '13 19:03

MathematicalOrchid


People also ask

What is the reader Monad?

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.

What is Writer 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.

Is either a Monad Haskell?

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 .

What does LIFT do in Haskell?

Lifting is a concept which allows you to transform a function into a corresponding function within another (usually more general) setting.


1 Answers

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.

like image 114
Philip JF Avatar answered Sep 29 '22 23:09

Philip JF