Data.Type.Product

Type combinators for type-level lists, lifting (f :: k -> *) to (Prod f :: [k] -> *), as well as its constructions, manipulations, and eliminations.

Prod is similar in nature to a few others in the Haskell ecosystem, such as:

Oleg Kiselyov's HList, from http://hackage.haskell.org/package/HList, and

Kenneth Foner's ConicList, from http://hackage.haskell.org/package/IndexedList-0.1.0.1/docs/Data-List-Indexed-Conic.html.

Documentation

data Prod f :: [k] -> * where

Constructors

Ø :: Prod f Ø

(:<) :: !(f a) -> !(Prod f as) -> Prod f (a :< as) infixr 5

Instances

Witness ØC ØC (Prod k f (Ø k))

Associated Types

type WitnessC (ØC :: Constraint) (ØC :: Constraint) (Prod k f (Ø k)) :: Constraint

Methods

(\\) :: ØC => (ØC -> r) -> Prod k f (Ø k) -> r

IxTraversable1 k [k] (Index k) (Prod k)

Methods

itraverse1 :: Applicative h => (forall a. i b a -> f a -> h (g a)) -> t f b -> h (t g b)

IxFoldable1 k [k] (Index k) (Prod k)

Methods

ifoldMap1 :: Monoid m => (forall a. i b a -> f a -> m) -> t f b -> m

IxFunctor1 k [k] (Index k) (Prod k)

Methods

imap1 :: (forall a. i b a -> f a -> g a) -> t f b -> t g b

Traversable1 [k] k (Prod k)

Methods

traverse1 :: Applicative h => (forall a. f a -> h (g a)) -> t f b -> h (t g b)

Foldable1 [k] k (Prod k)

Methods

foldMap1 :: Monoid m => (forall a. f a -> m) -> t f b -> m

Functor1 [k] k (Prod k)

Methods

map1 :: (forall a. f a -> g a) -> t f b -> t g b

TestEquality k f => TestEquality [k] (Prod k f)

Methods

testEquality :: f a -> f b -> Maybe ((Prod k f :~: a) b)

Read1 k f => Read1 [k] (Prod k f)

Methods

readsPrec1 :: Int -> ReadS (Some (Prod k f) f)

Show1 k f => Show1 [k] (Prod k f)

Methods

showsPrec1 :: Int -> f a -> ShowS

show1 :: f a -> String

Ord1 k f => Ord1 [k] (Prod k f)

Methods

compare1 :: f a -> f a -> Ordering

