Add Compactable

Compactable/Type

@@ -0,0 +1,19 @@
+{-
+
+Compactable serves as an abstraction over filtering and partitioning, using two functions
+compact and separate, respectively.
+
+Both functions work over some higher kind f (Type -> Type).
+
+compact works over the f when it is fully applied with an Optional type. It filters out None
+values, leaving only the values contained in the Some values.
+
+separate works over the f when it is fully applied with an Either type. It partitions Left
+values to the _1 element of a tuple, and Right values to the _2 element of a tuple.
+
+Since both functions can be written in terms of the other, we can create instances by choosing one
+of the function fromCompact or fromSeparate.
+
+-}
+  λ(f : Type → Type)
+→ { mapOptional : ∀(a : Type) → ∀(b : Type) → (a → Optional b) → f a → f b }

Compactable/apEither

@@ -0,0 +1,30 @@
+{-
+apEither maps an `f` of functions to Eithers over the `f a` and `separate`s `Left`s from `Right`s.
+
+    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,31 @@
+{-
+
+apOptional maps a `f` of functions to Optionals over the `f` and `compact`s away the `None` values.
+
+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,44 @@
+{-
+
+bindEither binds to a `f` of Optional over the `f a` and `separate`s `Left`s and `Right`s.
+
+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,38 @@
+{-
+
+bindOptional binds to a `f` of Optional over the `f a` and `compact`s away the `None` values.
+
+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,23 @@
+{-
+
+mapOptional maps a function to Optionals over the `f` and `compact`s away the `None` values.
+
+Examples:
+
+```
+./Compactable/mapOptional
+List
+./List/compactable
+./List/functor
+Natural
+Natural
+(λ(n : Natural) → if Natural/even n then Some n else None Natural)
+[ 1, 2, 3, 4, 5 ]
+= [ 2, 4 ]
+```
+
+-}
+  λ(f : Type → Type)
+→ λ(c : ./Type f)
+→ λ(a : Type)
+→ c.mapOptional (Optional a) a ((./../Function/category).identity (Optional a))

Compactable/separate

@@ -0,0 +1,49 @@
+{-
+
+mapEither maps a function to Either over the `f` and `separate`s `Left`s from `Right`s.
+
+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 flipEither = ./../Either/flipEither
+
+in    λ(f : Type → Type)
+    → λ(c : ./Type f)
+    → λ(l : Type)
+    → λ(r : Type)
+    → λ(fa : f (Either l r))
+    → { _1 =
+          c.mapOptional
+          (Either l r)
+          l
+          ( compose
+            (Either l r)
+            (Either r l)
+            (Optional l)
+            (hush r l)
+            (flipEither l r)
+          )
+          fa
+      , _2 =
+          c.mapOptional (Either l r) r (hush l r) fa
+      }

Compactable/traverseEither

@@ -0,0 +1,20 @@
+    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)
+    → λ(b : Type)
+    → λ(k : a → g (Either a b))
+    → λ(fa : f a)
+    → applicative.map
+      (f (Either a b))
+      { _1 : f a, _2 : f b }
+      (./separate f c a b)
+      (traversable.traverse g applicative a (Either a b) k fa)

Compactable/traverseOptional

@@ -0,0 +1,18 @@
+    let Traversable = ./../Traversable/Type
+
+in  let Applicative = ./../Applicative/Type
+
+in    λ(f : Type → Type)
+    → λ(c : ./Type f)
+    → λ(traversable : Traversable f)
+    → λ(g : Type → Type)
+    → λ(applicative : Applicative g)
+    → λ(a : Type)
+    → λ(b : Type)
+    → λ(k : a → g (Optional b))
+    → λ(fa : f a)
+    → applicative.map
+      (f (Optional b))
+      (f b)
+      (./compact f c b)
+      (traversable.traverse g applicative a (Optional b) k fa)

Either/compactable

@@ -0,0 +1,31 @@
+{-
+mapOptional : (a -> Optional b) -> Either m a -> Either m b
+-}
+    let Either = ./Type
+
+in  let Monoid = ./../Monoid/Type
+
+in    λ(m : Type)
+    → λ(monoid : Monoid m)
+    →   { mapOptional =
+              λ(a : Type)
+            → λ(b : Type)
+            → λ(k : a → Optional b)
+            → λ(either : Either m a)
+            →     let E = constructors (Either m b)
+
+              in  merge
+                  { Left =
+                      λ(x : m) → E.Left x
+                  , Right =
+                        λ(y : a)
+                      → Optional/fold
+                        b
+                        (k y)
+                        (Either m b)
+                        E.Right
+                        (E.Left monoid.unit)
+                  }
+                  either
+        }
+      : ./../Compactable/Type (Either m)

Either/flipEither

@@ -0,0 +1,30 @@
+{-
+
+Flip the value of an Either where `Right` goes to `Left`, and `Left` goes to `Right`.
+
+Examples:
+```
+    let Either = ./Either/Type
+
+in  let E = constructors (Either Text Natural)
+
+in  ./Either/flipEither Text Natural (E.Left "ohno")
+= < Right = "ohno" | Left : Natural >
+
+
+    let Either = ./Either/Type
+
+in  let E = constructors (Either Text Natural)
+
+in  ./Either/flipEither Text Natural (E.Right 42)
+= < Left = 42 | Right : Text >
+```
+
+-}
+    let Either = ./Type
+
+in    λ(a : Type)
+    → λ(b : Type)
+    →     let E = constructors (Either b a)
+
+      in  ./fold a b (Either b a) E.Right E.Left

Either/hush

@@ -0,0 +1,27 @@
+{-
+
+Turns an `Either a b` into an `Optional b` by hushing `Left` values to `None` and
+converting `Right` values to `Some`.
+
+Examples:
+```
+    let Either = ./Either/Type
+
+in  let E = constructors (Either Text Natural)
+
+in  ./Either/hush Text Natural (E.Right 42)
+= Some 42
+
+
+    let Either = ./Either/Type
+
+in  let E = constructors (Either Text Natural)
+
+in  ./Either/hush Text Natural (E.Left "ohno")
+= None Natural
+```
+
+-}
+  λ(a : Type)
+→ λ(b : Type)
+→ ./fold a b (Optional b) (λ(_ : a) → None b) (λ(x : b) → Some x)

Either/lefts

@@ -3,4 +3,4 @@
 in    λ(a : Type)
     → λ(b : Type)
     → λ(eithers : List (Either a b))
-    → (./partition a b eithers).lefts
+    → (./partition a b eithers)._1