
   0 | module Nested
   1 | 
   2 | import Control.Applicative.Const
   3 | import Control.Monad.Identity
   4 | import Control.Monad.Reader.Reader
   5 | 
   6 | ||| This serves as our higher-order "function" from `a` to `b`.
   7 | public export
   8 | NaturalTransformation : {k : Type} -> (k -> Type) -> (k -> Type) -> Type
   9 | NaturalTransformation a b = {x : k} -> a x -> b x
  10 | 
  11 | ||| Higher-order version of an "f-algebra" (i.e. `f a -> a`)
  12 | public export
  13 | Algebra : {k : Type} -> ((k -> Type) -> k -> Type) -> (k -> Type) -> Type
  14 | Algebra f g = NaturalTransformation (f g) g
  15 | 
  16 | ||| Higher-order version of an "f-co-algebra" (i.e. `a -> f a`)
  17 | public export
  18 | Coalgebra : {k : Type} -> ((k -> Type) -> k -> Type) -> (k -> Type) -> Type
  19 | Coalgebra f g = NaturalTransformation g (f g)
  20 | 
  21 | ||| Type of an higher-order mapping, a functor over type indexes.
  22 | public export
  23 | HFunctor : {k1, k2 : Type} -> ((k1 -> Type) -> k2 -> Type) -> Type
  24 | HFunctor f =  {a, b : k1 -> Type}
  25 |            -> NaturalTransformation a b -> NaturalTransformation (f a) (f b)
  26 | 
  27 | ||| Serves as a proof that an indexed type (e.g.), `t`, is formed through nested
  28 | ||| (a.k.a. non-uniform) layers of the higher-order functor, `f`.
  29 | public export
  30 | record Nested (t : k -> Type) (f : (k -> Type) -> k -> Type) where
  31 |   constructor MkNested
  32 |   hfunctor : HFunctor f
  33 |   project : Coalgebra f t
  34 |   embed : Algebra f t
  35 | 
  36 | ||| Reduce a realized nested value bottom-up to a output with the same index.
  37 | export
  38 | hfold :  {t, r : k -> Type} -> Nested t f
  39 |       -> Algebra f r -> NaturalTransformation t r
  40 | hfold n a = f
  41 |   where
  42 |     f : NaturalTransformation t r
  43 |     f x = a (n.hfunctor f (n.project x))
  44 | 
  45 | ||| Given an algebra-based transformation, prepare a transformation that acts
  46 | ||| as if it were unfolding a nested value, without reifying the nested
  47 | ||| structure.  Effectively substituting a call to the algebra for any
  48 | ||| constructors of `t`
  49 | |||
  50 | ||| Universal property (for all n, a, and ghf):
  51 | |||   hfold n a . hbuild n ghf = ghf a
  52 | export
  53 | hbuild :  {t : k -> Type} -> Nested t f -> {r : k -> Type}
  54 |        -> ({x : k -> Type} -> Algebra f x -> NaturalTransformation r x)
  55 |        -> NaturalTransformation r t
  56 | hbuild n f = f n.embed
  57 | 
  58 | ||| Build a nested value top-down to from a seed with the same index.
  59 | export
  60 | hunfold :  {t, r : k -> Type} -> Nested t f
  61 |         -> Coalgebra f r -> NaturalTransformation r t
  62 | hunfold n c = u
  63 |   where
  64 |     u : NaturalTransformation r t
  65 |     u x = n.embed (n.hfunctor u (c x))
  66 | 
  67 | ||| Universal property (for all n, ghu, and c):
  68 | |||   hdestory n ghu . hunfold n c = ghu c
  69 | export
  70 | hdestroy :  {t, r : k -> Type} -> Nested t f
  71 |          -> ({x : k -> Type} -> Coalgebra f x -> NaturalTransformation x r)
  72 |          -> NaturalTransformation t r
  73 | hdestroy n u = u n.project
  74 | 
  75 | ||| Build a transformation with a nested recursion pattern, roughly equivalent
  76 | ||| to `hfold n a . hunfold n c`, but the nested type, `n`, is an implicit
  77 | ||| fixed-point of `f`.
  78 | export
  79 | hhylo :  {k : Type} -> {f : (k -> Type) -> k -> Type} -> HFunctor f
  80 |       -> {i, o : k -> Type} -> Coalgebra f i -> Algebra f o -> NaturalTransformation i o
  81 | hhylo hmap c a = h
  82 |   where
  83 |     h : NaturalTransformation i o
  84 |     h = a . hmap h . c
  85 | 
  86 | HJoin : {k : Type} -> ((k -> Type) -> k -> Type) -> Type
  87 | HJoin m = {f : k -> Type} -> NaturalTransformation (m (m f)) (m f)
  88 | 
  89 | HDuplicate : {k : Type} -> ((k -> Type) -> k -> Type) -> Type
  90 | HDuplicate w = {f : k -> Type} -> NaturalTransformation (w f) (w (w f))
  91 | 
  92 | record HMonad (m : (k -> Type) -> k -> Type) where
  93 |   constructor MkHMonad
  94 |   hfunctor : HFunctor m
  95 |   hjoin : HJoin m
  96 | 
  97 | record HComonad (w : (k -> Type) -> k -> Type) where
  98 |   constructor MkHComonad
  99 |   hfunctor : HFunctor w
 100 |   hduplicate : HDuplicate w
 101 | 
 102 | HDist : {k : Type} -> (f, g : (k -> Type) -> k -> Type) -> Type
 103 | HDist f g = {y : k -> Type} -> NaturalTransformation (f (g y)) (g (f y))
 104 | 
 105 | ghhylo :  {k : Type} -> {f, m, w : (k -> Type) -> k -> Type}
 106 |        -> HFunctor f -> HMonad m -> HComonad w
 107 |        -> HDist m f -> HDist f w
 108 |        -> {i, o : k -> Type} -> Coalgebra (f . m) i -> Algebra (f . w) o
 109 |        -> NaturalTransformation i o
 110 | ghhylo hmap monad comonad distM distW c a =
 111 |     a . hmap (hhylo {f} hmap gc ga) . c
 112 |   where
 113 |     gc : Coalgebra f (m i)
 114 |     gc = hmap monad.hjoin . distM . monad.hfunctor c
 115 |     ga : Algebra f (w o)
 116 |     ga = comonad.hfunctor a . distW . hmap comonad.hduplicate
 117 | 
 118 | data HFree : (f : (k -> Type) -> k -> Type) -> (a : k -> Type) -> k -> Type where
 119 |   HFreePure : {x : k} -> a x -> HFree f a x
 120 |   HFreeWrap : f (HFree f a) x -> HFree f a x
 121 | 
 122 | hfunctorHfree :  {f : (k -> Type) -> k -> Type}
 123 |               -> HFunctor f -> HFunctor (HFree f)
 124 | hfunctorHfree hmap = freeMap
 125 |  where
 126 |    freeMap :  NaturalTransformation a b
 127 |            -> NaturalTransformation (HFree f a) (HFree f b)
 128 |    freeMap t = mappedT
 129 |      where
 130 |        mappedT : NaturalTransformation (HFree f a) (HFree f b)
 131 |        mappedT (HFreePure ax) = HFreePure (t ax)
 132 |        mappedT (HFreeWrap ffax) = HFreeWrap (hmap mappedT ffax)
 133 | 
 134 | hjoinHfree : {g : (k -> Type) -> k -> Type} -> HFunctor g -> HJoin (HFree g)
 135 | hjoinHfree hmap = freeJoin
 136 |   where
 137 |     freeJoin : HJoin (HFree g)
 138 |     freeJoin (HFreePure ffgx) = ffgx
 139 |     freeJoin (HFreeWrap gfgfgfx) = HFreeWrap (hmap freeJoin gfgfgfx)
 140 | 
 141 | hmonadHfree : {f : (k -> Type) -> k -> Type} -> HFunctor f -> HMonad (HFree f)
 142 | hmonadHfree hmap = MkHMonad (hfunctorHfree {f} hmap) (hjoinHfree {g=f} hmap)
 143 | 
 144 | hdistHfree : {f : (k -> Type) -> k -> Type} -> HFunctor f -> HDist (HFree f) f
 145 | hdistHfree hmap = freeDist
 146 |   where
 147 |     freeDist : HDist (HFree f) f
 148 |     freeDist (HFreePure fyx) = hmap HFreePure fyx
 149 |     freeDist (HFreeWrap ffffyx) = hmap (HFreeWrap . freeDist) ffffyx
 150 | 
 151 | record HCofree (f : (k -> Type) -> k -> Type) (a : k -> Type) (x : k) where
 152 |   constructor (:<)
 153 |   hextract : a x
 154 |   hunwrap : f (HCofree f a) x
 155 | 
 156 | hfunctorHcofree :  {f : (k -> Type) -> k -> Type}
 157 |                 -> HFunctor f -> HFunctor (HCofree f)
 158 | hfunctorHcofree hmap = cofreeMap
 159 |   where
 160 |     cofreeMap :  NaturalTransformation a b
 161 |               -> NaturalTransformation (HCofree f a) (HCofree f b)
 162 |     cofreeMap t = mappedT
 163 |       where
 164 |         mappedT : NaturalTransformation (HCofree f a) (HCofree f b)
 165 |         mappedT (ax :< fcfax) = t ax :< hmap mappedT fcfax
 166 | 
 167 | hduplicateHcofree :  {g : (k -> Type) -> k -> Type}
 168 |                   -> HFunctor g -> HDuplicate (HCofree g)
 169 | hduplicateHcofree hmap = cofreeDup
 170 |   where
 171 |     cofreeDup : HDuplicate (HCofree g)
 172 |     cofreeDup cfg@(ax :< gcfax) = cfg :< hmap cofreeDup gcfax
 173 | 
 174 | hcomonadHcofree :  {f : (k -> Type) -> k -> Type}
 175 |                 -> HFunctor f -> HComonad (HCofree f)
 176 | hcomonadHcofree hmap =
 177 |   MkHComonad (hfunctorHcofree {f} hmap) (hduplicateHcofree {g=f} hmap)
 178 | 
 179 | hdistHcofree :  {f : (k -> Type) -> k -> Type}
 180 |              -> HFunctor f -> HDist f (HCofree f)
 181 | hdistHcofree hmap = cofreeDist
 182 |   where
 183 |     cofreeDist : HDist f (HCofree f)
 184 |     cofreeDist fcfyx = hmap hextract fcfyx :< hmap (cofreeDist . hunwrap) fcfyx
 185 | 
 186 | hchrono :  {k : Type} -> {f : (k -> Type) -> k -> Type} -> HFunctor f
 187 |         -> {i, o : k -> Type}
 188 |         -> Coalgebra (f . HFree f) i -> Algebra (f . HCofree f) o
 189 |         -> NaturalTransformation i o
 190 | hchrono hmap =
 191 |   ghhylo
 192 |     {f} hmap
 193 |     (hmonadHfree {f} hmap) (hcomonadHcofree {f} hmap)
 194 |     (hdistHfree {f} hmap) (hdistHcofree {f} hmap)
 195 | 
 196 | ||| Polykinded right Kan extension of `g` along `f`
 197 | public export
 198 | Ran : {k : Type} -> (k -> Type) -> (k -> Type) -> Type -> Type
 199 | Ran f g a = {y : k} -> (a -> f y) -> g y
 200 | 
 201 | mapRan : {a, b : Type} -> (a -> b) -> Ran f g a -> Ran f g b
 202 | mapRan f r mk = r (mk . f)
 203 | 
 204 | runRan : {a : Type} -> Ran f g a -> (a -> f a) -> g a
 205 | runRan r p = r p
 206 | 
 207 | ||| Index-changing fold via right Kan extension of the `r`esult functor along a
 208 | ||| `c`arrier functor.  A specialized version of `hfold` with some of the
 209 | ||| arguments rearranged.
 210 | export
 211 | gfold :  {t, c, r : Type -> Type} -> Nested t f -> Algebra f (Ran c r)
 212 |       -> {i, o : Type} -> (i -> c o) -> t i -> r o
 213 | gfold n a fn tx = hfold n a tx fn
 214 | 
 215 | ||| Polykinded left Kan extension of `g` along `f`
 216 | public export
 217 | record Lan (f : k -> Type) (g : k -> Type) a where
 218 |   constructor MkLan
 219 |   {target : k}
 220 |   extract : f target -> a
 221 |   pool : g target
 222 | 
 223 | mapLan : {a, b : Type} -> (a -> b) -> Lan f g a -> Lan f g b
 224 | mapLan f l = MkLan (f . l.extract) l.pool
 225 | 
 226 | ||| Like `gunfold`, but apply the algebra instead of the constructors of `t`.
 227 | export
 228 | gbuild :  {t : Type -> Type} -> Nested t f -> {c, s : Type -> Type}
 229 |        -> (ghf :  {x : Type -> Type}
 230 |                -> Algebra f x -> NaturalTransformation (Lan c s) x
 231 |           )
 232 |        -> {i, o : Type} -> (c i -> o) -> s i -> t o
 233 | gbuild n ghf fn sx = hbuild n ghf (MkLan fn sx)
 234 | 
 235 | -- gfold n a . gbuild n ghf = ghf a
 236 | 
 237 | ||| Index-changing unfold via left Kan extension of the `s`eed functor along
 238 | ||| a `c`arrier function.  A specialized version of `hunfold` with the "Lan"
 239 | ||| argument curried.
 240 | export
 241 | gunfold :  {t, c, s : Type -> Type} -> Nested t f -> Coalgebra f (Lan c s)
 242 |         -> {i, o : Type} -> (c i -> o) -> s i -> t o
 243 | gunfold n ca fn sx = hunfold n ca (MkLan fn sx)
 244 | 
 245 | ||| Like `hdestroy` in the same way that `gfold` is like `hfold`.
 246 | |||
 247 | ||| Universal property:
 248 | |||   (gdestroy n ghu f . gunfold n c g) x = ghu c (MkLan g x) f
 249 | export
 250 | gdestroy :  {t, c, r : Type -> Type} -> Nested t f
 251 |          -> (ghu :  {x : Type -> Type} -> Coalgebra f x
 252 |                  -> NaturalTransformation x (Ran c r)
 253 |             )
 254 |          -> {i, o : Type} -> (i -> c o) -> t i -> r o
 255 | gdestroy n ghu fn tx = hdestroy n ghu tx fn
 256 | 
 257 | ||| Codensity monad, the right Kan extension of a functor along itself
 258 | public export
 259 | Codensity : {k : Type} -> (k -> Type) -> Type -> Type
 260 | Codensity f = Ran f f
 261 | 
 262 | ||| Index changing refold, like `gfold n co ec . gunfold n a ic` except that
 263 | ||| the `n : Nested t f` (and indeed `t` itself) are implied by `t` being an
 264 | ||| implicit fixed-point of `f`.  A specialization of 
 265 | ghylo :  {f : (Type -> Type) -> Type -> Type} -> HFunctor f
 266 |       -> {s, c, r : Type -> Type}
 267 |       -> Coalgebra f (Lan c s) -> Algebra f (Ran c r)
 268 |       -> {i, m, o : Type} -> (m -> c o) -> (c i -> m) -> s i -> r o
 269 | ghylo hmap co a ic ec sx = hhylo {f} hmap co a (MkLan ec sx) ic
 270 | 
 271 | ||| Reduce to a single value of the index type.  A specialization of `gfold`.
 272 | export
 273 | ffold :  {t : Type -> Type} -> Nested t f
 274 |       -> {a : Type} -> Algebra f (Codensity (Const a)) -> t a -> a
 275 | ffold n alg = runConst . gfold n alg {o=Void} MkConst
 276 | 
 277 | ||| Density comonad, the left Kan extension of a functor along itself.
 278 | public export
 279 | Density : (k -> Type) -> Type -> Type
 280 | Density f = Lan f f
 281 | 
 282 | pureDensity : ({0 x : Type} -> x -> f x) -> a -> Density f a
 283 | pureDensity puref x = MkLan (const x) (puref MkUnit)
 284 | 
 285 | applyDensity :  ({0 a, b : Type} -> (a -> b) -> f a -> f b)
 286 |              -> ({0 x : Type} -> x -> f x)
 287 |              -> ({0 a, b : Type} -> f (a -> b) -> f a -> f b)
 288 |              -> Density f (a -> b) -> Density f a -> Density f b
 289 | applyDensity mapf puref applyf (MkLan extractf poolf) (MkLan extractx poolx) =
 290 |   MkLan (\fk => extractf (mapf fst fk) (extractx (mapf snd fk)))
 291 |     (applyf (applyf (puref MkPair) poolf) poolx)
 292 | 
 293 | dupDensity : Density f a -> Density f (Density f a)
 294 | dupDensity x = MkLan (const x) (pool x)
 295 | 
 296 | ||| Like `funfold` in the same way `gbuild` is like `gunfold`.  Specialization
 297 | ||| of `gbuild`.
 298 | export
 299 | fbuild :  {t : Type -> Type} -> Nested t f -> {a : Type}
 300 |        -> (ghf :  {x : Type -> Type}
 301 |                -> Algebra f x -> NaturalTransformation (Density (Const a)) x
 302 |           )
 303 |        -> a -> t a
 304 | fbuild n ghf = gbuild n ghf {i=Void} runConst . MkConst
 305 | 
 306 | 
 307 | ||| Unfold from a single value, with the type of that value being the output
 308 | ||| index.  A specialization of `gunfold`.
 309 | export
 310 | funfold :  {t : Type -> Type} -> Nested t f
 311 |         -> {a : Type} -> Coalgebra f (Density (Const a)) -> a -> t a
 312 | funfold n c = gunfold n c {i=Void} runConst . MkConst
 313 | 
 314 | ||| Like `ffold` in the same way `gdestroy` is like `gfold`.  Specialization of
 315 | ||| `gdestroy`.
 316 | export
 317 | fdestroy :  {t : Type -> Type} -> Nested t f -> {a : Type}
 318 |          -> (ghu :  {x : Type -> Type}
 319 |                  -> Coalgebra f x
 320 |                  -> NaturalTransformation x (Codensity (Const a))
 321 |             )
 322 |          -> t a -> a
 323 | fdestroy n ghu = runConst . gdestroy n ghu {o=Void} MkConst
 324 | 
 325 | Recursive : Type -> (Type -> Type) -> Type
 326 | Recursive t f = Nested (const t) ((.) f)
 327 | 
 328 | mkRecursive :  (ffmap : {a, b : Type} -> (a -> b) -> f a -> f b)
 329 |             -> (project : t -> f t)
 330 |             -> (embed : f t -> t)
 331 |             -> Recursive t f
 332 | mkRecursive fmap project embed = MkNested hmap project embed
 333 | where
 334 |   hmap :  {a, b : Unit -> Type} -> NaturalTransformation a b
 335 |        -> NaturalTransformation (f . a) (f . b)
 336 |   hmap n = fmap n
 337 | 
 338 | fmap : Recursive t f -> {a, b : Type} -> (a -> b) -> f a -> f b
 339 | fmap n fn = n.hfunctor {x = MkUnit} fn
 340 | 
 341 | (.fmap) : Recursive t f -> {a, b : Type} -> (a -> b) -> f a -> f b
 342 | (.fmap) = fmap
 343 | 
 344 | project : Recursive t f -> t -> f t
 345 | project r = r.project {x = MkUnit}
 346 | 
 347 | (.project) : Recursive t f -> t -> f t
 348 | (.project) = project
 349 | 
 350 | embed : Recursive t f -> f t -> t
 351 | embed r = r.embed {x = MkUnit}
 352 | 
 353 | (.embed) : Recursive t f -> f t -> t
 354 | (.embed) = embed
 355 | 
 356 | fold : {t : Type} -> Recursive t f -> {a : Type} -> (f a -> a) -> t -> a
 357 | fold r alg tx = hfold r alg {x = MkUnit} tx
 358 | 
 359 | nmap :  {t : Type -> Type} -> Nested t f
 360 |      -> (ffmap :  ({a, b : Type} -> (a -> b) -> t a -> t b)
 361 |                -> {a, b : Type} -> (a -> b) -> f t a -> f t b)
 362 |      -> {a, b : Type} -> (a -> b) -> t a -> t b
 363 | nmap n ffmap = tmap
 364 | where
 365 |   tmap : {a, b : Type} -> (a -> b) -> t a -> t b
 366 |   tmap {a} {b} f = fmap
 367 |   where
 368 |     fmap : t a -> t b
 369 |     fmap = n.embed . ffmap tmap f . n.project
 370 |