Add Compactable

Compactable/Type

@@ -0,0 +1,16 @@
+{-
+
+Compactable serves as an abstraction over filtering using a mapping function to `Optional`s over
+a higher-kind `f : Type -> Type`.
+
+`mapOptional` should map over the `f` applying the function `a -> Optional b` and filtering
+out `None` values, leaving only the values contained in the `Some` values.
+
+We can see the relation between `mapOptional` and `filter` by observing that we keep values when
+we have `Some` i.e. `True` for `filter`, and discard vaues when have `None` i.e. `False` for `filter`.
+`mapOptional` is more powerful than `filter` because we can also transform our values to another type `b`,
+whereas `filter` will only work on values of type `a`.
+
+-}
+  λ(f : Type → Type)
+→ { mapOptional : ∀(a : Type) → ∀(b : Type) → (a → Optional b) → f a → f b }

Compactable/apEither

@@ -0,0 +1,36 @@
+{-
+
+When `f` is an Applicative we can apply a function that separates results, via `Either`, within the Applicative
+context while still preserving the semantics of `ap`.
+
+Examples:
+
+```
+    let E = constructors (./Either/Type Natural Natural)
+
+in  ./Compactable/apEither
+    List
+    ./List/compactable
+    ./List/applicative
+    Natural
+    Natural
+    [ λ(n : Natural) → if Natural/even n then E.Left n else E.Right n
+    , λ(n : Natural) → if Natural/odd n then E.Left n else E.Right n
+    ]
+    [ 0, 1, 2, 3, 4, 5 ]
+= { _1 = [ 0, 2, 4, 1, 3, 5 ], _2 = [ 1, 3, 5, 0, 2, 4 ] }
+```
+
+-}
+    let Applicative = ./../Applicative/Type
+
+in  let Either = ./../Either/Type
+
+in    λ(f : Type → Type)
+    → λ(c : ./Type f)
+    → λ(applicative : Applicative f)
+    → λ(a : Type)
+    → λ(b : Type)
+    → λ(k : f (a → Either a b))
+    → λ(fa : f a)
+    → ./separate f c a b (applicative.ap a (Either a b) k fa)

Compactable/apOptional

@@ -0,0 +1,32 @@
+{-
+
+When `f` is an Applicative we can apply a function that compacts results, via `Optional`, within the Applicative
+context while still preserving the semantics of `ap`.
+
+Examples:
+
+```
+./Compactable/apOptional
+List
+./List/compactable
+./List/applicative
+Natural
+Natural
+[ λ(n : Natural) → if Natural/even n then Some n else None Natural
+, λ(n : Natural) → if Natural/odd n then Some n else None Natural
+]
+[ 0, 1, 2, 3, 4, 5 ]
+= [ 0, 2, 4, 1, 3, 5 ]
+```
+
+-}
+    let Applicative = ./../Applicative/Type
+
+in    λ(f : Type → Type)
+    → λ(c : ./Type f)
+    → λ(applicative : Applicative f)
+    → λ(a : Type)
+    → λ(b : Type)
+    → λ(k : f (a → Optional b))
+    → λ(fa : f a)
+    → ./compact f c b (applicative.ap a (Optional b) k fa)

Compactable/bindEither

@@ -0,0 +1,45 @@
+{-
+
+When `f` is a Monad we can bind a function that separates results, via `Either`, within the Monadic
+context while still preserving the semantics of `bind`.
+
+Examples:
+
+```
+    let replicate =
+          https://raw.githubusercontent.com/dhall-lang/dhall-lang/master/Prelude/List/replicate
+
+in  let Either = ./Either/Type
+
+in  let E = constructors (Either Natural Natural)
+
+in  ./Compactable/bindEither
+    List
+    ./List/compactable
+    ./List/monad
+    Natural
+    Natural
+    (   λ(n : Natural)
+      →       if Natural/even n
+
+        then  replicate n (Either Natural Natural) (E.Left n)
+
+        else  replicate n (Either Natural Natural) (E.Right n)
+    )
+    [ 0, 1, 2, 3, 4, 5 ]
+= { _1 = [ 2, 2, 4, 4, 4, 4 ], _2 = [ 1, 3, 3, 3, 5, 5, 5, 5, 5 ] }
+```
+
+-}
+    let Monad = ./../Monad/Type
+
+in  let Either = ./../Either/Type
+
+in    λ(f : Type → Type)
+    → λ(c : ./Type f)
+    → λ(monad : Monad f)
+    → λ(a : Type)
+    → λ(b : Type)
+    → λ(k : a → f (Either a b))
+    → λ(fa : f a)
+    → ./separate f c a b (monad.bind a (Either a b) fa k)

Compactable/bindOptional

@@ -0,0 +1,39 @@
+{-
+
+When `f` is a Monad we can apply a function that compacts results, via `Optional`, within the Monadic
+context while still preserving the semantics of `bind`.
+
+Examples:
+
+```
+    let replicate =
+          https://raw.githubusercontent.com/dhall-lang/dhall-lang/master/Prelude/List/replicate
+
+in  ./Compactable/bindOptional
+    List
+    ./List/compactable
+    ./List/monad
+    Natural
+    Natural
+    (   λ(n : Natural)
+      →       if Natural/even n
+
+        then  replicate n (Optional Natural) (Some n)
+
+        else  [] : List (Optional Natural)
+    )
+    [ 0, 1, 2, 3, 4, 5 ]
+= [ 2, 2, 4, 4, 4, 4 ]
+```
+
+-}
+    let Monad = ./../Monad/Type
+
+in    λ(f : Type → Type)
+    → λ(c : ./Type f)
+    → λ(monad : Monad f)
+    → λ(a : Type)
+    → λ(b : Type)
+    → λ(k : a → f (Optional b))
+    → λ(fa : f a)
+    → ./compact f c b (monad.bind a (Optional b) fa k)

