From 6e6b3c3128d5d6e12d40b0b72e80efcfe7a3c6ed Mon Sep 17 00:00:00 2001 From: Andrey Mokhov Date: Tue, 12 May 2020 01:02:06 +0100 Subject: [PATCH] Move batch and match to the united repo --- selective.cabal | 9 +- src/Control/Batch.hs | 52 ---------- src/Control/Match.hs | 173 -------------------------------- src/Control/Match/Arrow.hs | 149 --------------------------- src/Control/Match/Profunctor.hs | 158 ----------------------------- src/Control/United.hs | 92 ----------------- 6 files changed, 2 insertions(+), 631 deletions(-) delete mode 100644 src/Control/Batch.hs delete mode 100644 src/Control/Match.hs delete mode 100644 src/Control/Match/Arrow.hs delete mode 100644 src/Control/Match/Profunctor.hs delete mode 100644 src/Control/United.hs diff --git a/selective.cabal b/selective.cabal index 85a6a84..9fa852c 100644 --- a/selective.cabal +++ b/selective.cabal @@ -34,16 +34,11 @@ source-repository head library hs-source-dirs: src - exposed-modules: Control.Batch, - Control.Match, - Control.Match.Arrow, - Control.Match.Profunctor, - Control.Selective, + exposed-modules: Control.Selective, Control.Selective.Free, Control.Selective.Multi, Control.Selective.Rigid.Free, - Control.Selective.Rigid.Freer, - Control.United + Control.Selective.Rigid.Freer build-depends: base >= 4.7 && < 5, containers >= 0.5.5.1 && < 0.7, transformers >= 0.4.2.0 && < 0.6 diff --git a/src/Control/Batch.hs b/src/Control/Batch.hs deleted file mode 100644 index acaf374..0000000 --- a/src/Control/Batch.hs +++ /dev/null @@ -1,52 +0,0 @@ -{-# LANGUAGE DeriveFunctor, EmptyCase, TypeFamilies, GADTs, RankNTypes #-} -{-# LANGUAGE GeneralizedNewtypeDeriving, ScopedTypeVariables, LambdaCase #-} ------------------------------------------------------------------------------ --- | --- Module : Control.Batch --- Copyright : (c) Andrey Mokhov 2018-2020 --- License : MIT (see the file LICENSE) --- Maintainer : andrey.mokhov@gmail.com --- Stability : experimental --- --- An experiment in expressing Functor, Applicative and Monad using the Batch --- type class. ------------------------------------------------------------------------------ -module Control.Batch where - -import Data.Kind -import Prelude hiding (pure) - --- | A data type defining no tags. Similar to 'Data.Void.Void' but parameterised. -data Zero a where - --- | A data type with a single tag. This data type is commonly known as @Refl@, --- see "Data.Type.Equality". -data One a b where - One :: One a a - --- | A data type with two tags 'A' and 'B' that allows us to encode the good old --- 'Either' as 'Sigma' 'Two', where the tags 'A' and 'B' correspond to 'Left' --- and 'Right', respectively. See 'eitherToSigma' and 'sigmaToEither' that --- witness the isomorphism between 'Either' @a b@ and 'Sigma' @(@'Two'@ a b)@. -data Two a b c where - A :: Two a b a - B :: Two a b b - --- | A potentially uncountable collection of tags for the same unit @()@ payload. -data Many a b where - Many :: a -> Many a () - -class Functor f => Batch f where - type Tag f :: (* -> *) -> Constraint - batch :: Tag f t => ((forall x. t x -> x) -> a) -> (forall x. t x -> f x) -> f a - -pure :: (Batch f, Tag f Zero) => a -> f a -pure a = batch (const a) (\(x :: Zero a) -> case x of {}) - -fmap :: (Batch f, Tag f (One a)) => (a -> b) -> f a -> f b -fmap f x = batch (\lookup -> f (lookup One)) (\One -> x) - -mult :: (Batch f, Tag f (Two a b)) => f a -> f b -> f (a, b) -mult x y = batch (\lookup -> (lookup A, lookup B)) $ \case { A -> x; B -> y } - --- What about Many? diff --git a/src/Control/Match.hs b/src/Control/Match.hs deleted file mode 100644 index 83571a9..0000000 --- a/src/Control/Match.hs +++ /dev/null @@ -1,173 +0,0 @@ -{-# LANGUAGE DeriveFunctor, TypeFamilies, GADTs, RankNTypes #-} -{-# LANGUAGE GeneralizedNewtypeDeriving, ScopedTypeVariables, LambdaCase #-} ------------------------------------------------------------------------------ --- | --- Module : Control.Match --- Copyright : (c) Andrey Mokhov 2018-2020 --- License : MIT (see the file LICENSE) --- Maintainer : andrey.mokhov@gmail.com --- Stability : experimental --- --- An experiment in expressing Applicative, Selective and Monad using the Match --- type class. ------------------------------------------------------------------------------ -module Control.Match where - -import Control.Applicative ((<**>)) -import Data.Functor.Const -import Data.Kind -import Prelude hiding (pure) - --- | A generalised sum type where @t@ stands for the type of constructor "tags". --- Each tag has a type parameter @x@ which determines the type of the payload. --- A 'Sigma' @t@ value therefore contains a payload whose type is not visible --- externally but is revealed when pattern-matching on the tag. --- --- See 'Two', 'eitherToSigma' and 'sigmaToEither' for an example. -data Sigma t where - Sigma :: t x -> x -> Sigma t - --- | A data type defining no tags. Similar to 'Data.Void.Void' but parameterised. -data Zero a where - --- | A data type with a single tag. This data type is commonly known as @Refl@, --- see "Data.Type.Equality". -data One a b where - One :: One a a - --- | A data type with two tags 'A' and 'B' that allows us to encode the good old --- 'Either' as 'Sigma' 'Two', where the tags 'A' and 'B' correspond to 'Left' --- and 'Right', respectively. See 'eitherToSigma' and 'sigmaToEither' that --- witness the isomorphism between 'Either' @a b@ and 'Sigma' @(@'Two'@ a b)@. -data Two a b c where - A :: Two a b a - B :: Two a b b - --- | Encode 'Either' into a generalised sum type. -eitherToSigma :: Either a b -> Sigma (Two a b) -eitherToSigma = \case - Left a -> Sigma A a - Right b -> Sigma B b - --- | Decode 'Either' from a generalised sum type. -sigmaToEither :: Sigma (Two a b) -> Either a b -sigmaToEither = \case - Sigma A a -> Left a - Sigma B b -> Right b - --- | A potentially uncountable collection of tags for the same unit @()@ payload. -data Many a b where - Many :: a -> Many a () - -many :: a -> Sigma (Many a) -many a = Sigma (Many a) () - --- | Hide the type of the payload a tag. --- --- There is a whole library dedicated to this nice little GADT: --- http://hackage.haskell.org/package/some. -data Some t where - Some :: t a -> Some t - --- | A class of tags with no constraint. -class Unconstrained (t :: * -> *) where - -instance Unconstrained Zero where -instance Unconstrained (One a) where -instance Unconstrained (Two a b) where -instance Unconstrained (Many a) where - --- | A class of tags that can be enumerated. --- --- A valid instance must list every tag in the resulting list exactly once. -class Unconstrained t => Countable t where - enumerate :: [Some t] - -instance Countable Zero where - enumerate = [] - -instance Countable (One a) where - enumerate = [Some single] - -instance Countable (Two a b) where - enumerate = [Some A, Some B] - --- | Like 'Countable' but the list has finite length. -class Countable t => Finite t where - -instance Finite Zero where -instance Finite (One a) where -instance Finite (Two a b) where - --- | Like 'Finite' but the list has length equal to one, so @enumerate@ must be --- equal to @[Some single]@. -class Finite t => Single t where - type Payload t - single :: t (Payload t) - matchSingle :: Sigma t -> Payload t - -instance Single (One a) where - type Payload (One a) = a - single = One - matchSingle (Sigma One x) = x - --- | Generalised pattern matching on a Sigma type using a Pi type to describe --- how to handle each case. -matchPure :: Sigma t -> (forall x. t x -> x -> a) -> a -matchPure (Sigma t x) pi = pi t x - --- | A type class that allows lifting 'matchPure' into an effect 'f'. -class Functor f => Match f where - type Tag f :: (* -> *) -> Constraint - pure :: a -> f a - match :: Tag f t => f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a - -fmapLike :: (Match f, Tag f (One a)) => a -> f (a -> b) -> f b -fmapLike a f = match (pure (Sigma One a)) (\One -> f) - -apply :: (Match f, Tag f (One a)) => f (a -> b) -> f a -> f b -apply f x = match (Sigma One <$> x) (\One -> f) - -select :: (Match f, Tag f (Two a b)) => f (Either a b) -> f (a -> b) -> f b -select x f = match (eitherToSigma <$> x) $ \case - A -> f - B -> pure id - -bind :: (Match f, Tag f (Many a)) => f a -> (a -> f b) -> f b -bind x f = match (many <$> x) (\(Many x) -> const <$> f x) - --- | Any applicative can be given a 'Match' instance. -newtype MatchA f a = MatchA { getMatchA :: f a } - deriving (Functor, Applicative) - -instance Applicative f => Match (MatchA f) where - type Tag (MatchA f) = Single - pure = pure - match = matchA - --- | Any monad can be given a 'Match' instance. -newtype MatchM f a = MatchM { getMatchM :: f a } - deriving (Functor, Applicative, Monad) - -instance Monad f => Match (MatchM f) where - type Tag (MatchM f) = Unconstrained - pure = return - match = matchM - -matchA :: (Applicative f, Single t) => f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a -matchA sigma pi = matchSingle <$> sigma <**> pi single - -instance Monoid m => Match (Const m) where - type Tag (Const m) = Single - pure _ = Const mempty - match (Const x) pi = Const (mappend x y) - where - y = getConst (pi single) - -matchM :: Monad f => f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a -matchM sigma pi = sigma >>= \(Sigma t x) -> ($x) <$> pi t - -instance Match Maybe where - type Tag Maybe = Unconstrained - pure = Just - match = matchM diff --git a/src/Control/Match/Arrow.hs b/src/Control/Match/Arrow.hs deleted file mode 100644 index c6c2696..0000000 --- a/src/Control/Match/Arrow.hs +++ /dev/null @@ -1,149 +0,0 @@ -{-# LANGUAGE DeriveFunctor, TypeFamilies, GADTs, RankNTypes #-} -{-# LANGUAGE GeneralizedNewtypeDeriving, ScopedTypeVariables, LambdaCase #-} ------------------------------------------------------------------------------ --- | --- Module : Control.Match.Arrow --- Copyright : (c) Andrey Mokhov 2018-2020 --- License : MIT (see the file LICENSE) --- Maintainer : andrey.mokhov@gmail.com --- Stability : experimental --- --- An experiment in expressing arrows using the Match type class. ------------------------------------------------------------------------------ -module Control.Match.Arrow where - -import Control.Category -import Data.Kind -import Prelude hiding (id, (.)) - --- | A generalised sum type where @t@ stands for the type of constructor "tags". --- Each tag has a type parameter @x@ which determines the type of the payload. --- A 'Sigma' @t@ value therefore contains a payload whose type is not visible --- externally but is revealed when pattern-matching on the tag. --- --- See 'Two', 'eitherToSigma' and 'sigmaToEither' for an example. -data Sigma t where - Sigma :: t x -> x -> Sigma t - --- | A data type defining no tags. Similar to 'Data.Void.Void' but parameterised. -data Zero a where - --- | A data type with a single tag. This data type is commonly known as @Refl@, --- see "Data.Type.Equality". -data One a b where - One :: One a a - --- | A data type with two tags 'A' and 'B' that allows us to encode the good old --- 'Either' as 'Sigma' 'Two', where the tags 'A' and 'B' correspond to 'Left' --- and 'Right', respectively. See 'eitherToSigma' and 'sigmaToEither' that --- witness the isomorphism between 'Either' @a b@ and 'Sigma' @(@'Two'@ a b)@. -data Two a b c where - A :: Two a b a - B :: Two a b b - --- | Encode 'Either' into a generalised sum type. -eitherToSigma :: Either a b -> Sigma (Two a b) -eitherToSigma = \case - Left a -> Sigma A a - Right b -> Sigma B b - --- | Decode 'Either' from a generalised sum type. -sigmaToEither :: Sigma (Two a b) -> Either a b -sigmaToEither = \case - Sigma A a -> Left a - Sigma B b -> Right b - --- | A potentially uncountable collection of tags for the same unit @()@ payload. -data Many a b where - Many :: a -> Many a () - -many :: a -> Sigma (Many a) -many a = Sigma (Many a) () - --- | Hide the type of the payload a tag. --- --- There is a whole library dedicated to this nice little GADT: --- http://hackage.haskell.org/package/some. -data Some t where - Some :: t a -> Some t - --- | A class of tags with no constraint. -class Unconstrained (t :: * -> *) where - -instance Unconstrained Zero where -instance Unconstrained (One a) where -instance Unconstrained (Two a b) where -instance Unconstrained (Many a) where - --- | A class of tags that can be enumerated. --- --- A valid instance must list every tag in the resulting list exactly once. -class Unconstrained t => Countable t where - enumerate :: [Some t] - -instance Countable Zero where - enumerate = [] - -instance Countable (One a) where - enumerate = [Some single] - -instance Countable (Two a b) where - enumerate = [Some A, Some B] - --- | Like 'Countable' but the list has finite length. -class Countable t => Finite t where - -instance Finite Zero where -instance Finite (One a) where -instance Finite (Two a b) where - --- | Like 'Finite' but the list has length equal to one, so @enumerate@ must be --- equal to @[Some single]@. -class Finite t => Single t where - type Payload t - single :: t (Payload t) - matchSingle :: Sigma t -> Payload t - -instance Single (One a) where - type Payload (One a) = a - single = One - matchSingle (Sigma One x) = x - --- | Generalised pattern matching on a Sigma type using a Pi type to describe --- how to handle each case. -matchPure :: Sigma t -> (forall x. t x -> x -> a) -> a -matchPure (Sigma t x) pi = pi t x - --- | A type class that allows lifting 'matchPure' into an arrow 'a'. -class Category a => Match a where - type Tag a :: (* -> *) -> Constraint - arr :: (i -> o) -> a i o - match :: Tag a t => a i (Sigma t) -> (forall x. t x -> a x o) -> a i o - --- Interestingly, this matches the type Mono from this blog post: --- https://elvishjerricco.github.io/2017/03/23/applicative-sorting.html -data ManyT a b c where - ManyT :: a -> ManyT a b b - --- This seems unsatisfactory -first :: (Match a, Tag a (ManyT x i)) => a i o -> a (i, x) (o, x) -first a = match (arr $ \(i, x) -> Sigma (ManyT x) i) $ - \case ManyT x -> arr (\o -> (o, x)) . a - -left :: (Match a, Tag a (Two i x)) => a i o -> a (Either i x) (Either o x) -left a = match (arr eitherToSigma) $ \case - A -> arr Left . a - B -> arr Right - -right :: (Match a, Tag a (Two x i)) => a i o -> a (Either x i) (Either x o) -right a = match (arr eitherToSigma) $ \case - A -> arr Left - B -> arr Right . a - -(|||) :: (Match a, Tag a (Two i1 i2)) => a i1 o1 -> a i2 o2 -> a (Either i1 i2) (Either o1 o2) -(|||) a b = match (arr eitherToSigma) $ \case - A -> arr Left . a - B -> arr Right . b - -app :: (Match a, Tag a (ManyT (a i o) i)) => a (a i o, i) o -app = match (arr $ \(a, i) -> Sigma (ManyT a) i) $ \case ManyT x -> x diff --git a/src/Control/Match/Profunctor.hs b/src/Control/Match/Profunctor.hs deleted file mode 100644 index b314957..0000000 --- a/src/Control/Match/Profunctor.hs +++ /dev/null @@ -1,158 +0,0 @@ -{-# LANGUAGE DeriveFunctor, TypeFamilies, GADTs, RankNTypes #-} -{-# LANGUAGE GeneralizedNewtypeDeriving, ScopedTypeVariables, LambdaCase #-} ------------------------------------------------------------------------------ --- | --- Module : Control.Match.Profunctor --- Copyright : (c) Andrey Mokhov 2018-2020 --- License : MIT (see the file LICENSE) --- Maintainer : andrey.mokhov@gmail.com --- Stability : experimental --- --- An experiment in expressing profunctors using the Match type class. ------------------------------------------------------------------------------ -module Control.Match.Profunctor where - -import Data.Kind -import Prelude hiding (id, (.)) -import qualified Prelude - --- | A generalised sum type where @t@ stands for the type of constructor "tags". --- Each tag has a type parameter @x@ which determines the type of the payload. --- A 'Sigma' @t@ value therefore contains a payload whose type is not visible --- externally but is revealed when pattern-matching on the tag. --- --- See 'Two', 'eitherToSigma' and 'sigmaToEither' for an example. -data Sigma t where - Sigma :: t x -> x -> Sigma t - --- | A data type defining no tags. Similar to 'Data.Void.Void' but parameterised. -data Zero a where - --- | A data type with a single tag. This data type is commonly known as @Refl@, --- see "Data.Type.Equality". -data One a b where - One :: One a a - --- | A data type with two tags 'A' and 'B' that allows us to encode the good old --- 'Either' as 'Sigma' 'Two', where the tags 'A' and 'B' correspond to 'Left' --- and 'Right', respectively. See 'eitherToSigma' and 'sigmaToEither' that --- witness the isomorphism between 'Either' @a b@ and 'Sigma' @(@'Two'@ a b)@. -data Two a b c where - A :: Two a b a - B :: Two a b b - --- | Encode 'Either' into a generalised sum type. -eitherToSigma :: Either a b -> Sigma (Two a b) -eitherToSigma = \case - Left a -> Sigma A a - Right b -> Sigma B b - --- | Decode 'Either' from a generalised sum type. -sigmaToEither :: Sigma (Two a b) -> Either a b -sigmaToEither = \case - Sigma A a -> Left a - Sigma B b -> Right b - --- | A potentially uncountable collection of tags for the same unit @()@ payload. -data Many a b where - Many :: a -> Many a () - -many :: a -> Sigma (Many a) -many a = Sigma (Many a) () - --- | Hide the type of the payload a tag. --- --- There is a whole library dedicated to this nice little GADT: --- http://hackage.haskell.org/package/some. -data Some t where - Some :: t a -> Some t - --- | A class of tags with no constraint. -class Unconstrained (t :: * -> *) where - -instance Unconstrained Zero where -instance Unconstrained (One a) where -instance Unconstrained (Two a b) where -instance Unconstrained (Many a) where - --- | A class of tags that can be enumerated. --- --- A valid instance must list every tag in the resulting list exactly once. -class Unconstrained t => Countable t where - enumerate :: [Some t] - -instance Countable Zero where - enumerate = [] - -instance Countable (One a) where - enumerate = [Some single] - -instance Countable (Two a b) where - enumerate = [Some A, Some B] - --- | Like 'Countable' but the list has finite length. -class Countable t => Finite t where - -instance Finite Zero where -instance Finite (One a) where -instance Finite (Two a b) where - --- | Like 'Finite' but the list has length equal to one, so @enumerate@ must be --- equal to @[Some single]@. -class Finite t => Single t where - type Payload t - single :: t (Payload t) - matchSingle :: Sigma t -> Payload t - -instance Single (One a) where - type Payload (One a) = a - single = One - matchSingle (Sigma One x) = x - --- | Generalised pattern matching on a Sigma type using a Pi type to describe --- how to handle each case. -matchPure :: Sigma t -> (forall x. t x -> x -> a) -> a -matchPure (Sigma t x) pi = pi t x - - -class Profunctor p where - dimap :: (a -> b) -> (c -> d) -> p b c -> p a d - - lmap :: (a -> b) -> p b c -> p a c - lmap f = dimap f Prelude.id - - rmap :: (b -> c) -> p a b -> p a c - rmap = dimap Prelude.id - --- | A type class that allows lifting 'matchPure' into a profunctor 'p'. -class Profunctor p => Match p where - type Tag p :: (* -> *) -> Constraint - id :: p a a - match :: Tag p t => p a (Sigma t) -> (forall x. t x -> p x b) -> p a b - --- We have a category -arr :: Match p => (a -> b) -> p a b -arr f = rmap f id - -(.) :: (Match p, Tag p (One b)) => p b c -> p a b -> p a c -(.) x y = match (rmap (Sigma One) y) $ \case One -> x - --- Interestingly, this matches the type Mono from this blog post: --- https://elvishjerricco.github.io/2017/03/23/applicative-sorting.html -data ManyT a b c where - ManyT :: a -> ManyT a b b - --- This seems unsatisfactory -first :: (Match p, Tag p (One b), Tag p (ManyT x a)) => p a b -> p (a, x) (b, x) -first p = match (arr $ \(a, x) -> Sigma (ManyT x) a) $ - \case ManyT x -> arr (\b -> (b, x)) . p - -left :: (Match p, Tag p (One b), Tag p (Two a x)) => p a b -> p (Either a x) (Either b x) -left p = match (arr eitherToSigma) $ \case - A -> arr Left . p - B -> arr Right - -right :: (Match p, Tag p (One b), Tag p (Two x a)) => p a b -> p (Either x a) (Either x b) -right p = match (arr eitherToSigma) $ \case - A -> arr Left - B -> arr Right . p diff --git a/src/Control/United.hs b/src/Control/United.hs deleted file mode 100644 index c29d022..0000000 --- a/src/Control/United.hs +++ /dev/null @@ -1,92 +0,0 @@ -{-# LANGUAGE ConstraintKinds, MultiParamTypeClasses, FunctionalDependencies #-} -{-# LANGUAGE EmptyCase, LambdaCase, GADTs, RankNTypes, ScopedTypeVariables #-} ------------------------------------------------------------------------------ --- | --- Module : Control.United --- Copyright : (c) Andrey Mokhov 2018-2020 --- License : MIT (see the file LICENSE) --- Maintainer : andrey.mokhov@gmail.com --- Stability : experimental --- --- An experiment in expressing Functor, Applicative, Selective and Monad using --- the United type class, which combines Match and Batch type classes into one. --- The name reflects the fact that the methods @match@ and @batch@ form a united --- monoid in the category of endofunctors. ------------------------------------------------------------------------------ -module Control.United where - -import Data.Function -import Prelude hiding (fmap, pure) - --- | A generalised sum type where @t@ stands for the type of constructor "tags". --- Each tag has a type parameter @x@ which determines the type of the payload. -data Sigma t a where - Sigma :: t x -> (x -> a) -> Sigma t a - --- | A data type defining no tags. Similar to 'Data.Void.Void' but parameterised. -data Zero a where - --- | A data type with a single tag. This data type is commonly known as @Refl@, --- see "Data.Type.Equality". -data One a b where - One :: One a a - --- | A data type with two tags 'A' and 'B' that allows us to encode the good old --- 'Either' as 'Sigma' 'Two', where the tags 'A' and 'B' correspond to 'Left' --- and 'Right', respectively. See 'eitherToSigma' and 'sigmaToEither' that --- witness the isomorphism between 'Either' @a b@ and 'Sigma' @(@'Two'@ a b)@. -data Two a b c where - A :: Two a b a - B :: Two a b b - --- Interestingly, this matches the type Mono from this blog post: --- https://elvishjerricco.github.io/2017/03/23/applicative-sorting.html --- | A potentially uncountable collection of tags. -data Many a b c where - Many :: a -> Many a b b - -type Aggregator t a = ((forall x. t x -> x) -> a) - -data Selector f t a where - Z :: Selector f Zero a - O :: (x -> a) -> Selector f (One x) a - S :: (x -> Sigma t a) -> f x -> Selector f t a - -class United p q f | f -> p q where - batch :: p t => Aggregator t a -> (forall x. t x -> f x) -> f a - match :: q t => Selector f t a -> (forall x. t x -> f x) -> f a - --- | This is the unit of both 'batch' and 'match'. -pure :: (United p q f, p Zero) => a -> f a -pure a = batch (const a) (\(x :: Zero a) -> case x of {}) - -mapBatch :: (United p q f, p (One a)) => (a -> b) -> f a -> f b -mapBatch f x = batch (\lookup -> f (lookup One)) (\One -> x) - -mult :: (United p q f, p (Two a b)) => f a -> f b -> f (a, b) -mult x y = batch (\lookup -> (lookup A, lookup B)) $ \case { A -> x; B -> y } - -mfix :: (United p q f, p (Many a a)) => (a -> f a) -> f a -mfix f = batch (\lookup -> fix (lookup . Many)) (\(Many a) -> f a) - --- United monoids have the same zero: --- 0 * x = 0 => 0 + x = 0 * x + x = 0 * x = 0 --- 0 + x = 0 => 0 * x = 0 * x + 0 = 0 -empty :: (United p q f, q Zero) => f a -empty = match Z (\(x :: Zero a) -> case x of {}) - -mapMatch :: (United p q f, q (One a)) => (a -> b) -> f a -> f b -mapMatch f x = match (O f) (\One -> x) - -branch :: (United p q f, q (Two (a -> c) (b -> c))) => f (Either a b) -> f (a -> c) -> f (b -> c) -> f c -branch x f g = match (S toSigma x) $ \case - A -> f - B -> g - where - toSigma (Left a) = Sigma A ($a) - toSigma (Right b) = Sigma B ($b) - -bind :: (United p q f, q (Many a b)) => f a -> (a -> f b) -> f b -bind x f = match (S toSigma x) (\(Many x) -> f x) - where - toSigma a = Sigma (Many a) id