Control.Comonad

Module providing comonads for idris.

liftW : Comonad w => (f : a -> b) -> w a -> w b

Lift a function into a function on comonadic values.

extend : Comonad w => (w a -> b) -> w a -> w b

interface Comonad 

A comonad is the categorical dual of a monad. It must satisfy the following
laws:

extend extract      = id
extract . extend f  = f
extend f . extend g = extend (f . extend g)

extract : Comonad w => w a -> a

duplicate : Comonad w => w a -> w (w a)

interface CoApplicative 

CoApplicatives provide a categorical approach to zippers. They must satisfy
the following laws:

(.) <$> u <@> v <@> w = u <@> (v <@> w)
extract (p <@> q) = extract p (extract q)
duplicate (p <@> q) = (<@>) <$> duplicate p <@> duplicate q

If 'w' is an applicative functor, it must further satisfy

(<@>) = (<*>)

(<@>) : CoApplicative w => w (a -> b) -> w a -> w b

Fixity

Left associative, precedence 4

(@>) : CoApplicative w => w a -> w b -> w b

Fixity

Left associative, precedence 4

(<@) : CoApplicative w => w a -> w b -> w a

Fixity

Left associative, precedence 4

(=>>) : Comonad w => w a -> (w a -> b) -> w b

Dual to '>>='

Fixity

Left associative, precedence 1

(=>=) : Comonad w => (w a -> b) -> (w b -> c) -> w a -> c

Left-to-right cokliesli composition

Fixity

Left associative, precedence 1

(=<=) : Comonad w => (w b -> c) -> (w a -> b) -> w a -> c

Right-to-left cokliesli composition

Fixity

Left associative, precedence 1

(<<=) : Comonad w => (w a -> b) -> w a -> w b

Operator giving us 'extend'

Fixity

Left associative, precedence 1