0 | module Stellar.API.Interface
  1 |
  2 | import Stellar.API.Definition
  3 | import public Control.Relation
  4 | import public Control.Category
  5 | import Data.List1
  6 |
  7 | public export
  8 | interface Category mor => APIFunctor (0 mor : Rel API) (0 f : API -> API) where
  9 |   constructor MkAPIFunctor
 10 |   map : (a `mor` b) -> f a `mor` f b
 11 |
 12 | private infixl 7 &&&
 13 |
 14 | public export
 15 | interface Category mor => APIBifunctor (0 mor : Rel API) (0 f : API -> API -> API) | f, mor where
 16 |   constructor MkAPIBifunctor
 17 |   bimap : (a `mor` b) -> x `mor` y -> f a x `mor` f b y
 18 |
 19 | export
 20 | mapFst : APIBifunctor mor bi => a `mor` b -> bi a c `mor` bi b c
 21 | mapFst m = bimap m id
 22 |
 23 | export
 24 | mapSnd : APIBifunctor mor bi => a `mor` b -> bi c a `mor` bi c b
 25 | mapSnd m = bimap id m
 26 |
 27 | public export
 28 | interface APIMonoid (0 mor : Rel API) (0 bi : API -> API -> API) where
 29 |   empty : API
 30 |   idLeft : bi empty a `mor` a
 31 |   idRight : bi a empty `mor` a
 32 |   assoc1 : bi a (bi b c) `mor` bi (bi a b) c
 33 |   assoc2 : bi (bi a b) c `mor` bi a (bi b c)
 34 |
 35 | public export
 36 | interface (APIBifunctor mor bi) => Cartesian (0 mor : Rel API) (0 bi : API -> API -> API) where
 37 |   constructor MkAPICartesian
 38 |   fst : (a `bi` b) `mor` a
 39 |   snd : (a `bi` b) `mor` b
 40 |   (&&&) : c `mor` a -> c `mor` b -> c `mor` (a `bi` b)
 41 |
 42 | export
 43 | swap : Cartesian mor bi => bi x y `mor` bi y x
 44 | swap = (&&&) snd fst
 45 |
 46 | export
 47 | duplicate : Cartesian mor bi => a `mor` bi a a
 48 | duplicate = id &&& id
 49 |
 50 | export
 51 | assocCart1 : Cartesian mor bi => bi a (bi b c) `mor` bi (bi a b) c
 52 | assocCart1 = mapSnd fst &&& (snd . snd)
 53 |
 54 | export
 55 | assocCart2 : Cartesian mor bi => bi (bi a b) c `mor` bi a (bi b c)
 56 | assocCart2 = (fst . fst) &&& mapFst snd
 57 |
 58 | public export
 59 | interface (Cartesian mor bi) => APIAlternative (0 mor : Rel API) (0 bi : API -> API -> API) (0 f : API -> API) | f, bi where
 60 |   constructor MkAPIAlternative
 61 |   err : Forever `mor` f a
 62 |   firstSuccess : (f a `bi` f a) `mor` f a
 63 |
 64 | export
 65 | or : (alt : APIAlternative mor bi f) => a `mor` f b -> a `mor` f b -> a `mor` f b
 66 | or x y = firstSuccess @{alt} . bimap x y . duplicate {bi}
 67 |
 68 | export
 69 | tryAll : (alt : APIAlternative mor bi f) => List1 (mor a (f b)) -> mor a (f b)
 70 | tryAll = foldl1 (or @{alt})
 71 |
 72 | export
 73 | [FromBifunctor] APIBifunctor mor f2 => APIFunctor mor (f2 a) where
 74 |   map = bimap id
 75 |
 76 | public export
 77 | interface APIFunctor mor f => APIPointed mor f | f where
 78 |   constructor MkAPIPointed
 79 |   pure : a `mor` f a
 80 |
 81 | public export
 82 | interface APIPointed mor f => APIMonad mor f | f, mor where
 83 |   constructor MkAPIMonad
 84 |   join : f (f a) `mor` f a
 85 |
 86 | public export
 87 | interface APIFunctor mor f => APICopointed mor f | f where
 88 |   constructor MkAPICopointed
 89 |   extract : f a `mor` a
 90 |
 91 | public export
 92 | interface APIPointed mor f => APIComonad mor f | f, mor where
 93 |   constructor MkAPIComonad
 94 |   dup : f a `mor` f (f a)
 95 |
 96 | export
 97 | returnFirst : (alt : APIAlternative mor bi f) =>
 98 |               a `mor` f b ->
 99 |               a `mor` f b ->
100 |               a `mor` f b
101 | returnFirst m1 m2 = firstSuccess @{alt} . bimap m1 m2 . duplicate
102 |
103 | %hide Prelude.(.)
104 |
105 | ||| Kleisli composition
106 | export
107 | (>=>) : (mon : APIMonad mor f) => a `mor` f b -> b `mor` f c -> a `mor` f c
108 | (>=>) x y = join . map y . x
109 |
110 | ||| Cokleisli composition, NOT right-to-left kleisli composition
111 | export
112 | (<=<) : (comon : APIComonad mor f) => f a `mor` b -> f b `mor` c -> f a `mor` c
113 | (<=<) y x = x . map {f} y . dup
114 |
115 | public export
116 | APIKleisli : (f : API -> API) -> Rel API -> Rel API
117 | APIKleisli f mor x y = x `mor` f y
118 |
119 | export %hint
120 | APIKleisliInstance :  (monad : APIMonad mor f) => Category (APIKleisli f mor)
121 | APIKleisliInstance = MkCategory (pure {mor, f}) (flip (>=>))
122 |