
   0 | ||| This module provides interfaces similar to `Applicative`
   1 | ||| and `Traversable` for heterogeneous container types.
   2 | ||| We distinguish between two types of containers: Product
   3 | ||| types hold all their values at once, while sum types
   4 | ||| represent a choice: A generalization of `Either`.
   5 | |||
   6 | ||| The core data types in this library are indexed over a
   7 | ||| container (typically a List or List of Lists) of values
   8 | ||| of type `k` plus a type-level function `f` of type `k -> Type`.
   9 | ||| The values of the container index together with `f` determine
  10 | ||| the types of values at each position in the
  11 | ||| heterogeneous product or sum, while the shape of container
  12 | ||| indices mirror the shape of the corresponding product types.
  13 | |||
  14 | ||| The interfaces in this module allow us to create
  15 | ||| hetereogeneous containers from sufficiently general functions
  16 | ||| (`HPure`), use unary functions to change the context of
  17 | ||| values in a heterogeneous container (`HFunctor`),
  18 | ||| collapse heterogeneous containers into a single value (`HFoldable`)
  19 | ||| and run an effectful computation over all values in
  20 | ||| a heterogeneous container (`HSequence`).
  21 | |||
  22 | ||| In addition, `HFunctor` can be generalized to arbitrary
  23 | ||| n-ary functions (`HAp`). However, this case is special in that only
  24 | ||| the last argument of such a function can be a sum type
  25 | ||| while all other arguments have to be product types.
  26 | ||| This makes sense, since when combining values of two sum types,
  27 | ||| we typically cannot guarantee that the values point at
  28 | ||| same choice and are therefore compatible.
  29 | |||
  30 | ||| Implementation notes:
  31 | |||
  32 | ||| For many of the functions in this module, there is a constrained
  33 | ||| version taking an implicit heterogeneous product holding
  34 | ||| the desired implementations. Since Idris2 uses the same
  35 | ||| mechanism for resolving interface constraints and auto implicits,
  36 | ||| we do not need an additional structure or interface
  37 | ||| for these constraints.
  38 | ||| The disadvantage of this is, that we more often have to explicitly
  39 | ||| pattern match on these constraint products in order for Idris2
  40 | ||| to know where to look for implementations.
  41 | module Data.SOP.Interfaces
  42 | 
  43 | import Data.SOP.Utils
  44 | 
  45 | %default total
  46 | 
  47 | ||| A heterogeneous container indexed over a container type `l`
  48 | ||| holding values of type `k`.
  49 | %inline
  50 | public export
  51 | HCont : (k : Type) -> (l : Type) -> Type
  52 | HCont k l = (k -> Type) -> l -> Type
  53 | 
  54 | --------------------------------------------------------------------------------
  55 | --          HPure
  56 | --------------------------------------------------------------------------------
  57 | 
  58 | ||| This interface allows a heterogenous product to be filled
  59 | ||| with values, given a function which produce values of
  60 | ||| every possible type required.
  61 | |||
  62 | ||| @ k kind of Types in a heterogeneous container's  type level code
  63 | |||
  64 | ||| @ l kind of container used to describe a heterogeneous containr's type
  65 | |||     level code
  66 | |||
  67 | ||| @ p the heterogeneous sum or product
  68 | public export
  69 | interface HPure k l (0 p : HCont k l) | p where
  70 | 
  71 |   ||| Creates a heterogeneous product by using the given functio
  72 |   ||| to produce values.
  73 |   |||
  74 |   ||| ```idris example
  75 |   ||| Person : (f : Type -> Type) -> Type
  76 |   ||| Person f = NP f [String,Int]
  77 |   |||
  78 |   ||| emptyPerson : Person Maybe
  79 |   ||| emptyPerson = hpure Nothing
  80 |   ||| ```
  81 |   hpure :
  82 |        {0 f : k -> Type}
  83 |     -> {ks : l}
  84 |     -> (forall a . f a)
  85 |     -> p f ks
  86 | 
  87 | ||| Alias for `hpure empty`.
  88 | |||
  89 | ||| ```idris example
  90 | ||| Person : (f : Type -> Type) -> Type
  91 | ||| Person f = NP f [String,Int]
  92 | |||
  93 | ||| emptyPerson : Person Maybe
  94 | ||| emptyPerson = empty
  95 | ||| ```
  96 | public export
  97 | hempty : {ks : _} -> Alternative f => HPure Type l p => p f ks
  98 | hempty = hpure empty
  99 | 
 100 | ||| Fills a heterogeneous structure with a constant value
 101 | ||| in the (K a) functor.
 102 | |||
 103 | ||| ```idris example
 104 | ||| Person : (f : Type -> Type) -> Type
 105 | ||| Person f = NP f [String,Int]
 106 | |||
 107 | ||| fooPerson : Person (K String)
 108 | ||| fooPerson = hconst "foo"
 109 | ||| ```
 110 | public export
 111 | hconst : {ks : _} -> HPure k l p => (v : a) -> p (K a) ks
 112 | hconst v = hpure v
 113 | 
 114 | 
 115 | --------------------------------------------------------------------------------
 116 | --          HFunctor
 117 | --------------------------------------------------------------------------------
 118 | 
 119 | ||| A higher kinded functor allowing us to change the
 120 | ||| wrapper type or context of an n-ary sum or product.
 121 | |||
 122 | ||| @ k kind of Types in a heterogeneous container's  type level code
 123 | |||
 124 | ||| @ l kind of container used to describe a heterogeneous containr's type
 125 | |||     level code
 126 | |||
 127 | ||| @ p the actual heterogeneous container
 128 | public export
 129 | interface HFunctor k l (0 p : HCont k l) | p where
 130 | 
 131 |   ||| Maps the given function over all values in a
 132 |   ||| heterogeneous container, thus changing the context
 133 |   ||| of all of its values.
 134 |   |||
 135 |   ||| @ fun maps values in a heterogeneous container to a new context
 136 |   |||
 137 |   ||| @ p   the heterogeneous container, over which `fun` is mapped.
 138 |   |||
 139 |   ||| ```idris example
 140 |   ||| Person : (f : Type -> Type) -> Type
 141 |   ||| Person f = NP f [String,Int]
 142 |   |||
 143 |   ||| toPersonMaybe : Person I -> Person Maybe
 144 |   ||| toPersonMaybe = hmap Just
 145 |   ||| ```
 146 |   hmap :
 147 |        {0 f,g : k -> Type}
 148 |     -> {0 ks : l}
 149 |     -> (fun : forall a . f a -> g a)
 150 |     -> p f ks
 151 |     -> p g ks
 152 | 
 153 | ||| Alias for `hmap`
 154 | public export %inline
 155 | hliftA : HFunctor k l p => (forall a . f a -> g a) -> p f ks -> p g ks
 156 | hliftA = hmap
 157 | 
 158 | ||| Like `hpure` but using a constrained function for
 159 | ||| generating values. Since Idris is able to provide
 160 | ||| the required constraints
 161 | ||| already wrapped in a container of the correct
 162 | ||| shape, this is actually a derivative of `HFunctor` and not
 163 | ||| `HPure`. This has interesting consequences for sum
 164 | ||| types, for which this function is available as well.
 165 | ||| Since Idris has to choose a value of the sum
 166 | ||| itself, it will use the first possibility it
 167 | ||| can fill with the requested constraints.
 168 | |||
 169 | ||| In the first example below, Idris generates the value
 170 | ||| `MkSOP (Z ["","",[]])`. However, if the first choice does
 171 | ||| not have a Monoid instance, Idris faithfully chooses the
 172 | ||| next working possibility. In the second example,
 173 | ||| the result is `MkSOP (S (Z [[],[]]))`:
 174 | |||
 175 | ||| ```idris example
 176 | ||| neutralFoo : SOP I [[String,String,List Int],[Int]]
 177 | ||| neutralFoo = hcpure Monoid neutral
 178 | |||
 179 | ||| neutralBar : SOP I [[String,Int,List Int],[List String, List Int]]
 180 | ||| neutralBar = hcpure Monoid neutral
 181 | ||| ```
 182 | |||
 183 | ||| @ c   erased function argument to specify the constraint
 184 | |||       to use
 185 | |||
 186 | ||| @ fun generates values depending on the availability of
 187 | |||       a constraint
 188 | public export
 189 | hcpure :
 190 |      {auto _ : HFunctor k l p}
 191 |   -> (0 c : k -> Type)
 192 |   -> {auto cs : p c ks}
 193 |   -> (fund : forall a . c a => f a)
 194 |   -> p f ks
 195 | hcpure _ {cs} fun = hmap (\_ => fun) cs
 196 | 
 197 | --------------------------------------------------------------------------------
 198 | --          HAp
 199 | --------------------------------------------------------------------------------
 200 | 
 201 | ||| Like `Applicative`, this interface allows to
 202 | ||| map arbitrary n-ary Rank-2 functions over
 203 | ||| heterogeneous data structures of the same shape.
 204 | ||| However, in order to support products as well as sum types
 205 | ||| all arguments except the last one have to be products
 206 | ||| indexed over the same container as the last argument.
 207 | |||
 208 | ||| @ k kind of Types in a heterogeneous container's  type level code
 209 | |||
 210 | ||| @ l kind of container used to describe a heterogeneous containr's type
 211 | |||     level code
 212 | |||
 213 | ||| @ q heterogeneous product related to `p`. For product types,
 214 | |||     this is the same as `p`, for sum types it is the corresponding
 215 | |||     product type.
 216 | |||
 217 | ||| @ p the actual heterogeneous container (sum or product)
 218 | public export
 219 | interface HFunctor k l q => HFunctor k l p => HAp k l q p | p where
 220 | 
 221 |   ||| Higher kinded equivalent to `(<*>)`.
 222 |   |||
 223 |   ||| Applies wrapped functions in the product
 224 |   ||| container to the corresponding values in the
 225 |   ||| second container.
 226 |   |||
 227 |   ||| @ q product holding unary Rank-2 functions.
 228 |   |||
 229 |   ||| @ p sum or product to whose values the functions in `q` should
 230 |   |||     be applied
 231 |   |||
 232 |   ||| ```idris example
 233 |   ||| hapTest : SOP Maybe [[String,Int]] -> SOP I [[String,Int]]
 234 |   ||| hapTest = hap (MkPOP $ [[fromMaybe "foo", const 12]])
 235 |   ||| ```
 236 |   hap :
 237 |        {0 f,g : k -> Type}
 238 |     -> {0 ks : l}
 239 |     -> q (\a => f a -> g a) ks
 240 |     -> p f ks
 241 |     -> p g ks
 242 | 
 243 | ||| Higher kinded version of `liftA2`.
 244 | ||| This is a generalization of `hliftA` to binary
 245 | ||| functions.
 246 | public export
 247 | hliftA2 :
 248 |      {auto _ : HAp k l q p}
 249 |   -> (forall a . f a -> g a -> h a)
 250 |   -> q f ks
 251 |   -> p g ks
 252 |   -> p h ks
 253 | hliftA2 fun fs gs  = hliftA fun fs `hap` gs
 254 | 
 255 | ||| Higher kinded version of `liftA3`.
 256 | ||| This is a generalization of `hliftA` to ternary
 257 | ||| functions.
 258 | public export
 259 | hliftA3 :
 260 |      {auto _ : HAp k l q q}
 261 |   -> {auto _ : HAp k l q p}
 262 |   -> (forall a . f a -> g a -> h a -> i a)
 263 |   -> q f ks
 264 |   -> q g ks
 265 |   -> p h ks
 266 |   -> p i ks
 267 | hliftA3 fun fs gs hs = hliftA2 fun fs gs `hap` hs
 268 | 
 269 | ||| Higher kinded version of `liftA4`.
 270 | ||| This is a generalization of `hliftA` to quartenary
 271 | ||| functions.
 272 | public export
 273 | hliftA4 :
 274 |      {auto _ : HAp k l q q}
 275 |   -> {auto _ : HAp k l q p}
 276 |   -> (forall a . f a -> g a -> h a -> i a -> j a)
 277 |   -> q f ks
 278 |   -> q g ks
 279 |   -> q h ks
 280 |   -> p i ks
 281 |   -> p j ks
 282 | hliftA4 fun fs gs hs is = hliftA3 fun fs gs hs `hap` is
 283 | 
 284 | ||| Like `hmap` but uses a constrained function.
 285 | |||
 286 | ||| @ c   constraint used to convert values
 287 | |||
 288 | ||| @ fun constrained function for converting values to
 289 | |||       a new context
 290 | |||
 291 | ||| ```idris example
 292 | ||| showValues : NP I [String,Int] -> NP (K String) [String,Int]
 293 | ||| showValues = hcmap Show show
 294 | ||| ```
 295 | public export
 296 | hcmap :
 297 |      {auto _ : HAp k l q p}
 298 |   -> (0 c : k -> Type)
 299 |   -> {auto cs : q c ks}
 300 |   -> (fun : forall a . c a => f a -> g a)
 301 |   -> p f ks
 302 |   -> p g ks
 303 | hcmap _ {cs} fun = hliftA2 (\_ => fun) cs
 304 | 
 305 | ||| Alias for `hcmap`
 306 | public export %inline
 307 | hcliftA :
 308 |      {auto _ : HAp k l q p}
 309 |   -> (0 c : k -> Type)
 310 |   -> q c ks
 311 |   -> (fun : forall a . c a => f a -> g a)
 312 |   -> p f ks
 313 |   -> p g ks
 314 | hcliftA c x = hcmap c
 315 | 
 316 | ||| Like `hliftA2` but with a constrained function.
 317 | public export %inline
 318 | hcliftA2 :
 319 |      {auto _ : HAp k l q q}
 320 |   -> {auto _ : HAp k l q p}
 321 |   -> (0 c : k -> Type)
 322 |   -> {auto cs : q c ks}
 323 |   -> (fun : forall a . c a => f a -> g a -> h a)
 324 |   -> q f ks
 325 |   -> p g ks
 326 |   -> p h ks
 327 | hcliftA2 _ {cs} fun = hliftA3 (\_ => fun) cs
 328 | 
 329 | ||| Like `hliftA3` but with a constrained function.
 330 | public export %inline
 331 | hcliftA3 :
 332 |      {auto _ : HAp k l q q}
 333 |   -> {auto _ : HAp k l q p}
 334 |   -> (c : k -> Type)
 335 |   -> {auto cs : q c ks}
 336 |   -> (fun : forall a . c a => f a -> g a -> h a -> i a)
 337 |   -> q f ks
 338 |   -> q g ks
 339 |   -> p h ks
 340 |   -> p i ks
 341 | hcliftA3 _ {cs} fun = hliftA4 (\_ => fun) cs
 342 | 
 343 | --------------------------------------------------------------------------------
 344 | --          HFold
 345 | --------------------------------------------------------------------------------
 346 | 
 347 | public export
 348 | interface HFold k l (0 p : HCont k l) | p where
 349 | 
 350 |   ||| Strict fold over a heterogeneous sum or product
 351 |   ||| parameterized by the constant functor (and thus being actually
 352 |   ||| a homogeneous sum or product).
 353 |   hfoldl : {0 ks : l} -> (acc -> el -> acc) -> acc -> p (K el) ks -> acc
 354 | 
 355 |   ||| Lazy fold over a heterogeneous sum or product
 356 |   ||| parameterized by the constant functor (and thus being actually
 357 |   ||| a homogeneous sum or product).
 358 |   hfoldr :
 359 |        {0 ks : l}
 360 |     -> (el -> Lazy acc -> acc)
 361 |     -> Lazy acc
 362 |     -> p (K el) ks
 363 |     -> acc
 364 | 
 365 | 
 366 | ||| Calculates the size of a heterogeneous container
 367 | public export
 368 | hsize : (HFunctor k l p, HFold k l p) => p f ks -> Nat
 369 | hsize = hfoldl (+) Z . hmap (const 1)
 370 | 
 371 | ||| Alias for `hfoldl (<+>) neutral`.
 372 | public export
 373 | hconcat : (Monoid m, HFold k l p) => p (K m) ks -> m
 374 | hconcat = hfoldl (<+>) neutral
 375 | 
 376 | ||| Alias for `hconcat . hmap fun`
 377 | public export
 378 | hconcatMap :
 379 |      {auto _ : Monoid m}
 380 |   -> {auto _ : HFunctor k l p}
 381 |   -> {auto _ : HFold k l p}
 382 |   -> (fun : forall a . f a -> m)
 383 |   -> p f ks
 384 |   -> m
 385 | hconcatMap fun = hconcat . hmap fun
 386 | 
 387 | ||| Alias for `hconcat . hcmap c fun`
 388 | public export
 389 | hcconcatMap :
 390 |      {auto _ : Monoid m}
 391 |   -> {auto _ : HAp k l q p}
 392 |   -> {auto _ : HFold k l p}
 393 |   -> (0 c    : k -> Type)
 394 |   -> {auto _ : q c ks}
 395 |   -> (fun    : forall a . c a => f a -> m)
 396 |   -> p f ks
 397 |   -> m
 398 | hcconcatMap c fun = hconcat . hcmap c fun
 399 | 
 400 | ||| Generalization of `sequence_` to heterogeneous containers.
 401 | |||
 402 | ||| Alias for `hfoldl (*>) (pure ())`.
 403 | public export
 404 | hsequence_ : (Applicative g, HFold k l p) => p (K (g ())) ks -> g ()
 405 | hsequence_ = hfoldl (*>) (pure ())
 406 | 
 407 | ||| Generalization of `traverse_` to heterogeneous containers.
 408 | |||
 409 | ||| Alias for `hsequence_ . hmap fun`.
 410 | public export
 411 | htraverse_ :
 412 |      {auto _ : Applicative g}
 413 |   -> {auto _ : HFunctor k l p}
 414 |   -> {auto _ : HFold k l p}
 415 |   -> (forall a . f a -> g ())
 416 |   -> p f ks
 417 |   -> g ()
 418 | htraverse_ fun = hsequence_ . hmap fun
 419 | 
 420 | ||| Generalization of `for_` to heterogeneous containers.
 421 | public export
 422 | hfor_ :  (Applicative g, HFold k l p, HFunctor k l p)
 423 |       => p f ks -> (forall a . f a -> g ()) -> g ()
 424 | hfor_ = flip htraverse_
 425 | 
 426 | ||| Generalization of `and` to heterogeneous containers.
 427 | public export
 428 | hand : HFold k l p => p (K Bool) ks -> Bool
 429 | hand = hfoldr (\a,b => a && b) True
 430 | 
 431 | ||| Generalization of `toList` to heterogeneous containers.
 432 | export
 433 | htoList : (HFunctor k l p, HFold k l p) => p (K a) ks -> List a
 434 | htoList = hconcatMap pure
 435 | 
 436 | ||| Generalization of `or` to heterogeneous containers.
 437 | export
 438 | hor : HFold k l p => p (K Bool) ks -> Bool
 439 | hor = hfoldr (\a,b => a || b) False
 440 | 
 441 | ||| Generalization of `all` to heterogeneous containers.
 442 | export
 443 | hall :
 444 |      {auto _ : HFunctor k l p}
 445 |   -> {auto _ : HFold k l p}
 446 |   -> (forall a . f a -> Bool)
 447 |   -> p f ks -> Bool
 448 | hall fun = hand . hmap fun
 449 | 
 450 | ||| Generalization of `any` to heterogeneous containers.
 451 | export
 452 | hany :
 453 |      {auto _ : HFunctor k l p}
 454 |   -> {auto _ : HFold k l p}
 455 |   -> (forall a . f a -> Bool)
 456 |   -> p f ks -> Bool
 457 | hany fun = hor . hmap fun
 458 | 
 459 | ||| Generalization of `choice` to heterogeneous containers.
 460 | export
 461 | hchoice : HFold k l p => Alternative f =>  p (K $ f a) ks -> f a
 462 | hchoice = hfoldr (\a,b => a <|> b) empty
 463 | 
 464 | --------------------------------------------------------------------------------
 465 | --          HSequence
 466 | --------------------------------------------------------------------------------
 467 | 
 468 | ||| Sequencing of applicative effects over a heterogeneous
 469 | ||| container.
 470 | public export
 471 | interface HSequence k l (0 p : HCont k l) | p where
 472 | 
 473 |   ||| Given a heterogeneous containers holding values
 474 |   ||| wrapped in effect `g`, sequences applications of
 475 |   ||| `g` to the outside of the heterogeneous container.
 476 |   |||
 477 |   ||| ```idris example
 478 |   ||| seqMaybe : NP Maybe [Int,String] -> Maybe (NP I [Int,String])
 479 |   ||| seqMaybe = hsequence
 480 |   ||| ```
 481 |   hsequence :
 482 |        {0 ks : l}
 483 |     -> {0 f : k -> Type}
 484 |     -> {auto app : Applicative g}
 485 |     -> p (\a => g (f a)) ks
 486 |     -> g (p f ks)
 487 | 
 488 | ||| Traverses a heterogeneous container by applying effectful
 489 | ||| function `fun`.
 490 | |||
 491 | ||| ```idris example
 492 | ||| htraverseEx : NP (Either String) [Int,String] -> Maybe (NP I [Int,String])
 493 | ||| htraverseEx = htraverse (either (const Nothing) Just)
 494 | ||| ```
 495 | export
 496 | htraverse :
 497 |      {0 f,f' : k -> Type}
 498 |   -> {auto _ : Applicative g}
 499 |   -> {auto _ : HFunctor k l p}
 500 |   -> {auto _ : HSequence k l p}
 501 |   -> (fun : forall a . f a -> g (f' a))
 502 |   -> p f ks
 503 |   -> g (p f' ks)
 504 | htraverse fun = hsequence . hmap fun
 505 | 
 506 | ||| Flipped version of `htraverse`.
 507 | export
 508 | hfor :
 509 |      {0 f,f' : k -> Type}
 510 |   -> {auto _ : Applicative g}
 511 |   -> {auto _ : HFunctor k l p}
 512 |   -> {auto _ : HSequence k l p}
 513 |   -> p f ks
 514 |   -> (forall a . f a -> g (f' a))
 515 |   -> g (p f' ks)
 516 | hfor = flip htraverse
 517 | 
 518 | ||| Constrained version of `htraverse`.
 519 | |||
 520 | ||| ```idris example
 521 | ||| interface Read a where
 522 | |||   read : String -> Maybe a
 523 | |||
 524 | ||| hctraverseEx : NP Read [Int,String] =>
 525 | |||                NP (K String) [Int,String] -> Maybe (NP I [Int,String])
 526 | ||| hctraverseEx = hctraverse Read read
 527 | ||| ```
 528 | export
 529 | hctraverse :
 530 |      {0 f,f' : k -> Type}
 531 |   -> {auto _ : Applicative g}
 532 |   -> {auto _ : HAp k l q p}
 533 |   -> {auto _ : HSequence k l p}
 534 |   -> (0 c : k -> Type)
 535 |   -> {auto cs : q c ks}
 536 |   -> (forall a . c a => f a -> g (f' a))
 537 |   -> p f ks
 538 |   -> g (p f' ks)
 539 | hctraverse c fun = hsequence . hcmap c fun
 540 | 
 541 | ||| Flipped version of `hctraverse`.
 542 | export
 543 | hcfor :
 544 |      {0 f,f' : k -> Type}
 545 |   -> {auto _ : Applicative g}
 546 |   -> {auto _ : HAp k l q p}
 547 |   -> {auto _ : HSequence k l p}
 548 |   -> (0 c : k -> Type)
 549 |   -> {auto cs : q c ks}
 550 |   -> p f ks
 551 |   -> (forall a . c a => f a -> g (f' a))
 552 |   -> g (p f' ks)
 553 | hcfor c = flip (hctraverse c)
 554 | 
 555 | --------------------------------------------------------------------------------
 556 | --          HCollapse
 557 | --------------------------------------------------------------------------------
 558 | 
 559 | ||| Collapsing a heterogeneous container to a homogeneous one
 560 | ||| of the same shape.
 561 | public export
 562 | interface HCollapse k l (0 p : HCont k l) (0 collapseTo : Type -> Type) | p where
 563 | 
 564 |   ||| A heterogeneous container over constant functor `K a` is
 565 |   ||| actually a homogeneous one holding only values of type `a`.
 566 |   ||| This function extracts the wrapped values into a homogeneous
 567 |   ||| one of the same size and shape.
 568 |   hcollapse : {0 a : Type} -> {0 ks : l} -> p (K a) ks -> collapseTo a
 569 |