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