diff --git a/Compactable/Type b/Compactable/Type new file mode 100644 index 0000000..2583b87 --- /dev/null +++ b/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 } diff --git a/Compactable/apEither b/Compactable/apEither new file mode 100644 index 0000000..ef6e360 --- /dev/null +++ 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) diff --git a/Compactable/apOptional b/Compactable/apOptional new file mode 100644 index 0000000..d12f3f3 --- /dev/null +++ b/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) diff --git a/Compactable/bindEither b/Compactable/bindEither new file mode 100644 index 0000000..3801eb1 --- /dev/null +++ b/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) diff --git a/Compactable/bindOptional b/Compactable/bindOptional new file mode 100644 index 0000000..0d853c7 --- /dev/null +++ b/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) diff --git a/Compactable/compact b/Compactable/compact new file mode 100644 index 0000000..6c8158f --- /dev/null +++ b/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)) diff --git a/Compactable/mapEither b/Compactable/mapEither new file mode 100644 index 0000000..52f2152 --- /dev/null +++ b/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 + } diff --git a/Compactable/separate b/Compactable/separate new file mode 100644 index 0000000..abc9093 --- /dev/null +++ b/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)) diff --git a/Compactable/traverseEither b/Compactable/traverseEither new file mode 100644 index 0000000..d2354b0 --- /dev/null +++ b/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) diff --git a/Compactable/traverseOptional b/Compactable/traverseOptional new file mode 100644 index 0000000..f6ee0be --- /dev/null +++ b/Compactable/traverseOptional @@ -0,0 +1,110 @@ +{- + +When `f` is Traversable we can apply a function that compacts results, via `Optional`, within the Applicative +context while still preserving the semantics of the `traverse`. + +Examples: + +``` + let Either = ./Either/Type + +in let E = constructors (Either Text (Optional Natural)) + +in ./Compactable/traverseOptional + List + ./List/compactable + ./List/traversable + (Either Text) + (./Either/applicative/sequential Text) + Natural + Natural + ( λ(x : Natural) + → if Natural/isZero x + + then E.Left "No Zeros Allowed!!" + + else if Natural/odd x + + then E.Right (Some x) + + else E.Left "Only Odds!!" + ) + [ 1, 2, 3, 4, 5 ] += < Left = "Only Odds!!" | Right : List Natural > +``` + +``` + let Either = ./Either/Type + +in let E = constructors (Either Text (Optional Natural)) + +in ./Compactable/traverseOptional + List + ./List/compactable + ./List/traversable + (Either Text) + (./Either/applicative/sequential Text) + Natural + Natural + ( λ(x : Natural) + → if Natural/isZero x + + then E.Left "No Zeros Allowed!!" + + else if Natural/odd x + + then E.Right (Some x) + + else E.Left "Only Odds!!" + ) + [ 0, 1, 2, 3, 4, 5 ] += < Left = "No Zeros Allowed!!" | Right : List Natural > +``` + +``` + let Either = ./Either/Type + +in let E = constructors (Either Text (Optional Natural)) + +in ./Compactable/traverseOptional + List + ./List/compactable + ./List/traversable + (Either Text) + (./Either/applicative/sequential Text) + Natural + Natural + ( λ(x : Natural) + → if Natural/isZero x + + then E.Left "No Zeros Allowed!!" + + else if Natural/odd x + + then E.Right (Some x) + + else E.Left "Only Odds!!" + ) + [ 1, 3, 5 ] += < Right = [ 1, 3, 5 ] | Left : Text > +``` + +-} + 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) diff --git a/Either/compactable b/Either/compactable new file mode 100644 index 0000000..e7d8719 --- /dev/null +++ b/Either/compactable @@ -0,0 +1,28 @@ + 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) diff --git a/Either/flip b/Either/flip new file mode 100644 index 0000000..02aa7c7 --- /dev/null +++ b/Either/flip @@ -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 diff --git a/Either/hush b/Either/hush new file mode 100644 index 0000000..67f029c --- /dev/null +++ b/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) diff --git a/Either/lefts b/Either/lefts index fab489b..1bb6802 100644 --- a/Either/lefts +++ b/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 diff --git a/Either/partition b/Either/partition index a289e40..e2a53af 100644 --- a/Either/partition +++ b/Either/partition @@ -1,37 +1,24 @@ let Either = ./Type -in let partition - : ∀(a : Type) - → ∀(b : Type) - → List (Either a b) - → { lefts : List a, rights : List b } - = λ(a : Type) - → λ(b : Type) - → λ(eithers : List (Either a b)) - → let left = - λ(acc : { lefts : List a, rights : List b }) - → λ(x : a) - → { lefts = [ x ] # acc.lefts, rights = acc.rights } - - in let right = - λ(acc : { lefts : List a, rights : List b }) - → λ(y : b) - → { lefts = acc.lefts, rights = [ y ] # acc.rights } - - in List/fold - (Either a b) - eithers - { lefts : List a, rights : List b } - ( λ(e : Either a b) - → λ(acc : { lefts : List a, rights : List b }) - → ./fold - a - b - { lefts : List a, rights : List b } - (left acc) - (right acc) - e - ) - { lefts = [] : List a, rights = [] : List b } - -in partition +in λ(a : Type) + → λ(b : Type) + → λ(eithers : List (Either a b)) + → let left = + λ(acc : { _1 : List a, _2 : List b }) + → λ(x : a) + → { _1 = [ x ] # acc._1, _2 = acc._2 } + + in let right = + λ(acc : { _1 : List a, _2 : List b }) + → λ(y : b) + → { _1 = acc._1, _2 = [ y ] # acc._2 } + + in List/fold + (Either a b) + eithers + { _1 : List a, _2 : List b } + ( λ(e : Either a b) + → λ(acc : { _1 : List a, _2 : List b }) + → ./fold a b { _1 : List a, _2 : List b } (left acc) (right acc) e + ) + { _1 = [] : List a, _2 = [] : List b } diff --git a/Either/rights b/Either/rights index 39520b9..72ab630 100644 --- a/Either/rights +++ b/Either/rights @@ -3,4 +3,4 @@ in λ(a : Type) → λ(b : Type) → λ(eithers : List (Either a b)) - → (./partition a b eithers).rights + → (./partition a b eithers)._2 diff --git a/List/compactable b/List/compactable new file mode 100644 index 0000000..1f32701 --- /dev/null +++ b/List/compactable @@ -0,0 +1,16 @@ + let Optional/toList = + https://raw.githubusercontent.com/dhall-lang/dhall-lang/0a7f596d03b3ea760a96a8e03935f4baa64274e1/Prelude/Optional/toList + +in { mapOptional = + λ(a : Type) + → λ(b : Type) + → λ(k : a → Optional b) + → λ(list : List a) + → List/fold + a + list + (List b) + (λ(x : a) → λ(xs : List b) → Optional/toList b (k x) # xs) + ([] : List b) + } + : ./../Compactable/Type List diff --git a/Monad/Type b/Monad/Type index ba9380d..841f986 100644 --- a/Monad/Type +++ b/Monad/Type @@ -1,10 +1,7 @@ let Applicative = ./../Applicative/Type -in let Monad - : (Type → Type) → Type - = λ(f : Type → Type) - → { bind : - ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(k : a → f b) → f b - } - -in λ(f : Type → Type) → Applicative f ⩓ Monad f +in λ(f : Type → Type) + → Applicative f + ⩓ { bind : + ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(k : a → f b) → f b + } diff --git a/Optional/compactable b/Optional/compactable new file mode 100644 index 0000000..56f1efe --- /dev/null +++ b/Optional/compactable @@ -0,0 +1,10 @@ + let bind = (./monad).bind + +in { mapOptional = + λ(a : Type) + → λ(b : Type) + → λ(k : a → Optional b) + → λ(o : Optional a) + → bind a b o k + } + : ./../Compactable/Type Optional