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

Description

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.

Synopsis

Documentation

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

Constructors

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

Instances

Witness ØC ØC (Prod k f (Ø k)) Source #
Associated Types type WitnessC (ØC :: Constraint) (ØC :: Constraint) (Prod k f (Ø k)) :: Constraint Source # Methods (\\) :: ØC => (ØC -> r) -> Prod k f (Ø k) -> r Source #
IxTraversable1 k [k] (Index k) (Prod k) Source #
Methods itraverse1 :: Applicative h => (forall a. i b a -> f a -> h (g a)) -> t f b -> h (t g b) Source #
IxFoldable1 k [k] (Index k) (Prod k) Source #
Methods ifoldMap1 :: Monoid m => (forall a. i b a -> f a -> m) -> t f b -> m Source #
IxFunctor1 k [k] (Index k) (Prod k) Source #
Methods imap1 :: (forall a. i b a -> f a -> g a) -> t f b -> t g b Source #
Traversable1 [k] k (Prod k) Source #
Methods traverse1 :: Applicative h => (forall a. f a -> h (g a)) -> t f b -> h (t g b) Source #
Foldable1 [k] k (Prod k) Source #
Methods foldMap1 :: Monoid m => (forall a. f a -> m) -> t f b -> m Source #
Functor1 [k] k (Prod k) Source #
Methods map1 :: (forall a. f a -> g a) -> t f b -> t g b Source #
TestEquality k f => TestEquality [k] (Prod k f) Source #
Methods testEquality :: f a -> f b -> Maybe ((Prod k f :~: a) b) #
Read1 k f => Read1 [k] (Prod k f) Source #
Methods readsPrec1 :: Int -> ReadS (Some (Prod k f) f) Source #
Show1 k f => Show1 [k] (Prod k f) Source #
Methods showsPrec1 :: Int -> f a -> ShowS Source # show1 :: f a -> String Source #
Ord1 k f => Ord1 [k] (Prod k f) Source #
Methods compare1 :: f a -> f a -> Ordering Source # (<#) :: f a -> f a -> Bool Source # (>#) :: f a -> f a -> Bool Source # (<=#) :: f a -> f a -> Bool Source # (>=#) :: f a -> f a -> Bool Source #
Eq1 k f => Eq1 [k] (Prod k f) Source #
Methods eq1 :: f a -> f a -> Bool Source # neq1 :: f a -> f a -> Bool Source #
BoolEquality k f => BoolEquality [k] (Prod k f) Source #
Methods boolEquality :: f a -> f b -> Boolean ((Prod k f == a) b) Source #
(Known [k] (Length k) as, Every k (Known k f) as) => Known [k] (Prod k f) as Source #
Associated Types type KnownC (Prod k f) (as :: Prod k f -> *) (a :: Prod k f) :: Constraint Source # Methods known :: as a Source #
(Witness p q (f a1), Witness s t (Prod a f as)) => Witness (p, s) (q, t) (Prod a f ((:<) a a1 as)) Source #
Associated Types type WitnessC ((p, s) :: Constraint) ((q, t) :: Constraint) (Prod a f ((:<) a a1 as)) :: Constraint Source # Methods (\\) :: (p, s) => ((q, t) -> r) -> Prod a f ((a :< a1) as) -> r Source #
ListC ((<$>) Constraint * Eq ((<$>) * k f as)) => Eq (Prod k f as) Source #
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) Source #
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) Source #
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)) Source #
type WitnessC ØC ØC (Prod k f (Ø k)) = ØC
type KnownC [k] (Prod k f) as Source #
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)) Source #
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 Source #

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] Source #

Build a singleton Prod.

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

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

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

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

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

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

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

Get the last element of a non-empty Prod.

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

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

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

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

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

type Tuple = Prod I Source #

A Prod of simple Haskell types.

only_ :: a -> Tuple '[a] Source #

Singleton Tuple.

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

Cons onto a Tuple.

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

Snoc onto a Tuple.

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

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

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

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

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

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

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

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

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

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

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] Source #