0 | module Control.Comonad
  1 |
  2 | import Control.Monad.Identity
  3 |
  4 | import Data.List1
  5 | import Data.Morphisms
  6 | import Data.Stream
  7 |
  8 | %default total
  9 |
 10 | --------------------------------------------------------------------------------
 11 | --          Comonad
 12 | --------------------------------------------------------------------------------
 13 |
 14 | public export
 15 | interface Functor w => Comonad w where
 16 |   extract   : w a -> a
 17 |
 18 |   duplicate : w a -> w (w a)
 19 |   duplicate = extend id
 20 |
 21 |   extend    : (w a -> b) -> w a -> w b
 22 |   extend f = map f . duplicate
 23 |
 24 | --------------------------------------------------------------------------------
 25 | --          Comonad Implementations
 26 | --------------------------------------------------------------------------------
 27 |
 28 | public export
 29 | Comonad (Pair e) where
 30 |   extract         = snd
 31 |   duplicate (e,a) = (e, (e, a))
 32 |
 33 | public export
 34 | Comonad Identity where
 35 |   extract   = runIdentity
 36 |   duplicate = Id
 37 |
 38 | public export
 39 | Comonad Stream where
 40 |   extract               = head
 41 |   duplicate xs@(_ :: t) = xs :: duplicate t
 42 |
 43 | public export
 44 | Comonad List1 where
 45 |   extract = head
 46 |   duplicate (x ::: xs) = (x ::: xs) ::: tails xs
 47 |
 48 |     where
 49 |       tails : List a -> List (List1 a)
 50 |       tails []        = []
 51 |       tails (x :: xs) = (x ::: xs) :: tails xs
 52 |
 53 | public export
 54 | Monoid e => Comonad (Morphism e) where
 55 |   extract   (Mor f) = f neutral
 56 |   duplicate (Mor f) = Mor $ \e => Mor (\e' => f (e <+> e'))
 57 |
 58 | --------------------------------------------------------------------------------
 59 | --          ComonadApply
 60 | --------------------------------------------------------------------------------
 61 |
 62 | export infixl 4 <@, @>, <@@>, <@>
 63 |
 64 | public export
 65 | interface Comonad w => ComonadApply w where
 66 |   (<@>) : w (a -> b) -> w a -> w b
 67 |
 68 |   (@>)  : w a -> w b -> w b
 69 |   (@>) = flip (<@)
 70 |
 71 |   (<@) : w a -> w b -> w a
 72 |   a <@ b = map const a <@> b
 73 |
 74 | --------------------------------------------------------------------------------
 75 | --          ComonadApply Implementations
 76 | --------------------------------------------------------------------------------
 77 |
 78 | public export
 79 | Semigroup m => ComonadApply (Pair m) where
 80 |   (m, f) <@> (n, a) = (m <+> n, f a)
 81 |   (m, a) <@  (n, _) = (m <+> n, a)
 82 |   (m, _)  @> (n, b) = (m <+> n, b)
 83 |
 84 | public export
 85 | ComonadApply List1 where
 86 |   (<@>) = (<*>)
 87 |
 88 | public export
 89 | ComonadApply Stream where
 90 |   (<@>) = (<*>)
 91 |
 92 | public export
 93 | Monoid m => ComonadApply (Morphism m) where
 94 |   (<@>) = (<*>)
 95 |
 96 | public export
 97 | ComonadApply Identity where
 98 |   (<@>) = (<*>)
 99 |   _ @> b = b
100 |   b <@ _ = b
101 |
102 | --------------------------------------------------------------------------------
103 | --          Utilities
104 | --------------------------------------------------------------------------------
105 |
106 | export infixl 1 =>>
107 | export infixr 1 <<=, =<=, =>=
108 |
109 | ||| `extend` with the arguments swapped. Dual to `>>=` for a `Monad`.
110 | public export %inline
111 | (=>>) : Comonad w => w a -> (w a -> b) -> w b
112 | (=>>) = flip extend
113 |
114 | ||| `extend` in operator form
115 | public export %inline
116 | (<<=) : Comonad w => (w a -> b) -> w a -> w b
117 | (<<=) = extend
118 |
119 | ||| Right-to-left `Cokleisli` composition
120 | public export %inline
121 | (=<=) : Comonad w => (w b -> c) -> (w a -> b) -> w a -> c
122 | f =<= g = f . extend g
123 |
124 | ||| Left-to-right `Cokleisli` composition
125 | public export %inline
126 | (=>=) : Comonad w => (w a -> b) -> (w b -> c) -> w a -> c
127 | f =>= g = g . extend f
128 |
129 | ||| Flipped version of `<@>`.
130 | public export %inline
131 | (<@@>) : ComonadApply w => w a -> w (a -> b) -> w b
132 | (<@@>) = flip (<@>)
133 |