
   0 | module Stellar.API.Morphism
   1 | 
   2 | import Stellar.API.Definition
   3 | import Stellar.API.Monoid
   4 | import public Stellar.Ops
   5 | 
   6 | import public Data.Sigma
   7 | import Data.Coproduct
   8 | import Data.Product
   9 | 
  10 | import Control.Relation
  11 | import Control.Category
  12 | import Control.Order
  13 | import Control.Comonad
  14 | 
  15 | import Debug.Trace
  16 | 
  17 | -- Closed API morphism
  18 | public export
  19 | record (=&>) (a, b : API) where
  20 |   constructor (!!)
  21 |   continuation : (x : a.message) -> Σ b.message (\y => b.response y -> a.response x)
  22 | 
  23 | export
  24 | (.fwd) : a =&> b -> a.message -> b.message
  25 | (.fwd) m x = (m.continuation x).π1
  26 | 
  27 | %unbound_implicits on
  28 | ----------------------------------------------------------------------------------
  29 | -- APIs form a category
  30 | ----------------------------------------------------------------------------------
  31 | 
  32 | ||| Identity of container morphisms
  33 | public export
  34 | identity : a =&> a
  35 | identity = !! \x => x ## id
  36 | 
  37 | ||| Composition of container morphisms
  38 | public export
  39 | (|&>) : a =&> b -> b =&> c -> a =&> c
  40 | (|&>) x y = !! \v =>
  41 |               let v1 ## v2 = x.continuation v
  42 |                   w1 ## w2 = y.continuation v1
  43 |               in w1 ## v2 . w2
  44 | 
  45 | ----------------------------------------------------------------------------------
  46 | -- API morphisms form a preorder
  47 | ----------------------------------------------------------------------------------
  48 | public export
  49 | Reflexive API (=&>) where
  50 |   reflexive = identity
  51 | 
  52 | public export
  53 | Transitive API (=&>) where
  54 |   transitive = (|&>)
  55 | 
  56 | public export
  57 | Preorder API (=&>) where
  58 | 
  59 | ----------------------------------------------------------------------------------
  60 | -- API morphisms form a category
  61 | ----------------------------------------------------------------------------------
  62 | public export
  63 | Category (=&>) where
  64 |   id = identity
  65 |   (.) = flip (|&>)
  66 | 
  67 | ----------------------------------------------------------------------------------
  68 | -- Ex is actually a Bifunctor
  69 | ----------------------------------------------------------------------------------
  70 | 
  71 | export
  72 | bimapEx : a =&> b -> (t -> s) -> Ex a t -> Ex b s
  73 | bimapEx m f (MkEx x y) =
  74 |   let v1 ## v2 = m.continuation x
  75 |   in MkEx v1 (f . y . v2)
  76 | 
  77 | ----------------------------------------------------------------------------------
  78 | -- Some bifunctors over containers
  79 | ----------------------------------------------------------------------------------
  80 | 
  81 | ||| Tensor is a bifunctor.
  82 | public export
  83 | parallel : c1 =&> c2 -> c3 =&> c4 -> (c1 // c3) =&> (c2 // c4)
  84 | parallel m1 m2 =
  85 |   !! \x => let v1 ## v2 = m1.continuation x.π1
  86 |                w1 ## w2 = m2.continuation x.π2
  87 |             in (v1 && w1) ## bimap v2 w2
  88 | 
  89 | ||| Dirichlet is a bifunctor.
  90 | public export
  91 | concurrent : c1 =&> c2 -> c3 =&> c4 -> (c1 * c3) =&> (c2 * c4)
  92 | concurrent m1 m2 =
  93 |   !! \x => let v1 ## v2 = m1.continuation x.π1
  94 |                w1 ## w2 = m2.continuation x.π2
  95 |             in (v1 && w1) ## bimap v2 w2
  96 | 
  97 | ||| Sequence is a bifunctor
  98 | ||| /!\ This calls the continuation of `m2` twice /!\
  99 | public export
 100 | biSequence :
 101 |   (m1 : a =&> b) -> (m2 : a' =&> b') ->
 102 |   a &> a' =&> b &> b'
 103 | biSequence m1 m2 =
 104 |   !! \x => let v1 ## v2 = m1.continuation x.req
 105 |             in MkEx v1 (\xs => π1 (m2.continuation (x.cont (v2 xs))) )
 106 |             ## \(y1 ## y2) => v2 y1 ## (π2 (m2.continuation (x.cont (v2 y1)))) y2
 107 | 
 108 | ||| + is a bifunctor.
 109 | export
 110 | choice : c1 =&> c2 -> c3 =&> c4 -> (c1 + c3) =&> (c2 + c4)
 111 | choice m1 m2 =
 112 |   !! \case (<+ x) => let v1 ## v2 = m1.continuation x
 113 |              in <+ v1 ## v2
 114 |            (+> x) => let v1 ## v2 = m2.continuation x
 115 |              in +> v1 ## v2
 116 | 
 117 | ----------------------------------------------------------------------------------
 118 | -- Properties about monoidal products
 119 | ----------------------------------------------------------------------------------
 120 | 
 121 | ||| Swap tensors
 122 | public export
 123 | swap : (a // b) =&> (b // a)
 124 | swap = !! \x => swap x ## swap
 125 | 
 126 | ||| Swap dirichelet
 127 | public export
 128 | swap' : (x * y) =&> (y * x)
 129 | swap' = !! \x => swap x ## Coproduct.swap
 130 | 
 131 | ||| Diagonal on coproduct
 132 | public export
 133 | dia : a + a =&> a
 134 | dia = !! \case (<+ x) => x ## id
 135 |                (+> x) => x ## id
 136 | 
 137 | ||| Diagonal on coproduct
 138 | public export
 139 | dia3 : a + a + a =&> a
 140 | dia3 = choice dia identity |&> dia
 141 | 
 142 | public export
 143 | inl : a =&> a + b
 144 | inl = !! \x => <+ x ## id
 145 | 
 146 | public export
 147 | inr : b =&> a + b
 148 | inr = !! \x => +> x ## id
 149 | 
 150 | export
 151 | elimChoice : a =&> c -> b =&> c -> a + b =&> c
 152 | elimChoice l r =
 153 |   !! \case (<+ x) => l.continuation x
 154 |            (+> x) => r.continuation x
 155 | 
 156 | ||| End is the neutral for //
 157 | public export
 158 | pairLUnit : End // a =&> a
 159 | pairLUnit = !! \x => x.π2 ## (() &&)
 160 | 
 161 | ||| End is the neutral for //
 162 | public export
 163 | pairRUnit : a // End =&> a
 164 | pairRUnit = !! \x => x.π1 ## (&& ())
 165 | 
 166 | ||| Extract the left value
 167 | public export
 168 | left : a + Void -> a
 169 | left (<+ x) = x
 170 | 
 171 | ||| Extract the right value
 172 | public export
 173 | right : Void + b -> b
 174 | right (+> x) = x
 175 | 
 176 | ||| End is the neutral for //
 177 | public export
 178 | sumLUnit : Never + a =&> a
 179 | sumLUnit = !! \(+> x) => x ## id
 180 | 
 181 | ||| End is the neutral for //
 182 | public export
 183 | sumRUnit : a + Never =&> a
 184 | sumRUnit = !! \(<+ x) => x ## id
 185 | 
 186 | ||| End is the neutral for &>
 187 | public export
 188 | compLUnit : End &> c =&> c
 189 | compLUnit = !! \x => x.cont () ## (() ##)
 190 | 
 191 | ||| End is the neutral for &>
 192 | public export
 193 | compRUnit : c &> End =&> c
 194 | compRUnit = !! \x => x.req ## (## ())
 195 | 
 196 | public export
 197 | comp2Unit : a =&> End -> b =&> End -> a &> b =&> End
 198 | comp2Unit m1 m2 = biSequence m1 m2 |&> compLUnit
 199 | 
 200 | ----------------------------------------------------------------------------------
 201 | -- State, Costate, and Contexts
 202 | ----------------------------------------------------------------------------------
 203 | 
 204 | ||| State x is the same a 1 =&> x
 205 | public export
 206 | State : API -> Type
 207 | State = (End =&>)
 208 | 
 209 | ||| Build a state from a value.
 210 | public export
 211 | state : a.message -> State a
 212 | state msg = !! \x => msg ## const ()
 213 | 
 214 | ||| Costate x is the same a x =&> 1
 215 | public export
 216 | Costate : API -> Type
 217 | Costate = (=&> End)
 218 | 
 219 | ||| Build a costate from a continuation.
 220 | public export
 221 | costate : ((x : a.message) -> a.response x) -> Costate a
 222 | costate f = !! \x => () ## const (f x)
 223 | 
 224 | ||| Extract the continuation from a costate
 225 | public export
 226 | extract : Costate a -> (x : a.message) -> a.response x
 227 | extract y x = π2 (y.continuation x) ()
 228 | 
 229 | ||| Extract the continuation from a costate
 230 | public export
 231 | runCostate : Costate a -> (x : a.message) -> a.response x
 232 | runCostate y x = π2 (y.continuation x) ()
 233 | 
 234 | ||| Obtain the value from a state.
 235 | public export
 236 | (.getVal) : State a -> a.message
 237 | x.getVal = π1 (x.continuation ())
 238 | 
 239 | ||| A context is both a State and a Costate.
 240 | public export
 241 | 0 Context : (a, b : API) -> Type
 242 | Context a b = Pair (State a) (Costate b)
 243 | 
 244 | ----------------------------------------------------------------------------------
 245 | -- Properties around Lifts
 246 | ----------------------------------------------------------------------------------
 247 | 
 248 | public export
 249 | map_Lift : Functor f => a =&> b -> Lift f a =&> Lift f b
 250 | map_Lift c = !! \x => let v1 ## v2 = c.continuation x in v1 ## map v2
 251 | 
 252 | ||| Given a monad m we get a counit.
 253 | public export
 254 | counit : Monad m => Lift m a =&> a
 255 | counit = !! \x => x ## pure
 256 | 
 257 | ||| Given a monad m we get a comulitiplication.
 258 | public export
 259 | comult : Monad m => Lift m a =&> Lift m (Lift m a)
 260 | comult = !! \x => x ## join
 261 | 
 262 | export
 263 | coKleisli : Monad m => Lift m a =&> b -> Lift m b =&> c -> Lift m a =&> c
 264 | coKleisli m1 m2 = comult |&> map_Lift m1 |&> m2
 265 | 
 266 | ||| Given a comonad we get a pure, or unit
 267 | public export
 268 | pure : Comonad m => a =&> m $- a
 269 | pure = !! \x => x ## extract
 270 | 
 271 | ||| Given a comonad we get a join
 272 | public export
 273 | join : Comonad m => m $- m $- a =&> m $- a
 274 | join = !! \x => x ## comult
 275 | 
 276 | ||| Coproduct distributes over Lifts.
 277 | public export
 278 | distrib_plus : Lift f (a + b) =&> Lift f a + Lift f b
 279 | distrib_plus =
 280 |   !! \case (<+ x) => <+ x ## id
 281 |            (+> x) => +> x ## id
 282 | 
 283 | ||| Coproduct distributes over Lifts.
 284 | public export
 285 | distrib_plus_3 : Lift f (a + b + c) =&> Lift f a + Lift f b + Lift f c
 286 | distrib_plus_3 =
 287 |   !! \case (<+ (<+ x)) => <+ <+ x ## id
 288 |            (<+ (+> x)) => <+ +> x ## id
 289 |            (+> x) => +> x ## id
 290 | 
 291 | export
 292 | lift_IO : HasIO io => io $- a =&> IO $- a
 293 | lift_IO = !! \x => x ## liftIO
 294 | 
 295 | ----------------------------------------------------------------------------------
 296 | -- How to run programs
 297 | ----------------------------------------------------------------------------------
 298 | 
 299 | ||| We need both a state and costate to run a program.
 300 | public export
 301 | run : (x : State a) -> Costate a -> a.response x.getVal
 302 | run x y = extract y x.getVal
 303 | 
 304 | ||| We can sequence two monadic costates
 305 | public export
 306 | seq2M : Monad m => Costate (Lift m a) -> Costate (Lift m b) -> Costate (Lift m (a &> b))
 307 | seq2M x y = costate
 308 |     (\xn => do v1 <- extract x xn.req
 309 |                v2 <- extract y (xn.cont v1)
 310 |                pure (v1 ## v2))
 311 | 
 312 | ||| Sequence and run three monadic operations.
 313 | public export
 314 | runSequenceM3 : Monad m =>
 315 |                 (input : State (a &> b &> c)) ->
 316 |                 Costate (Lift m a) -> Costate (Lift m b) -> Costate (Lift m c) ->
 317 |                 m ((a &> b &> c).response input.getVal)
 318 | runSequenceM3 inp x y z =
 319 |   let xn : Costate (Lift m (a &> b))
 320 |       xn = seq2M {m} x y
 321 |       yn : Costate (Lift m ((a &> b) &> c))
 322 |       yn = seq2M {m, a = a &> b, b = c} xn z
 323 |   in run {a = Lift m (a &> b &> c)} (state inp.getVal) yn
 324 | 
 325 | export
 326 | forward : (a -> b) -> (a :- c) =&> (b :- c)
 327 | forward f = !! \x => f x ## id
 328 | 
 329 | export
 330 | backward : (a -> b) -> (c :- b) =&> (c :- a)
 331 | backward f = !! \x => x ## f
 332 | 
 333 | ----------------------------------------------------------------------------------
 334 | -- Debugging
 335 | ----------------------------------------------------------------------------------
 336 | 
 337 | export
 338 | trace : Show a => (forall x. Show (b x)) => (!>) a b =&> (!>) a b
 339 | trace = !! \x => x ## (\y => trace "fwd input: \{show x}\nbwd input: \{show y}" y)
 340 | 
 341 | export
 342 | traceFwd : Show a => (!>) a b =&> (!>) a b
 343 | traceFwd = !! \x => x ## (\y => trace "fwd input: \{show x}" y)
 344 | 
 345 | export
 346 | traceBwd : (forall x. Show (b x)) => (!>) a b =&> (!>) a b
 347 | traceBwd = !! \x =>  x ## (\y => trace "bwd input: \{show y}" y)
 348 |