Copyright  (c) Andrey Mokhov 20182020 

License  MIT (see the file LICENSE) 
Maintainer  andrey.mokhov@gmail.com 
Stability  experimental 
Safe Haskell  Safe 
Language  Haskell2010 
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://www.staff.ncl.ac.uk/andrey.mokhov/selectivefunctors.pdf.
This module defines multiway 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
Synopsis
 data Sigma t where
 inject :: t x > x > Sigma t
 data Zero a
 data One a b where
 data Two a b c where
 data Many a b where
 many :: a > Sigma (Many a)
 matchPure :: Sigma t > (forall x. t x > x > a) > a
 eitherToSigma :: Either a b > Sigma (Two a b)
 sigmaToEither :: Sigma (Two a b) > Either a b
 data Some t where
 class Enumerable t where
 class Applicative f => Selective f where
 match :: Enumerable t => f (Sigma t) > (forall x. t x > f (x > a)) > f a
 newtype Over m a = Over {
 getOver :: m
 newtype Under m a = Under {
 getUnder :: m
 select :: Selective f => f (Either a b) > f (a > b) > f b
 branch :: Selective f => f (Either a b) > f (a > c) > f (b > c) > f c
 apS :: Selective f => f a > f (a > b) > f b
 bindS :: (Enum a, Selective f) => f a > (a > f b) > f b
 class Functor f => ApplicativeS f where
 ap :: ApplicativeS f => f a > f (a > b) > f b
 matchA :: (Applicative f, t ~ One x) => f (Sigma t) > (forall x. t x > f (x > a)) > f a
 class Applicative f => MonadS f where
 matchUnconstrained :: f (Sigma t) > (forall x. t x > f (x > a)) > f a
 bind :: MonadS f => f a > (a > f b) > f b
 matchM :: Monad f => f (Sigma t) > (forall x. t x > f (x > a)) > f a
 type (~>) t u = forall x. t x > u x
 type Pi t = t ~> Identity
 project :: t a > Pi t > a
 identity :: t ~> t
 compose :: (u ~> v) > (t ~> u) > t ~> v
 apply :: (t ~> u) > Sigma t > Sigma u
 toSigma :: a > Sigma (One a)
 fromSigma :: Sigma (One a) > a
 toPi :: a > Pi (One a)
 fromPi :: Pi (One a) > a
 pairToPi :: (a, b) > Pi (Two a b)
 piToPair :: Pi (Two a b) > (a, b)
 newtype Case f a x = Case {
 handleCase :: f (x > a)
 matchCases :: Functor f => Sigma t > (t ~> Case f a) > f a
Generalised sum types
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 patternmatching on the tag.
See Two
, eitherToSigma
and sigmaToEither
for an example.
A data type defining no tags. Similar to Void
but parameterised.
Instances
Enumerable Zero Source #  
A data type with a single tag. This data type is commonly known as Refl
,
see Data.Type.Equality.
Instances
Enumerable (One a) Source #  
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)
.
Instances
Enumerable (Two a b) Source #  
A potentially uncountable collection of tags for the same unit ()
payload.
matchPure :: Sigma t > (forall x. t x > x > a) > a Source #
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
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.
class Enumerable t where Source #
A class of tags that can be enumerated.
A valid instance must list every tag in the resulting list exactly once.
Instances
Enumerable Zero Source #  
Enum a => Enumerable (Many a) Source #  
Enumerable (One a) Source #  
Enumerable (Two a b) Source #  
class Applicative f => Selective f where Source #
Multiway 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
match :: Enumerable t => f (Sigma t) > (forall x. t x > f (x > a)) > f a Source #
Static analysis of selective functors with overapproximation.
Static analysis of selective functors with underapproximation.
select :: Selective f => f (Either a b) > f (a > b) > f b Source #
The basic "ifthen" selection primitive from Control.Selective.
branch :: Selective f => f (Either a b) > f (a > c) > f (b > c) > f c Source #
Choose a matching effect with Either
.
bindS :: (Enum a, Selective f) => f a > (a > f b) > f b Source #
A restricted version of monadic bind.
Applicative functors
class Functor f => ApplicativeS f where Source #
ap :: ApplicativeS f => f a > f (a > b) > f b Source #
matchA :: (Applicative f, t ~ One x) => f (Sigma t) > (forall x. t x > f (x > a)) > f a Source #
Every Applicative
is also an ApplicativeS
.
Monads
class Applicative f => MonadS f where Source #
An alternative definition of monads, as witnessed by bind
and matchM
.
This class is almost like Selective
but has no the constraint on t
.
matchUnconstrained :: f (Sigma t) > (forall x. t x > f (x > a)) > f a Source #
matchM :: Monad f => f (Sigma t) > (forall x. t x > f (x > a)) > f a Source #
Every monad is a multiway selective functor.
Generalised products and various combinators
type Pi t = t ~> Identity Source #
A product type where the payload has the type specified with the tag.
A trivial product type that stores nothing and simply returns the given tag as the result.
compose :: (u ~> v) > (t ~> u) > t ~> v Source #
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.
apply :: (t ~> u) > Sigma t > Sigma u Source #
Update a generalised sum given a generalised product that takes care of all possible cases.
toSigma :: a > Sigma (One a) Source #
Encode a value into a generalised sum type that has a single tag One
.
fromSigma :: Sigma (One a) > a Source #
Decode a value from a generalised sum type that has a single tag One
.
toPi :: a > Pi (One a) Source #
Encode a value into a generalised product type that has a single tag One
.
fromPi :: Pi (One a) > a Source #
Decode a value from a generalised product type that has a single tag One
.
Handler of a single case in a generalised pattern matching matchCases
.
Case  
