    {-# LANGUAGE DeriveFunctor, GADTs, RankNTypes, TupleSections, TypeOperators #-}
    {-# LANGUAGE ScopedTypeVariables, LambdaCase #-}
    -----------------------------------------------------------------------------
    -- |
    -- Module     : Control.Selective.Multi
    -- Copyright  : (c) Andrey Mokhov 2018-2024
    -- License    : MIT (see the file LICENSE)
    -- Maintainer : andrey.mokhov@gmail.com
    -- Stability  : experimental
    --
    -- This is a library for /selective applicative functors/, or just
    -- /selective functors/ for short, an abstraction between applicative functors
    -- and monads, introduced in this paper: https://dl.acm.org/doi/10.1145/3341694.
    --
    -- This module defines /multi-way selective functors/, which are more efficient
    -- when selecting from a large number of options. They also fully subsume the
    -- 'Applicative' type class because they allow to express the notion of
    -- independet effects.
    --
    -- This definition is inspired by the following construction by Daniel Peebles,
    -- with the main difference being the added @Enumerable@ constraint:
    -- https://gist.github.com/copumpkin/d5bdbc7afda54ff04049b6bdbcffb67e
    --
    -----------------------------------------------------------------------------
    module Control.Selective.Multi (
        -- * Generalised sum types
        Sigma (..), inject, Zero, One (..), Two (..), Many (..), many, matchPure,
        eitherToSigma, sigmaToEither,

        -- * Selective functors
        Some (..), Enumerable (..), Selective (..), Over (..), Under (..), select,
        branch, apS, bindS,

        -- * Applicative functors
        ApplicativeS (..), ap, matchA,

        -- * Monads
        MonadS (..), bind, matchM,

        -- * Generalised products and various combinators
        type (~>), Pi, project, identity, compose, apply, toSigma, fromSigma, toPi,
        fromPi, pairToPi, piToPair, Case (..), matchCases,
        ) where

    import Control.Applicative ((<**>))
    import Data.Functor.Identity

    ------------------------ Meet two friends: Sigma and Pi ------------------------
    -- | 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

    -- | An injection into a generalised sum. An alias for 'Sigma'.
    inject :: t x -> x -> Sigma t
    inject :: forall (t :: * -> *) x. t x -> x -> Sigma t
    inject = t x -> x -> Sigma t
    forall (t :: * -> *) x. t x -> x -> Sigma t
    Sigma

    -- | 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 :: forall a b. Either a b -> Sigma (Two a b)
    eitherToSigma = \case
        Left  a
    a -> Two a b a -> a -> Sigma (Two a b)
    forall (t :: * -> *) x. t x -> x -> Sigma t
    inject Two a b a
    forall a b. Two a b a
    A a
    a
        Right b
    b -> Two a b b -> b -> Sigma (Two a b)
    forall (t :: * -> *) x. t x -> x -> Sigma t
    inject Two a b b
    forall a b. Two a b b
    B b
    b

    -- | Decode 'Either' from a generalised sum type.
    sigmaToEither :: Sigma (Two a b) -> Either a b
    sigmaToEither :: forall a b. Sigma (Two a b) -> Either a b
    sigmaToEither = \case
        Sigma Two a b x
    A x
    a -> a -> Either a b
    forall a b. a -> Either a b
    Left  a
    x
    a
        Sigma Two a b x
    B x
    b -> b -> Either a b
    forall a b. b -> Either a b
    Right b
    x
    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 :: forall a. a -> Sigma (Many a)
    many a
    a = Many a () -> () -> Sigma (Many a)
    forall (t :: * -> *) x. t x -> x -> Sigma t
    Sigma (a -> Many a ()
    forall a. a -> Many a ()
    Many a
    a) ()

    -- | Generalised pattern matching on a Sigma type using a Pi type to describe
    -- how to handle each case.
    --
    -- This is a specialisation of 'matchCases' for @f = Identity@. We could also
    -- have also given it the following type:
    --
    -- @
    -- matchPure :: Sigma t -> (t ~> Case Identity a) -> a
    -- @
    --
    -- We chose to simplify it by inlining '~>', 'Case' and 'Identity'.
    matchPure :: Sigma t -> (forall x. t x -> x -> a) -> a
    matchPure :: forall (t :: * -> *) a. Sigma t -> (forall x. t x -> x -> a) -> a
    matchPure (Sigma t x
    t x
    x) forall x. t x -> x -> a
    pi = t x -> x -> a
    forall x. t x -> x -> a
    pi t x
    t x
    x

    ------------------------- Mutli-way selective functors -------------------------
    -- | 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 that can be enumerated.
    --
    -- A valid instance must list every tag in the resulting list exactly once.
    class Enumerable t where
        enumerate :: [Some t]

    instance Enumerable Zero where
        enumerate :: [Some Zero]
    enumerate = []

    instance Enumerable (One a) where
        enumerate :: [Some (One a)]
    enumerate = [One a a -> Some (One a)
    forall (t :: * -> *) a. t a -> Some t
    Some One a a
    forall a. One a a
    One]

    instance Enumerable (Two a b) where
        enumerate :: [Some (Two a b)]
    enumerate = [Two a b a -> Some (Two a b)
    forall (t :: * -> *) a. t a -> Some t
    Some Two a b a
    forall a b. Two a b a
    A, Two a b b -> Some (Two a b)
    forall (t :: * -> *) a. t a -> Some t
    Some Two a b b
    forall a b. Two a b b
    B]

    instance Enum a => Enumerable (Many a) where
        enumerate :: [Some (Many a)]
    enumerate = [ Many a () -> Some (Many a)
    forall (t :: * -> *) a. t a -> Some t
    Some (a -> Many a ()
    forall a. a -> Many a ()
    Many a
    x) | a
    x <- a -> [a]
    forall a. Enum a => a -> [a]
    enumFrom (Int -> a
    forall a. Enum a => Int -> a
    toEnum Int
    0) ]

    -- | Multi-way selective functors. Given a computation that produces a value of
    -- a sum type, we can 'match' it to the corresponding computation in a given
    -- product type.
    --
    -- For greater similarity with 'matchCases', we could have given the following
    -- type to 'match':
    --
    -- @
    -- match :: f (Sigma t) -> (t ~> Case f a) -> f a
    -- @
    --
    -- We chose to simplify it by inlining '~>' and 'Case'.
    class Applicative f => Selective f where
        match :: Enumerable t => f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a

    -- | The basic "if-then" selection primitive from "Control.Selective".
    select :: Selective f => f (Either a b) -> f (a -> b) -> f b
    select :: forall (f :: * -> *) a b.
    Selective f =>
    f (Either a b) -> f (a -> b) -> f b
    select f (Either a b)
    x f (a -> b)
    f = f (Sigma (Two a b)) -> (forall x. Two a b x -> f (x -> b)) -> f b
    forall (f :: * -> *) (t :: * -> *) a.
    (Selective f, Enumerable t) =>
    f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a
    forall (t :: * -> *) a.
    Enumerable t =>
    f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a
    match (Either a b -> Sigma (Two a b)
    forall a b. Either a b -> Sigma (Two a b)
    eitherToSigma (Either a b -> Sigma (Two a b))
    -> f (Either a b) -> f (Sigma (Two a b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f (Either a b)
    x) ((forall x. Two a b x -> f (x -> b)) -> f b)
    -> (forall x. Two a b x -> f (x -> b)) -> f b
    forall a b. (a -> b) -> a -> b
    $ \case
        Two a b x
    A -> f (a -> b)
    f (x -> b)
    f
        Two a b x
    B -> (x -> b) -> f (x -> b)
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure x -> b
    x -> x
    forall a. a -> a
    id

    -- | Choose a matching effect with 'Either'.
    branch :: Selective f => f (Either a b) -> f (a -> c) -> f (b -> c) -> f c
    branch :: forall (f :: * -> *) a b c.
    Selective f =>
    f (Either a b) -> f (a -> c) -> f (b -> c) -> f c
    branch f (Either a b)
    x f (a -> c)
    f f (b -> c)
    g = f (Sigma (Two a b)) -> (forall x. Two a b x -> f (x -> c)) -> f c
    forall (f :: * -> *) (t :: * -> *) a.
    (Selective f, Enumerable t) =>
    f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a
    forall (t :: * -> *) a.
    Enumerable t =>
    f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a
    match (Either a b -> Sigma (Two a b)
    forall a b. Either a b -> Sigma (Two a b)
    eitherToSigma (Either a b -> Sigma (Two a b))
    -> f (Either a b) -> f (Sigma (Two a b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f (Either a b)
    x) ((forall x. Two a b x -> f (x -> c)) -> f c)
    -> (forall x. Two a b x -> f (x -> c)) -> f c
    forall a b. (a -> b) -> a -> b
    $ \case
        Two a b x
    A -> f (a -> c)
    f (x -> c)
    f
        Two a b x
    B -> f (b -> c)
    f (x -> c)
    g

    -- | Recover the application operator '<*>' from 'match'.
    apS :: Selective f => f a -> f (a -> b) -> f b
    apS :: forall (f :: * -> *) a b. Selective f => f a -> f (a -> b) -> f b
    apS f a
    x f (a -> b)
    f = f (Sigma (One a)) -> (forall x. One a x -> f (x -> b)) -> f b
    forall (f :: * -> *) (t :: * -> *) a.
    (Selective f, Enumerable t) =>
    f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a
    forall (t :: * -> *) a.
    Enumerable t =>
    f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a
    match (One a a -> a -> Sigma (One a)
    forall (t :: * -> *) x. t x -> x -> Sigma t
    inject One a a
    forall a. One a a
    One (a -> Sigma (One a)) -> f a -> f (Sigma (One a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f a
    x) (\One a x
    One -> f (a -> b)
    f (x -> b)
    f)

    -- | A restricted version of monadic bind.
    bindS :: (Enum a, Selective f) => f a -> (a -> f b) -> f b
    bindS :: forall a (f :: * -> *) b.
    (Enum a, Selective f) =>
    f a -> (a -> f b) -> f b
    bindS f a
    x a -> f b
    f = f (Sigma (Many a)) -> (forall x. Many a x -> f (x -> b)) -> f b
    forall (f :: * -> *) (t :: * -> *) a.
    (Selective f, Enumerable t) =>
    f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a
    forall (t :: * -> *) a.
    Enumerable t =>
    f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a
    match (a -> Sigma (Many a)
    forall a. a -> Sigma (Many a)
    many (a -> Sigma (Many a)) -> f a -> f (Sigma (Many a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f a
    x) (\(Many a
    x) -> b -> x -> b
    forall a b. a -> b -> a
    const (b -> x -> b) -> f b -> f (x -> b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> f b
    f a
    x)

    -- | Static analysis of selective functors with over-approximation.
    newtype Over m a = Over { forall m a. Over m a -> m
    getOver :: m }
        deriving (Over m a -> Over m a -> Bool
    (Over m a -> Over m a -> Bool)
    -> (Over m a -> Over m a -> Bool) -> Eq (Over m a)
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    forall m a. Eq m => Over m a -> Over m a -> Bool
    $c== :: forall m a. Eq m => Over m a -> Over m a -> Bool
    == :: Over m a -> Over m a -> Bool
    $c/= :: forall m a. Eq m => Over m a -> Over m a -> Bool
    /= :: Over m a -> Over m a -> Bool
    Eq, (forall a b. (a -> b) -> Over m a -> Over m b)
    -> (forall a b. a -> Over m b -> Over m a) -> Functor (Over m)
    forall a b. a -> Over m b -> Over m a
    forall a b. (a -> b) -> Over m a -> Over m b
    forall m a b. a -> Over m b -> Over m a
    forall m a b. (a -> b) -> Over m a -> Over m b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall m a b. (a -> b) -> Over m a -> Over m b
    fmap :: forall a b. (a -> b) -> Over m a -> Over m b
    $c<$ :: forall m a b. a -> Over m b -> Over m a
    <$ :: forall a b. a -> Over m b -> Over m a
    Functor, Eq (Over m a)
    Eq (Over m a) =>
    (Over m a -> Over m a -> Ordering)
    -> (Over m a -> Over m a -> Bool)
    -> (Over m a -> Over m a -> Bool)
    -> (Over m a -> Over m a -> Bool)
    -> (Over m a -> Over m a -> Bool)
    -> (Over m a -> Over m a -> Over m a)
    -> (Over m a -> Over m a -> Over m a)
    -> Ord (Over m a)
    Over m a -> Over m a -> Bool
    Over m a -> Over m a -> Ordering
    Over m a -> Over m a -> Over m a
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    forall m a. Ord m => Eq (Over m a)
    forall m a. Ord m => Over m a -> Over m a -> Bool
    forall m a. Ord m => Over m a -> Over m a -> Ordering
    forall m a. Ord m => Over m a -> Over m a -> Over m a
    $ccompare :: forall m a. Ord m => Over m a -> Over m a -> Ordering
    compare :: Over m a -> Over m a -> Ordering
    $c< :: forall m a. Ord m => Over m a -> Over m a -> Bool
    < :: Over m a -> Over m a -> Bool
    $c<= :: forall m a. Ord m => Over m a -> Over m a -> Bool
    <= :: Over m a -> Over m a -> Bool
    $c> :: forall m a. Ord m => Over m a -> Over m a -> Bool
    > :: Over m a -> Over m a -> Bool
    $c>= :: forall m a. Ord m => Over m a -> Over m a -> Bool
    >= :: Over m a -> Over m a -> Bool
    $cmax :: forall m a. Ord m => Over m a -> Over m a -> Over m a
    max :: Over m a -> Over m a -> Over m a
    $cmin :: forall m a. Ord m => Over m a -> Over m a -> Over m a
    min :: Over m a -> Over m a -> Over m a
    Ord, Int -> Over m a -> ShowS
    [Over m a] -> ShowS
    Over m a -> String
    (Int -> Over m a -> ShowS)
    -> (Over m a -> String) -> ([Over m a] -> ShowS) -> Show (Over m a)
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    forall m a. Show m => Int -> Over m a -> ShowS
    forall m a. Show m => [Over m a] -> ShowS
    forall m a. Show m => Over m a -> String
    $cshowsPrec :: forall m a. Show m => Int -> Over m a -> ShowS
    showsPrec :: Int -> Over m a -> ShowS
    $cshow :: forall m a. Show m => Over m a -> String
    show :: Over m a -> String
    $cshowList :: forall m a. Show m => [Over m a] -> ShowS
    showList :: [Over m a] -> ShowS
    Show)

    instance Monoid m => Applicative (Over m) where
        pure :: forall a. a -> Over m a
    pure a
    _            = m -> Over m a
    forall m a. m -> Over m a
    Over m
    forall a. Monoid a => a
    mempty
        Over m
    x <*> :: forall a b. Over m (a -> b) -> Over m a -> Over m b
    <*> Over m
    y = m -> Over m b
    forall m a. m -> Over m a
    Over (m -> m -> m
    forall a. Monoid a => a -> a -> a
    mappend m
    x m
    y)

    instance Monoid m => Selective (Over m) where
        match :: forall (t :: * -> *) a.
    Enumerable t =>
    Over m (Sigma t) -> (forall x. t x -> Over m (x -> a)) -> Over m a
    match (Over m
    m) forall x. t x -> Over m (x -> a)
    pi = m -> Over m a
    forall m a. m -> Over m a
    Over ([m] -> m
    forall a. Monoid a => [a] -> a
    mconcat (m
    m m -> [m] -> [m]
    forall a. a -> [a] -> [a]
    : [m]
    ms))
          where
            ms :: [m]
    ms = [ Over m (a -> a) -> m
    forall m a. Over m a -> m
    getOver (t a -> Over m (a -> a)
    forall x. t x -> Over m (x -> a)
    pi t a
    t) | Some t a
    t <- [Some t]
    forall (t :: * -> *). Enumerable t => [Some t]
    enumerate ]

    -- | Static analysis of selective functors with under-approximation.
    newtype Under m a = Under { forall m a. Under m a -> m
    getUnder :: m }
        deriving (Under m a -> Under m a -> Bool
    (Under m a -> Under m a -> Bool)
    -> (Under m a -> Under m a -> Bool) -> Eq (Under m a)
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    forall m a. Eq m => Under m a -> Under m a -> Bool
    $c== :: forall m a. Eq m => Under m a -> Under m a -> Bool
    == :: Under m a -> Under m a -> Bool
    $c/= :: forall m a. Eq m => Under m a -> Under m a -> Bool
    /= :: Under m a -> Under m a -> Bool
    Eq, (forall a b. (a -> b) -> Under m a -> Under m b)
    -> (forall a b. a -> Under m b -> Under m a) -> Functor (Under m)
    forall a b. a -> Under m b -> Under m a
    forall a b. (a -> b) -> Under m a -> Under m b
    forall m a b. a -> Under m b -> Under m a
    forall m a b. (a -> b) -> Under m a -> Under m b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall m a b. (a -> b) -> Under m a -> Under m b
    fmap :: forall a b. (a -> b) -> Under m a -> Under m b
    $c<$ :: forall m a b. a -> Under m b -> Under m a
    <$ :: forall a b. a -> Under m b -> Under m a
    Functor, Eq (Under m a)
    Eq (Under m a) =>
    (Under m a -> Under m a -> Ordering)
    -> (Under m a -> Under m a -> Bool)
    -> (Under m a -> Under m a -> Bool)
    -> (Under m a -> Under m a -> Bool)
    -> (Under m a -> Under m a -> Bool)
    -> (Under m a -> Under m a -> Under m a)
    -> (Under m a -> Under m a -> Under m a)
    -> Ord (Under m a)
    Under m a -> Under m a -> Bool
    Under m a -> Under m a -> Ordering
    Under m a -> Under m a -> Under m a
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    forall m a. Ord m => Eq (Under m a)
    forall m a. Ord m => Under m a -> Under m a -> Bool
    forall m a. Ord m => Under m a -> Under m a -> Ordering
    forall m a. Ord m => Under m a -> Under m a -> Under m a
    $ccompare :: forall m a. Ord m => Under m a -> Under m a -> Ordering
    compare :: Under m a -> Under m a -> Ordering
    $c< :: forall m a. Ord m => Under m a -> Under m a -> Bool
    < :: Under m a -> Under m a -> Bool
    $c<= :: forall m a. Ord m => Under m a -> Under m a -> Bool
    <= :: Under m a -> Under m a -> Bool
    $c> :: forall m a. Ord m => Under m a -> Under m a -> Bool
    > :: Under m a -> Under m a -> Bool
    $c>= :: forall m a. Ord m => Under m a -> Under m a -> Bool
    >= :: Under m a -> Under m a -> Bool
    $cmax :: forall m a. Ord m => Under m a -> Under m a -> Under m a
    max :: Under m a -> Under m a -> Under m a
    $cmin :: forall m a. Ord m => Under m a -> Under m a -> Under m a
    min :: Under m a -> Under m a -> Under m a
    Ord, Int -> Under m a -> ShowS
    [Under m a] -> ShowS
    Under m a -> String
    (Int -> Under m a -> ShowS)
    -> (Under m a -> String)
    -> ([Under m a] -> ShowS)
    -> Show (Under m a)
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    forall m a. Show m => Int -> Under m a -> ShowS
    forall m a. Show m => [Under m a] -> ShowS
    forall m a. Show m => Under m a -> String
    $cshowsPrec :: forall m a. Show m => Int -> Under m a -> ShowS
    showsPrec :: Int -> Under m a -> ShowS
    $cshow :: forall m a. Show m => Under m a -> String
    show :: Under m a -> String
    $cshowList :: forall m a. Show m => [Under m a] -> ShowS
    showList :: [Under m a] -> ShowS
    Show)

    instance Monoid m => Applicative (Under m) where
        pure :: forall a. a -> Under m a
    pure a
    _              = m -> Under m a
    forall m a. m -> Under m a
    Under m
    forall a. Monoid a => a
    mempty
        Under m
    x <*> :: forall a b. Under m (a -> b) -> Under m a -> Under m b
    <*> Under m
    y = m -> Under m b
    forall m a. m -> Under m a
    Under (m -> m -> m
    forall a. Monoid a => a -> a -> a
    mappend m
    x m
    y)

    instance Monoid m => Selective (Under m) where
        match :: forall (t :: * -> *) a.
    Enumerable t =>
    Under m (Sigma t)
    -> (forall x. t x -> Under m (x -> a)) -> Under m a
    match (Under m
    m) forall x. t x -> Under m (x -> a)
    _ = m -> Under m a
    forall m a. m -> Under m a
    Under m
    m

    -- | An alternative definition of applicative functors, as witnessed by 'ap' and
    -- 'matchOne'. This class is almost like 'Selective' but has a strict constraint
    -- on @t@.
    class Functor f => ApplicativeS f where
        pureA    :: a -> f a
        matchOne :: t ~ One x => f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a

    -- | Recover the application operator '<*>' from 'matchOne'.
    ap :: ApplicativeS f => f a -> f (a -> b) -> f b
    ap :: forall (f :: * -> *) a b.
    ApplicativeS f =>
    f a -> f (a -> b) -> f b
    ap f a
    x f (a -> b)
    f = f (Sigma (One a)) -> (forall x. One a x -> f (x -> b)) -> f b
    forall (f :: * -> *) (t :: * -> *) x a.
    (ApplicativeS f, t ~ One x) =>
    f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a
    forall (t :: * -> *) x a.
    (t ~ One x) =>
    f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a
    matchOne (One a a -> a -> Sigma (One a)
    forall (t :: * -> *) x. t x -> x -> Sigma t
    Sigma One a a
    forall a. One a a
    One (a -> Sigma (One a)) -> f a -> f (Sigma (One a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f a
    x) (\One a x
    One -> f (a -> b)
    f (x -> b)
    f)

    -- | Every 'Applicative' is also an 'ApplicativeS'.
    matchA :: (Applicative f, t ~ One x) => f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a
    matchA :: forall (f :: * -> *) (t :: * -> *) x a.
    (Applicative f, t ~ One x) =>
    f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a
    matchA f (Sigma t)
    x forall x. t x -> f (x -> a)
    pi = (\(Sigma t x
    One x x
    One x
    x) -> x
    x
    x) (Sigma t -> x) -> f (Sigma t) -> f x
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f (Sigma t)
    x f x -> f (x -> a) -> f a
    forall (f :: * -> *) a b. Applicative f => f a -> f (a -> b) -> f b
    <**> t x -> f (x -> a)
    forall x. t x -> f (x -> a)
    pi t x
    One x x
    forall a. One a a
    One

    -- | An alternative definition of monads, as witnessed by 'bind' and 'matchM'.
    -- This class is almost like 'Selective' but has no the constraint on @t@.
    class Applicative f => MonadS f where
        matchUnconstrained :: f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a

    -- Adapted from the original implementation by Daniel Peebles:
    -- https://gist.github.com/copumpkin/d5bdbc7afda54ff04049b6bdbcffb67e

    -- | Monadic bind.
    bind :: MonadS f => f a -> (a -> f b) -> f b
    bind :: forall (f :: * -> *) a b. MonadS f => f a -> (a -> f b) -> f b
    bind f a
    x a -> f b
    f = f (Sigma (Many a)) -> (forall x. Many a x -> f (x -> b)) -> f b
    forall (f :: * -> *) (t :: * -> *) a.
    MonadS f =>
    f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a
    forall (t :: * -> *) a.
    f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a
    matchUnconstrained (a -> Sigma (Many a)
    forall a. a -> Sigma (Many a)
    many (a -> Sigma (Many a)) -> f a -> f (Sigma (Many a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f a
    x) (\(Many a
    x) -> b -> x -> b
    forall a b. a -> b -> a
    const (b -> x -> b) -> f b -> f (x -> b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> f b
    f a
    x)

    -- | Every monad is a multi-way selective functor.
    matchM :: Monad f => f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a
    matchM :: forall (f :: * -> *) (t :: * -> *) a.
    Monad f =>
    f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a
    matchM f (Sigma t)
    sigma forall x. t x -> f (x -> a)
    pi = f (Sigma t)
    sigma f (Sigma t) -> (Sigma t -> f a) -> f a
    forall a b. f a -> (a -> f b) -> f b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case Sigma t x
    t x
    x -> ((x -> a) -> x -> a
    forall a b. (a -> b) -> a -> b
    $x
    x) ((x -> a) -> a) -> f (x -> a) -> f a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> t x -> f (x -> a)
    forall x. t x -> f (x -> a)
    pi t x
    t

    -- | A generalised product type (Pi), which holds an appropriately tagged
    -- payload @u x@ for every possible tag @t x@.
    --
    -- Note that this looks different than the standard formulation of Pi types.
    -- Maybe it's just all wrong!
    --
    -- See 'Two', 'pairToPi' and 'piToPair' for an example.
    type (~>) t u = forall x. t x -> u x
    infixl 4 ~>

    -- | A product type where the payload has the type specified with the tag.
    type Pi t = t ~> Identity

    -- | A projection from a generalised product.
    project :: t a -> Pi t -> a
    project :: forall (t :: * -> *) a. t a -> Pi t -> a
    project t a
    t Pi t
    pi = Identity a -> a
    forall a. Identity a -> a
    runIdentity (t a -> Identity a
    Pi t
    pi t a
    t)

    -- | A trivial product type that stores nothing and simply returns the given tag
    -- as the result.
    identity :: t ~> t
    identity :: forall (t :: * -> *) x. t x -> t x
    identity = t x -> t x
    forall a. a -> a
    id

    -- | As it turns out, one can compose such generalised products. Why not: given
    -- a tag, get the payload of the first product and then pass it as input to the
    -- second. This feels too trivial to be useful but is still somewhat cute.
    compose :: (u ~> v) -> (t ~> u) -> (t ~> v)
    compose :: forall (u :: * -> *) (v :: * -> *) (t :: * -> *).
    (u ~> v) -> (t ~> u) -> t ~> v
    compose u ~> v
    f t ~> u
    g = u x -> v x
    u ~> v
    f (u x -> v x) -> (t x -> u x) -> t x -> v x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . t x -> u x
    t ~> u
    g

    -- | Update a generalised sum given a generalised product that takes care of all
    -- possible cases.
    apply :: (t ~> u) -> Sigma t -> Sigma u
    apply :: forall (t :: * -> *) (u :: * -> *). (t ~> u) -> Sigma t -> Sigma u
    apply t ~> u
    pi (Sigma t x
    t x
    x) = u x -> x -> Sigma u
    forall (t :: * -> *) x. t x -> x -> Sigma t
    Sigma (t x -> u x
    t ~> u
    pi t x
    t) x
    x

    -- | Encode a value into a generalised sum type that has a single tag 'One'.
    toSigma :: a -> Sigma (One a)
    toSigma :: forall a. a -> Sigma (One a)
    toSigma = One a a -> a -> Sigma (One a)
    forall (t :: * -> *) x. t x -> x -> Sigma t
    inject One a a
    forall a. One a a
    One

    -- | Decode a value from a generalised sum type that has a single tag 'One'.
    fromSigma :: Sigma (One a) -> a
    fromSigma :: forall a. Sigma (One a) -> a
    fromSigma (Sigma One a x
    One x
    a) = a
    x
    a

    -- | Encode a value into a generalised product type that has a single tag 'One'.
    toPi :: a -> Pi (One a)
    toPi :: forall a. a -> Pi (One a)
    toPi a
    a One a x
    One = x -> Identity x
    forall a. a -> Identity a
    Identity a
    x
    a

    -- | Decode a value from a generalised product type that has a single tag 'One'.
    fromPi :: Pi (One a) -> a
    fromPi :: forall a. Pi (One a) -> a
    fromPi = One a a -> Pi (One a) -> a
    forall (t :: * -> *) a. t a -> Pi t -> a
    project One a a
    forall a. One a a
    One

    -- | Encode @(a, b)@ into a generalised product type.
    pairToPi :: (a, b) -> Pi (Two a b)
    pairToPi :: forall a b. (a, b) -> Pi (Two a b)
    pairToPi (a
    a, b
    b) = \case
        Two a b x
    A -> x -> Identity x
    forall a. a -> Identity a
    Identity a
    x
    a
        Two a b x
    B -> x -> Identity x
    forall a. a -> Identity a
    Identity b
    x
    b

    -- | Decode @(a, b)@ from a generalised product type.
    piToPair :: Pi (Two a b) -> (a, b)
    piToPair :: forall a b. Pi (Two a b) -> (a, b)
    piToPair Pi (Two a b)
    pi = (Two a b a -> Pi (Two a b) -> a
    forall (t :: * -> *) a. t a -> Pi t -> a
    project Two a b a
    forall a b. Two a b a
    A Two a b x -> Identity x
    Pi (Two a b)
    pi, Two a b b -> Pi (Two a b) -> b
    forall (t :: * -> *) a. t a -> Pi t -> a
    project Two a b b
    forall a b. Two a b b
    B Two a b x -> Identity x
    Pi (Two a b)
    pi)

    -- | Handler of a single case in a generalised pattern matching 'matchCases'.
    newtype Case f a x = Case { forall (f :: * -> *) a x. Case f a x -> f (x -> a)
    handleCase :: f (x -> a) }

    -- | Generalised pattern matching on a Sigma type using a Pi type to describe
    -- how to handle each case.
    matchCases :: Functor f => Sigma t -> (t ~> Case f a) -> f a
    matchCases :: forall (f :: * -> *) (t :: * -> *) a.
    Functor f =>
    Sigma t -> (t ~> Case f a) -> f a
    matchCases (Sigma t x
    t x
    x) t ~> Case f a
    pi = ((x -> a) -> x -> a
    forall a b. (a -> b) -> a -> b
    $x
    x) ((x -> a) -> a) -> f (x -> a) -> f a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Case f a x -> f (x -> a)
    forall (f :: * -> *) a x. Case f a x -> f (x -> a)
    handleCase (t x -> Case f a x
    t ~> Case f a
    pi t x
    t)