(<#) :: f a -> f a -> Bool

(>#) :: f a -> f a -> Bool

(<=#) :: f a -> f a -> Bool

(>=#) :: f a -> f a -> Bool

Eq1 k f => Eq1 [k] (Prod k f)

Methods

eq1 :: f a -> f a -> Bool

neq1 :: f a -> f a -> Bool

BoolEquality k f => BoolEquality [k] (Prod k f)

Methods

boolEquality :: f a -> f b -> Boolean ((Prod k f == a) b)

(Known [k] (Length k) as, Every k (Known k f) as) => Known [k] (Prod k f) as

Associated Types

type KnownC (Prod k f) (as :: Prod k f -> *) (a :: Prod k f) :: Constraint

Methods

known :: as a

(Witness p q (f a1), Witness s t (Prod a f as)) => Witness (p, s) (q, t) (Prod a f ((:<) a a1 as))

Associated Types

type WitnessC ((p, s) :: Constraint) ((q, t) :: Constraint) (Prod a f ((:<) a a1 as)) :: Constraint

Methods

(\\) :: (p, s) => ((q, t) -> r) -> Prod a f ((a :< a1) as) -> r

ListC ((<$>) Constraint * Eq ((<$>) * k f as)) => Eq (Prod k f as)

Methods

(==) :: Prod k f as -> Prod k f as -> Bool

(/=) :: Prod k f as -> Prod k f as -> Bool

(ListC ((<$>) Constraint * Eq ((<$>) * k f as)), ListC ((<$>) Constraint * Ord ((<$>) * k f as))) => Ord (Prod k f as)

Methods

compare :: Prod k f as -> Prod k f as -> Ordering

(<) :: Prod k f as -> Prod k f as -> Bool

(<=) :: Prod k f as -> Prod k f as -> Bool

(>) :: Prod k f as -> Prod k f as -> Bool

(>=) :: Prod k f as -> Prod k f as -> Bool

max :: Prod k f as -> Prod k f as -> Prod k f as

min :: Prod k f as -> Prod k f as -> Prod k f as

ListC ((<$>) Constraint * Show ((<$>) * k f as)) => Show (Prod k f as)

Methods

showsPrec :: Int -> Prod k f as -> ShowS

show :: Prod k f as -> String

showList :: [Prod k f as] -> ShowS

type WitnessC ØC ØC (Prod k f (Ø k))

type WitnessC ØC ØC (Prod k f (Ø k)) = ØC

type KnownC [k] (Prod k f) as

type KnownC [k] (Prod k f) as = (Known [k] (Length k) as, Every k (Known k f) as)

type WitnessC (p, s) (q, t) (Prod a f ((:<) a a1 as))

type WitnessC (p, s) (q, t) (Prod a f ((:<) a a1 as)) = (Witness p q (f a1), Witness s t (Prod a f as))

pattern (:>) :: forall k f a b. f a -> f b -> Prod k f ((:) k a ((:) k b ([] k))) infix 6

Construct a two element Prod. Since the precedence of (:>) is higher than (:<), we can conveniently write lists like:

>>> a :< b :> c

Which is identical to:

>>> a :< b :< c :< Ø

only :: f a -> Prod f '[a]

Build a singleton Prod.

(>:) :: Prod f as -> f a -> Prod f (as >: a) infixl 6

snoc function. insert an element at the end of the list.

head' :: Prod f (a :< as) -> f a

tail' :: Prod f (a :< as) -> Prod f as

init' :: Prod f (a :< as) -> Prod f (Init' a as)

Get all but the last element of a non-empty Prod.

last' :: Prod f (a :< as) -> f (Last' a as)

Get the last element of a non-empty Prod.

reverse' :: Prod f as -> Prod f (Reverse as)

append' :: Prod f as -> Prod f bs -> Prod f (as ++ bs)

lookupPar :: TestEquality f => f a -> Prod (f :*: g) as -> Maybe (Some g)

permute :: Known Length bs => (forall x. Index bs x -> Index as x) -> Prod f as -> Prod f bs

permute' :: (forall x. Index bs x -> Index as x) -> Prod f as -> Length bs -> Prod f bs

type Tuple = Prod I

A Prod of simple Haskell types.

only_ :: a -> Tuple '[a]

Singleton Tuple.

pattern (::<) :: forall a as. a -> Tuple as -> Tuple ((:<) * a as) infixr 5

Cons onto a Tuple.

(>::) :: Tuple as -> a -> Tuple (as >: a) infixl 6

Snoc onto a Tuple.

elimProd :: p Ø -> (forall x xs. Index as x -> f x -> p xs -> p (x :< xs)) -> Prod f as -> p as

onHead' :: (f a -> f b) -> Prod f (a :< as) -> Prod f (b :< as)

onTail' :: (Prod f as -> Prod f bs) -> Prod f (a :< as) -> Prod f (a :< bs)

uncurry' :: (f a -> Prod f as -> r) -> Prod f (a :< as) -> r

curry' :: l ~ (a :< as) => (Prod f l -> r) -> f a -> Prod f as -> r

index :: Index as a -> Prod f as -> f a

select :: Prod (Index as) bs -> Prod f as -> Prod f bs

indices :: forall as. Known Length as => Prod (Index as) as

indices' :: Length as -> Prod (Index as) as

type family Witnesses (ps :: [Constraint]) (qs :: [Constraint]) (f :: k -> *) (as :: [k]) :: Constraint where ...

Equations

Witnesses Ø Ø f Ø = ØC

Witnesses (p :< ps) (q :< qs) f (a :< as) = (Witness p q (f a), Witnesses ps qs f as)

toList :: (forall a. f a -> r) -> Prod f as -> [r]