Copyright	Copyright (C) 2015 Kyle Carter
License	BSD3
Maintainer	Kyle Carter <kylcarte@indiana.edu>
Stability	experimental
Portability	RankNTypes
Safe Haskell	None
Language	Haskell2010

Data.Type.Quantifier

Description

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.

Synopsis

Documentation

data Some f :: * where Source

Constructors

Some :: f a -> Some f

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

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.

(>>-) :: Some f -> (forall a. f a -> r) -> r infixl 1 Source

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

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

data Some2 f :: * where Source

Constructors

Some2 :: f a b -> Some2 f

some2 :: Some2 f -> (forall a b. f a b -> r) -> r Source

(>>--) :: Some2 f -> (forall a b. f a b -> r) -> r infixl 1 Source

withSome2 :: (forall a b. f a b -> r) -> Some2 f -> r Source

onSome2 :: (forall a b. f a b -> g x y) -> Some2 f -> Some2 g Source

data Some3 f :: * where Source

Constructors

Some3 :: f a b c -> Some3 f

some3 :: Some3 f -> (forall a b c. f a b c -> r) -> r Source

(>>---) :: Some3 f -> (forall a b c. f a b c -> r) -> r infixl 1 Source

withSome3 :: (forall a b c. f a b c -> r) -> Some3 f -> r Source

onSome3 :: (forall a b c. f a b c -> g x y z) -> Some3 f -> Some3 g Source

data SomeC c f where Source

Constructors

SomeC :: c a => f a -> SomeC c f

someC :: SomeC c f -> (forall a. c a => f a -> r) -> r Source

(>>~) :: SomeC c f -> (forall a. c a => f a -> r) -> r infixl 1 Source

data Every f :: * where Source

Constructors

Every :: (forall a. f a) -> Every f
Fields instEvery :: forall a. f a

data Every2 f :: * where Source

Constructors

Every2 :: (forall a b. f a b) -> Every2 f
Fields instEvery2 :: forall a b. f a b

data Every3 f :: * where Source

Constructors

Every3 :: (forall a b c. f a b c) -> Every3 f
Fields instEvery3 :: forall a b c. f a b c