Safe Haskell | Safe |
---|---|

Language | Haskell2010 |

Lists.

## Synopsis

- data Foldr :: (a -> b -> Exp b) -> b -> [a] -> Exp b
- data Unfoldr :: (b -> Exp (Maybe (a, b))) -> b -> Exp [a]
- data UnList :: b -> (a -> b -> Exp b) -> [a] -> Exp b
- data Cons :: a -> [a] -> Exp [a]
- data (++) :: [a] -> [a] -> Exp [a]
- data Concat :: [[a]] -> Exp [a]
- data ConcatMap :: (a -> Exp [b]) -> [a] -> Exp [b]
- data Filter :: (a -> Exp Bool) -> [a] -> Exp [a]
- data Head :: [a] -> Exp (Maybe a)
- data Last :: [a] -> Exp (Maybe a)
- data Tail :: [a] -> Exp (Maybe [a])
- data Init :: [a] -> Exp (Maybe [a])
- data Null :: [a] -> Exp Bool
- data Length :: [a] -> Exp Nat
- data Replicate :: Nat -> a -> Exp [a]
- data Find :: (a -> Exp Bool) -> [a] -> Exp (Maybe a)
- data FindIndex :: (a -> Exp Bool) -> [a] -> Exp (Maybe Nat)
- data Elem :: a -> [a] -> Exp Bool
- data Lookup :: k -> [(k, b)] -> Exp (Maybe b)
- data SetIndex :: Nat -> a -> [a] -> Exp [a]
- data ZipWith :: (a -> b -> Exp c) -> [a] -> [b] -> Exp [c]
- data Zip :: [a] -> [b] -> Exp [(a, b)]
- data Unzip :: Exp [(a, b)] -> Exp ([a], [b])
- data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])
- data Take :: Nat -> [a] -> Exp [a]
- data Drop :: Nat -> [a] -> Exp [a]
- data TakeWhile :: (a -> Exp Bool) -> [a] -> Exp [a]
- data DropWhile :: (a -> Exp Bool) -> [a] -> Exp [a]
- data Reverse :: [a] -> Exp [a]

# Documentation

data Foldr :: (a -> b -> Exp b) -> b -> [a] -> Exp b Source #

Foldr for type-level lists.

### Example

`>>>`

Eval (Foldr (+) 0 '[1, 2, 3, 4]) :: Nat = 10`:kind! Eval (Foldr (+) 0 '[1, 2, 3, 4])`

data Unfoldr :: (b -> Exp (Maybe (a, b))) -> b -> Exp [a] Source #

Type-level Unfoldr.

### Example

`>>>`

`data ToThree :: Nat -> Exp (Maybe (Nat, Nat))`

`>>>`

type instance Eval (ToThree b) = If (Eval (b Fcf.>= 4)) 'Nothing ('Just '(b, b TL.+ 1)) :}`:{`

`>>>`

Eval (Unfoldr ToThree 0) :: [Nat] = '[0, 1, 2, 3]`:kind! Eval (Unfoldr ToThree 0)`

See also the definition of `Replicate`

.

data UnList :: b -> (a -> b -> Exp b) -> [a] -> Exp b Source #

N.B.: This is equivalent to a `Foldr`

flipped.

data Cons :: a -> [a] -> Exp [a] Source #

Append an element for type-level lists.

### Example

`>>>`

Eval (Cons 1 '[2, 3]) :: [Nat] = '[1, 2, 3]`:kind! Eval (Cons 1 '[2, 3])`

`>>>`

Eval (Cons Int '[Char, Maybe Double]) :: [*] = '[Int, Char, Maybe Double]`:kind! Eval (Cons Int '[Char, Maybe Double])`

data (++) :: [a] -> [a] -> Exp [a] Source #

Type-level list catenation.

### Example

`>>>`

Eval ('[1, 2] ++ '[3, 4]) :: [Nat] = '[1, 2, 3, 4]`:kind! Eval ('[1, 2] ++ '[3, 4])`

data Concat :: [[a]] -> Exp [a] Source #

Concat for lists.

### Example

`>>>`

Eval (Concat ( '[ '[1,2], '[3,4], '[5,6]])) :: [Nat] = '[1, 2, 3, 4, 5, 6]`:kind! Eval (Concat ( '[ '[1,2], '[3,4], '[5,6]]))`

`>>>`

Eval (Concat ( '[ '[Int, Maybe Int], '[Maybe String, Either Double Int]])) :: [*] = '[Int, Maybe Int, Maybe String, Either Double Int]`:kind! Eval (Concat ( '[ '[Int, Maybe Int], '[Maybe String, Either Double Int]]))`

data Replicate :: Nat -> a -> Exp [a] Source #

Type-level `Replicate`

for lists.

### Example

`>>>`

Eval (Replicate 4 '("ok", 2)) :: [(TL.Symbol, Nat)] = '[ '("ok", 2), '("ok", 2), '("ok", 2), '("ok", 2)]`:kind! Eval (Replicate 4 '("ok", 2))`

data Find :: (a -> Exp Bool) -> [a] -> Exp (Maybe a) Source #

data FindIndex :: (a -> Exp Bool) -> [a] -> Exp (Maybe Nat) Source #

Find the index of an element satisfying the predicate.

data Elem :: a -> [a] -> Exp Bool Source #

Type-level `Elem`

for lists.

### Example

`>>>`

Eval (Elem 1 '[1,2,3]) :: Bool = 'True`:kind! Eval (Elem 1 '[1,2,3])`

`>>>`

Eval (Elem 1 '[2,3]) :: Bool = 'False`:kind! Eval (Elem 1 '[2,3])`

data SetIndex :: Nat -> a -> [a] -> Exp [a] Source #

Modify an element at a given index.

The list is unchanged if the index is out of bounds.

data ZipWith :: (a -> b -> Exp c) -> [a] -> [b] -> Exp [c] Source #

data Take :: Nat -> [a] -> Exp [a] Source #

Type-level list take.

### Example

`>>>`

Eval (Take 2 '[1,2,3,4,5]) :: [Nat] = '[1, 2]`:kind! Eval (Take 2 '[1,2,3,4,5])`

data Drop :: Nat -> [a] -> Exp [a] Source #

Type-level list drop.

### Example

`>>>`

Eval (Drop 2 '[1,2,3,4,5]) :: [Nat] = '[3, 4, 5]`:kind! Eval (Drop 2 '[1,2,3,4,5])`

data TakeWhile :: (a -> Exp Bool) -> [a] -> Exp [a] Source #

Type-level list takeWhile.

### Example

`>>>`

Eval (TakeWhile ((>=) 3) '[1, 2, 3, 4, 5]) :: [Nat] = '[1, 2, 3]`:kind! Eval (TakeWhile ((>=) 3) '[1, 2, 3, 4, 5])`

data DropWhile :: (a -> Exp Bool) -> [a] -> Exp [a] Source #

Type-level list dropWhile.

### Example

:kind! Eval (DropWhile ((>=) 3) '[1, 2, 3, 4, 5]) Eval (DropWhile ((>=) 3) '[1, 2, 3, 4, 5]) :: [Nat] = '[4, 5]