Compactable/compact

@@ -0,0 +1,21 @@
+{-
+
+`compact` removes any `None` values from `f` and preserves the `Some` values, compacting
+the result.
+
+Examples:
+
+```
+./Compactable/compact
+List
+./List/compactable
+Natural
+[ None Natural, Some 2, None Natural, Some 4, None Natural ]
+= [ 2, 4 ]
+```
+
+-}
+  λ(f : Type → Type)
+→ λ(c : ./Type f)
+→ λ(a : Type)
+→ c.mapOptional (Optional a) a ((./../Function/category).identity (Optional a))

Compactable/mapEither

@@ -0,0 +1,59 @@
+{-
+
+Similar to a Functor map over `f` where `b` is constrained to `Either`. This constraint gives
+us enough information to partition results into a tuple, where `Left`s match to `_1` and `Right`s
+match to `_2`.
+
+`mapEither` can also be seen as a parititioning function.
+
+Examples:
+
+```
+    let E = constructors (./Either/Type Natural Natural)
+
+in  ./Compactable/mapEither
+    List
+    ./List/compactable
+    ./List/functor
+    Natural
+    Natural
+    (λ(n : Natural) → if Natural/even n then E.Left n else E.Right n)
+    [ 1, 2, 3, 4, 5 ]
+= { _1 = [ 2, 4 ], _2 = [ 1, 3, 5 ] }
+```
+
+-}
+    let Either = ./../Either/Type
+
+in  let compose = (./../Function/category).compose
+
+in  let hush = ./../Either/hush
+
+in  let flip = ./../Either/flip
+
+in    λ(f : Type → Type)
+    → λ(c : ./Type f)
+    → λ(a : Type)
+    → λ(l : Type)
+    → λ(r : Type)
+    → λ(k : a → Either l r)
+    → λ(fa : f a)
+    → { _1 =
+          c.mapOptional
+          a
+          l
+          ( compose
+            a
+            (Either r l)
+            (Optional l)
+            (hush r l)
+            (compose a (Either l r) (Either r l) (flip l r) k)
+          )
+          fa
+      , _2 =
+          c.mapOptional
+          a
+          r
+          (compose a (Either l r) (Optional r) (hush l r) k)
+          fa
+      }

Compactable/separate

@@ -0,0 +1,33 @@
+{-
+
+`separate` partitions any `Left` values from `f` into the `_1` side of a tuple, and any `Right` values
+from `f` into the `_2` side of a tuple, essentially separating the values.
+
+Examples:
+
+```
+    let E = constructors (./Either/Type Natural Natural)
+
+in  ./Compactable/separate
+    List
+    ./List/compactable
+    Natural
+    Natural
+    [ E.Right 1, E.Left 2, E.Right 3, E.Left 4, E.Right 5 ]
+= { _1 = [ 2, 4 ], _2 = [ 1, 3, 5 ] }
+```
+
+-}
+    let Either = ./../Either/Type
+
+in    λ(f : Type → Type)
+    → λ(c : ./Type f)
+    → λ(l : Type)
+    → λ(r : Type)
+    → ./mapEither
+      f
+      c
+      (Either l r)
+      l
+      r
+      ((./../Function/category).identity (Either l r))

Compactable/traverseEither

@@ -0,0 +1,87 @@
+{-
+
+When `f` is Traverable we can apply a function that separates results, via `Either`, within the Applicative
+context while still preserving the semantics of the `traverse`.
+
+Examples:
+
+```
+    let Either = ./Either/Type
+
+in  let E = constructors (Either Natural Natural)
+
+in  ./Compactable/traverseEither
+    List
+    ./List/compactable
+    ./List/traversable
+    Optional
+    ./Optional/applicative
+    Natural
+    Natural
+    Natural
+    (   λ(x : Natural)
+      →       if Natural/isZero x
+
+        then  None (Either Natural Natural)
+
+        else  if Natural/odd x
+
+        then  Some (E.Left x)
+
+        else  Some (E.Right x)
+    )
+    [ 1, 2, 3, 4, 5]
+= Some { _1 = [ 1, 3, 5 ], _2 = [ 2, 4 ] }
+```
+
+```
+    let Either = ./Either/Type
+
+in  let E = constructors (Either Natural Natural)
+
+in  ./Compactable/traverseEither
+    List
+    ./List/compactable
+    ./List/traversable
+    Optional
+    ./Optional/applicative
+    Natural
+    Natural
+    Natural
+    (   λ(x : Natural)
+      →       if Natural/isZero x
+
+        then  None (Either Natural Natural)
+
+        else  if Natural/odd x
+
+        then  Some (E.Left x)
+
+        else  Some (E.Right x)
+    )
+    [ 0, 1, 2, 3, 4, 5]
+= None { _1 : List Natural, _2 : List Natural }
+```
+
+-}
+    let Traversable = ./../Traversable/Type
+
+in  let Applicative = ./../Applicative/Type
+
+in  let Either = ./../Either/Type
+
+in    λ(f : Type → Type)
+    → λ(c : ./Type f)
+    → λ(traversable : Traversable f)
+    → λ(g : Type → Type)
+    → λ(applicative : Applicative g)
+    → λ(a : Type)
+    → λ(l : Type)
+    → λ(r : Type)
+    → λ(k : a → g (Either l r))
+    → λ(fa : f a)
+    → applicative.map
+      (f (Either l r))
+      { _1 : f l, _2 : f r }
+      (./separate f c l r)
+      (traversable.traverse g applicative a (Either l r) k fa)