Type

{-

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 }