Data.Type.Quantifier

Types for working with (and under) existentially and universally quantified types.

The Some type can be very useful when working with type-indexed GADTs, where defining instances for classes like Read can be tedious at best, and frequently impossible, for the GADT itself.

Documentation

data Some f :: * where

Constructors

Some :: f a -> Some f

some :: Some f -> (forall a. f a -> r) -> r

An eliminator for a Some type.

Consider this function akin to a Monadic bind, except instead of binding into a Monad with a sequent function, we're binding into the existential quantification with a universal eliminator function.

It serves as an explicit delimiter in a program of where the type index may be used and depended on, and where it may not.

NB: the result type of the eliminating function may not refer to the universally quantified type index a.

withSome :: (forall a. f a -> r) -> Some f -> r

onSome :: (forall a. f a -> g b) -> Some f -> Some g

type Some2 f = Some (Some :.: f)

pattern Some2 :: f a b -> Some2 k k f

data All f :: * where

Constructors

All :: (forall a. f a) -> All f

Fields

instAll :: forall a. f a

data f :-> g where infixr 4

A data type for natural transformations.

Constructors

NT :: (forall a. f a -> g a) -> f :-> g

data p :--> q where infixr 4

Constructors

NT2 :: (forall a b. p a b -> q a b) -> p :--> q