Copyright | Copyright (C) 2015 Kyle Carter |
---|---|

License | BSD3 |

Maintainer | Kyle Carter <kylcarte@indiana.edu> |

Stability | experimental |

Portability | RankNTypes |

Safe Haskell | None |

Language | Haskell2010 |

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.

- data Prod f :: [k] -> * where
- pattern (:>) :: forall k f a b. f a -> f b -> Prod k f ((:) k a ((:) k b ([] k)))
- only :: f a -> Prod f '[a]
- (>:) :: Prod f as -> f a -> Prod f (as >: a)
- 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)
- last' :: Prod f (a :< as) -> f (Last' a as)
- 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
- only_ :: a -> Tuple '[a]
- pattern (::<) :: forall a as. a -> Tuple as -> Tuple ((:<) * a as)
- (>::) :: Tuple as -> a -> Tuple (as >: a)
- 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 ...
- toList :: (forall a. f a -> r) -> Prod f as -> [r]

# Documentation

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

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 :< Ø`

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

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

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

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

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

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

Cons onto a Tuple.

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

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