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'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 (:>) :: 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)
- lookup' :: TestEquality f => f a -> Prod (f :&: g) as -> Maybe (g a)
- 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 (::<) :: 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
Documentation
data Prod f :: [k] -> * where Source
Witness ØC ØC (Prod k f (Ø k)) Source | |
Traversable1 k [k] (Prod k) Source | |
Foldable1 k [k] (Prod k) Source | |
Functor1 k [k] (Prod k) Source | |
IxTraversable1 [k] k (Index k) (Prod k) Source | |
IxFoldable1 [k] k (Index k) (Prod k) Source | |
IxFunctor1 [k] k (Index k) (Prod k) Source | |
TestEquality k f => TestEquality [k] (Prod k f) Source | |
Read1 k f => Read1 [k] (Prod k f) Source | |
Show1 k f => Show1 [k] (Prod k f) Source | |
Ord1 k f => Ord1 [k] (Prod k f) Source | |
Eq1 k f => Eq1 [k] (Prod k f) Source | |
Known [k] (Prod k f) (Ø k) Source | |
(Known k f a, Known [k] (Prod k f) as) => Known [k] (Prod k f) ((:<) k a as) Source | |
(Witness p q (f a), Witness s t (Prod k f as)) => Witness (p, s) (q, t) (Prod k f ((:<) k a as)) Source | |
ListC ((<$>) Constraint * Eq ((<$>) * k f as)) => Eq (Prod k f as) Source | |
(ListC ((<$>) Constraint * Eq ((<$>) * k f as)), ListC ((<$>) Constraint * Ord ((<$>) * k f as))) => Ord (Prod k f as) Source | |
ListC ((<$>) Constraint * Show ((<$>) * k f as)) => Show (Prod k f as) Source | |
type WitnessC ØC ØC (Prod k f (Ø k)) = ØC | |
type KnownC [k] (Prod k f) (Ø k) = ØC | |
type KnownC [k] (Prod k f) ((:<) k a as) = (Known k f a, Known [k] (Prod k f) as) Source | |
type WitnessC (p, s) (q, t) (Prod k f ((:<) k a as)) = (Witness p q (f a), Witness s t (Prod k f as)) Source |
pattern (:>) :: 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.