{-# 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)