Copyright	(c) Andrey Mokhov 2018-2020
License	MIT (see the file LICENSE)
Maintainer	andrey.mokhov@gmail.com
Stability	experimental
Safe Haskell	Safe-Inferred
Language	Haskell2010

Control.Selective.Multi

Contents

Generalised sum types
Selective functors
Applicative functors
Monads
Generalised products and various combinators

Description

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/selective-functors.pdf .

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

Synopsis

data Sigma t where
- Sigma :: t x -> x -> Sigma t
inject :: t x -> x -> Sigma t
data Zero a
data One a b where
- One :: One a a
data Two a b c where
- A :: Two a b a
- B :: Two a b b
data Many a b where
- Many :: a -> Many a ()
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
- Some :: t a -> Some t
class Enumerable t where
- enumerate :: [ Some t]
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
- pureA :: a -> f a
- matchOne :: t ~ One x => f ( Sigma t) -> ( forall x. t x -> f (x -> a)) -> f a
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

data Sigma t where Source #

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.

Constructors

Sigma :: t x -> x -> Sigma t

inject :: t x -> x -> Sigma t Source #

An injection into a generalised sum. An alias for Sigma .

data Zero a Source #

A data type defining no tags. Similar to Void but parameterised.

Instances

Instances details

Enumerable Zero Source #
Instance details Defined in Control.Selective.Multi Methods enumerate :: [ Some Zero ] Source #

data One a b where Source #

A data type with a single tag. This data type is commonly known as Refl , see Data.Type.Equality .

Constructors

One :: One a a

Instances

Instances details

Enumerable ( One a) Source #
Instance details Defined in Control.Selective.Multi Methods enumerate :: [ Some ( One a)] Source #

data Two a b c where 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) .

Constructors

A :: Two a b a
B :: Two a b b

Instances

Instances details

Enumerable ( Two a b) Source #
Instance details Defined in Control.Selective.Multi Methods enumerate :: [ Some ( Two a b)] Source #

data Many a b where Source #

A potentially uncountable collection of tags for the same unit () payload.

Constructors

Many :: a -> Many a ()

Instances

Instances details

Enum a => Enumerable ( Many a) Source #
Instance details Defined in Control.Selective.Multi Methods enumerate :: [ Some ( Many a)] Source #

many :: a -> Sigma ( Many a) Source #

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

We chose to simplify it by inlining ~> , Case and Identity .

eitherToSigma :: Either a b -> Sigma ( Two a b) Source #

Encode Either into a generalised sum type.

sigmaToEither :: Sigma ( Two a b) -> Either a b Source #

Decode Either from a generalised sum type.

Selective functors

data Some t where Source #

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 .

Constructors

Some :: t a -> Some t

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.

Methods

enumerate :: [ Some t] Source #

Instances

Instances details

Enumerable Zero Source #
Instance details Defined in Control.Selective.Multi Methods enumerate :: [ Some Zero ] Source #
Enum a => Enumerable ( Many a) Source #
Instance details Defined in Control.Selective.Multi Methods enumerate :: [ Some ( Many a)] Source #
Enumerable ( One a) Source #
Instance details Defined in Control.Selective.Multi Methods enumerate :: [ Some ( One a)] Source #
Enumerable ( Two a b) Source #
Instance details Defined in Control.Selective.Multi Methods enumerate :: [ Some ( Two a b)] Source #

class Applicative f => Selective f where Source #

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 .

Methods

match :: Enumerable t => f ( Sigma t) -> ( forall x. t x -> f (x -> a)) -> f a Source #

Instances

Instances details

Monoid m => Selective ( Under m) Source #
Instance details Defined in Control.Selective.Multi Methods match :: Enumerable t => Under m ( Sigma t) -> ( forall x. t x -> Under m (x -> a)) -> Under m a Source #
Monoid m => Selective ( Over m) Source #
Instance details Defined in Control.Selective.Multi Methods match :: Enumerable t => Over m ( Sigma t) -> ( forall x. t x -> Over m (x -> a)) -> Over m a Source #

newtype Over m a Source #

Static analysis of selective functors with over-approximation.

Constructors

Over
Fields getOver :: m

Instances

Instances details

