Control.Selective.Multi

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.

Recover the application operator <*> from matchOne.

Recover the application operator <*> from match.

A restricted version of monadic bind.

Choose a matching effect with Either.

Every monad is a multi-way selective functor.

Static analysis of selective functors with over-approximation.

The basic "if-then" selection primitive from Control.Selective.

Static analysis of selective functors with under-approximation.

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

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

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.

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).

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

Update a generalised sum given a generalised product that takes care of all possible cases.

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.

Monadic bind.

Encode Either into a generalised sum type.

Decode a value from a generalised product type that has a single tag One.

Decode a value from a generalised sum type that has a single tag One.

A trivial product type that stores nothing and simply returns the given tag as the result.

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

Every Applicative is also an ApplicativeS.

Generalised pattern matching on a Sigma type using a Pi type to describe how to handle each case.

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.

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

Decode (a, b) from a generalised product type.

A projection from a generalised product.

Decode Either from a generalised sum type.

Encode a value into a generalised product type that has a single tag One.

Encode a value into a generalised sum type that has a single tag One.

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.

Handler of a single case in a generalised pattern matching matchCases.

A class of tags that can be enumerated.

A valid instance must list every tag in the resulting list exactly once.

An alternative definition of monads, as witnessed by bind and matchM. This class is almost like Selective but has no the constraint on t.

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

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.

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.