0 | module Control.HigherOrder
  1 |
  2 | infixr 0 ~>
  3 | infixr 0 ~~>
  4 |
  5 | ||| Type of natural transformations between two functors.
  6 | public export
  7 | 0
  8 | (~>) : (Type -> Type) -> (Type -> Type) -> Type
  9 | f ~> g = forall a. f a -> g a
 10 |
 11 | ||| As above, but with explicit 0-morphisms.
 12 | public export
 13 | 0
 14 | (~~>) : (Type -> Type) -> (Type -> Type) -> (Type -> Type)
 15 | (f ~~> g) a = f a -> g a
 16 |
 17 | ||| Higher-order functor, i.e. a functor
 18 | ||| in the category of functors and natural transformations.
 19 | public export
 20 | interface HFunctor h where
 21 |   hmap : (Functor f, Functor g)
 22 |       =>   f ~>   g
 23 |       -> h f ~> h g
 24 |
 25 | infixr 8 :+:
 26 |
 27 | ||| Higher-order disjoint union.
 28 | ||| Effects are composed via this datatype.
 29 | public export
 30 | data (:+:) : (sig1 : (Type -> Type) -> (Type -> Type))
 31 |           -> (sig2 : (Type -> Type) -> (Type -> Type))
 32 |           -> (m : Type -> Type)
 33 |           -> (a : Type)
 34 |           -> Type where
 35 |   Inl : sig1 m a -> (:+:) sig1 sig2 m a
 36 |   Inr : sig2 m a -> (:+:) sig1 sig2 m a
 37 |
 38 | public export
 39 | HFunctor sig1 => HFunctor sig2 => HFunctor (sig1 :+: sig2) where
 40 |   hmap t (Inl op) = Inl (hmap t op)
 41 |   hmap t (Inr op) = Inr (hmap t op)
 42 |
 43 | ||| Higher order projections.
 44 | ||| Prj forms a category.
 45 | public export
 46 | interface Prj (0 sup : (Type -> Type) -> (Type -> Type))
 47 |               (0 sub : (Type -> Type) -> (Type -> Type)) | sub where
 48 |   constructor MkPrj
 49 |   prj : sup m a -> sub m a
 50 |
 51 | ||| Higher order injections.
 52 | ||| Inj forms a category.
 53 | public export
 54 | interface Inj (0 sub : (Type -> Type) -> (Type -> Type))
 55 |               (0 sup : (Type -> Type) -> (Type -> Type)) | sub where
 56 |   constructor MkInj
 57 |   inj : sub m a -> sup m a
 58 |
 59 | export
 60 | Prj sub' sub => Inj sub sup => Inj sub' sup where
 61 |   inj = inj . prj {sup = sub', sub}
 62 |
 63 | namespace Inj
 64 |   ||| Identity injection.
 65 |   ||| Example: `a :+: b ↦ a :+: b`
 66 |   public export
 67 |   [S] Inj sig sig where
 68 |      inj = id
 69 |
 70 |   ||| Inject to a Sum from the left.
 71 |   ||| Example: `a ↦ a :+: b`
 72 |   public export
 73 |   [L] Inj sig1 (sig1 :+: sig2) where
 74 |     inj = Inl
 75 |
 76 |   ||| Inject to a Sum from the right.
 77 |   ||| Example: `b ↦ a :+: b`
 78 |   public export
 79 |   [R] Inj sig2 (sig1 :+: sig2) where
 80 |     inj = Inr
 81 |
 82 |   ||| Composition of injections.
 83 |   ||| Example: `b ↦ (a :+: b) :+: c`
 84 |   public export
 85 |   [Trans] (inner : Inj siga sigb) => (outer : Inj sigb sigc) => Inj siga sigc where
 86 |     inj = inj {sub = sigb, sup = sigc}
 87 |         . inj {sub = siga, sup = sigb}
 88 |
 89 |   ||| Same as `Trans`, but the two arguments are explicit.
 90 |   public export
 91 |   T : (inner : Inj siga sigb) -> (outer : Inj sigb sigc) -> Inj siga sigc
 92 |   T inner outer = Trans @{inner} @{outer}
 93 |
 94 | ||| State-preserving transformation of
 95 | ||| a computation in one monad into a computation
 96 | ||| in another monad, whose value is annotated with the final state.
 97 | ||| Handler is a natural transformation.
 98 | public export
 99 | 0
100 | Handler : (Type -> Type)
101 |        -> (Type -> Type)
102 |        -> (Type -> Type)
103 |        -> Type
104 | Handler s m n = s . m ~> n . s
105 |
106 | ||| Handler with explicit 0-morphism.
107 | public export
108 | 0
109 | HandlerX : (Type -> Type)
110 |         -> (Type -> Type)
111 |         -> (Type -> Type)
112 |         -> (Type -> Type)
113 | HandlerX s m n = s . m ~~> n . s
114 |
115 | public export
116 | interface HFunctor sig => Syntax sig where
117 |   ||| Extend the continuation.
118 |   emap : forall m. (m a -> m b) -> (sig m a -> sig m b)
119 |   ||| Generically thread a handler through a higher-order
120 |   ||| signature.
121 |   weave : (m1 : Monad m) => (m2 : Monad n) => (fs : Functor s)
122 |        => s ()
123 |        -> Handler s m n
124 |        -> (sig m a -> sig n (s a))
125 |
126 | public export
127 | Syntax sig1 => Syntax sig2 => Syntax (sig1 :+: sig2) where
128 |   emap f (Inl op) = Inl (emap f op)
129 |   emap f (Inr op) = Inr (emap f op)
130 |
131 |   weave s hdl (Inl op) = Inl (weave s hdl op)
132 |   weave s hdl (Inr op) = Inr (weave s hdl op)
133 |
134 | ||| Lift a first-order functor to a second-order one.
135 | public export
136 | data Lift : (sig : (Type -> Type))
137 |          -> ((Type -> Type) -> (Type -> Type)) where
138 |   MkLift : sig (m a) -> Lift sig m a
139 |
140 | public export
141 | unlift : Lift sig m a -> sig (m a)
142 | unlift (MkLift x) = x
143 |
144 | ||| Alias for use as an effect.
145 | public export
146 | LiftE : (sig : Type -> Type) -> (Type -> Type) -> (Type -> Type)
147 | LiftE = Lift
148 |
149 | public export
150 | Functor sig => HFunctor (Lift sig) where
151 |   hmap t (MkLift op) = MkLift (map t op)
152 |
153 | public export
154 | Functor sig => Syntax (Lift sig) where
155 |   emap f (MkLift op) = MkLift (map f op)
156 |
157 |   weave s hdl (MkLift op) = MkLift $
158 |     map (\p => hdl (map (const p) s)) op
159 |
160 | infixr 1 ~<~
161 |
162 | -- hdl1 : ctxt1 . m ~> n . ctxt1
163 | -- hdl2 : ctxt2 . l ~> m . ctxt2
164 | -- ?    : (ctxt1 . ctxt2) . l ~> n . (ctxt1 . ctxt2)
165 | --
166 | --  (ctxt1 . ctxt2) . l ===
167 | --  ctxt1 . (ctxt2 . l) ==>
168 | --  ctxt1 . (m . ctxt2) ===
169 | --  (ctxt1 . m) . ctxt2 ==>
170 | --  (n . ctxt1) . ctxt2 ===
171 | --  n . (ctxt1 . ctxt2)
172 | ||| Fuse two handlers.
173 | public export
174 | (~<~) : (f : Functor n)
175 |      => (g : Functor ctx1)
176 |      => (forall q. HandlerX ctx1 m n q)
177 |      -> (forall t. HandlerX ctx2 l m t)
178 |      -> (forall p. HandlerX (ctx1 . ctx2) l n p)
179 | hdl1 ~<~ hdl2 = hdl1 . map hdl2
180 |
181 |