Functor ( Over m) Source #
Instance details Defined in Control.Selective.Multi Methods fmap :: (a -> b) -> Over m a -> Over m b Source # (<$) :: a -> Over m b -> Over m a Source #
Monoid m => Applicative ( Over m) Source #
Instance details Defined in Control.Selective.Multi Methods pure :: a -> Over m a Source # (<>) :: Over m (a -> b) -> Over m a -> Over m b Source # liftA2 :: (a -> b -> c) -> Over m a -> Over m b -> Over m c Source # (>) :: Over m a -> Over m b -> Over m b Source # (<*) :: Over m a -> Over m b -> Over m a Source #
Monoid m => Selective ( Over m) Source #
Instance details Defined in Control.Selective.Multi Methods match :: Enumerable t => Over m ( Sigma t) -> ( forall x. t x -> Over m (x -> a)) -> Over m a Source #
Eq m => Eq ( Over m a) Source #
Instance details Defined in Control.Selective.Multi Methods (==) :: Over m a -> Over m a -> Bool Source # (/=) :: Over m a -> Over m a -> Bool Source #
Ord m => Ord ( Over m a) Source #
Instance details Defined in Control.Selective.Multi Methods compare :: Over m a -> Over m a -> Ordering Source # (<) :: Over m a -> Over m a -> Bool Source # (<=) :: Over m a -> Over m a -> Bool Source # (>) :: Over m a -> Over m a -> Bool Source # (>=) :: Over m a -> Over m a -> Bool Source # max :: Over m a -> Over m a -> Over m a Source # min :: Over m a -> Over m a -> Over m a Source #
Show m => Show ( Over m a) Source #
Instance details Defined in Control.Selective.Multi Methods showsPrec :: Int -> Over m a -> ShowS Source # show :: Over m a -> String Source # showList :: [ Over m a] -> ShowS Source #

newtype Under m a Source #

Static analysis of selective functors with under-approximation.

Constructors

Under
Fields getUnder :: m

Instances

Instances details

Functor ( Under m) Source #
Instance details Defined in Control.Selective.Multi Methods fmap :: (a -> b) -> Under m a -> Under m b Source # (<$) :: a -> Under m b -> Under m a Source #
Monoid m => Applicative ( Under m) Source #
Instance details Defined in Control.Selective.Multi Methods pure :: a -> Under m a Source # (<>) :: Under m (a -> b) -> Under m a -> Under m b Source # liftA2 :: (a -> b -> c) -> Under m a -> Under m b -> Under m c Source # (>) :: Under m a -> Under m b -> Under m b Source # (<*) :: Under m a -> Under m b -> Under m a Source #
Monoid m => Selective ( Under m) Source #
Instance details Defined in Control.Selective.Multi Methods match :: Enumerable t => Under m ( Sigma t) -> ( forall x. t x -> Under m (x -> a)) -> Under m a Source #
Eq m => Eq ( Under m a) Source #
Instance details Defined in Control.Selective.Multi Methods (==) :: Under m a -> Under m a -> Bool Source # (/=) :: Under m a -> Under m a -> Bool Source #
Ord m => Ord ( Under m a) Source #
Instance details Defined in Control.Selective.Multi Methods compare :: Under m a -> Under m a -> Ordering Source # (<) :: Under m a -> Under m a -> Bool Source # (<=) :: Under m a -> Under m a -> Bool Source # (>) :: Under m a -> Under m a -> Bool Source # (>=) :: Under m a -> Under m a -> Bool Source # max :: Under m a -> Under m a -> Under m a Source # min :: Under m a -> Under m a -> Under m a Source #
Show m => Show ( Under m a) Source #
Instance details Defined in Control.Selective.Multi Methods showsPrec :: Int -> Under m a -> ShowS Source # show :: Under m a -> String Source # showList :: [ Under m a] -> ShowS Source #

select :: Selective f => f ( Either a b) -> f (a -> b) -> f b Source #

The basic "if-then" 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 .

apS :: Selective f => f a -> f (a -> b) -> f b Source #

Recover the application operator <*> from match .

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 #

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 .

Methods

pureA :: a -> f a Source #

matchOne :: t ~ One x => f ( Sigma t) -> ( forall x. t x -> f (x -> a)) -> f a Source #

ap :: ApplicativeS f => f a -> f (a -> b) -> f b Source #

Recover the application operator <*> from matchOne .

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 .

Methods

matchUnconstrained :: f ( Sigma t) -> ( forall x. t x -> f (x -> a)) -> f a Source #

bind :: MonadS f => f a -> (a -> f b) -> f b Source #

Monadic bind.

matchM :: Monad f => f ( Sigma t) -> ( forall x. t x -> f (x -> a)) -> f a Source #

Every monad is a multi-way selective functor.

Generalised products and various combinators

type (~>) t u = forall x. t x -> u x infixl 4 Source #

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 Pi t = t ~> Identity Source #

A product type where the payload has the type specified with the tag.

project :: t a -> Pi t -> a Source #

A projection from a generalised product.

identity :: t ~> t Source #

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 .

pairToPi :: (a, b) -> Pi ( Two a b) Source #

Encode (a, b) into a generalised product type.