Fcf.Data.List

Lists.

See also Fcf.Class.Foldable for additional functions.

Basic functions

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

List catenation.

Example

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

Instances

type Eval (xs ++ ys :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (xs ++ ys :: [a] -> Type) = xs <> ys

data Head :: [a] -> Exp (Maybe a)

Instances

type Eval (Head (a2 ': _as) :: Maybe a1 -> Type)

Defined in Fcf.Data.List

type Eval (Head (a2 ': _as) :: Maybe a1 -> Type) = Just a2

type Eval (Head ([] :: [a]) :: Maybe a -> Type)

Defined in Fcf.Data.List

type Eval (Head ([] :: [a]) :: Maybe a -> Type) = (Nothing :: Maybe a)

data Last :: [a] -> Exp (Maybe a)

Instances

type Eval (Last (a2 ': (b ': as)) :: Maybe a1 -> Type)

Defined in Fcf.Data.List

type Eval (Last (a2 ': (b ': as)) :: Maybe a1 -> Type) = Eval (Last (b ': as))

type Eval (Last (a2 ': ([] :: [a1])) :: Maybe a1 -> Type)

Defined in Fcf.Data.List

type Eval (Last (a2 ': ([] :: [a1])) :: Maybe a1 -> Type) = Just a2

type Eval (Last ([] :: [a]) :: Maybe a -> Type)

Defined in Fcf.Data.List

type Eval (Last ([] :: [a]) :: Maybe a -> Type) = (Nothing :: Maybe a)

data Tail :: [a] -> Exp (Maybe [a])

Instances

type Eval (Tail (_a ': as) :: Maybe [a] -> Type)

Defined in Fcf.Data.List

type Eval (Tail (_a ': as) :: Maybe [a] -> Type) = Just as

type Eval (Tail ([] :: [a]) :: Maybe [a] -> Type)

Defined in Fcf.Data.List

type Eval (Tail ([] :: [a]) :: Maybe [a] -> Type) = (Nothing :: Maybe [a])

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

Append an element to a list.

Example

>>> :kind! Eval (Cons 1 '[2, 3])
Eval (Cons 1 '[2, 3]) :: [Nat]
= '[1, 2, 3]
>>> :kind! Eval (Cons Int '[Char, Maybe Double])
Eval (Cons Int '[Char, Maybe Double]) :: [*]
= '[Int, Char, Maybe Double]

Instances

type Eval (Cons a2 as :: [a1] -> Type)

Defined in Fcf.Data.List

type Eval (Cons a2 as :: [a1] -> Type) = a2 ': as

data Snoc :: [a] -> a -> Exp [a]

Append an element to the end of a list.

Example

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

Instances

type Eval (Snoc lst a :: [k] -> Type)

Defined in Fcf.Data.List

type Eval (Snoc lst a :: [k] -> Type) = Eval (lst ++ (a ': ([] :: [k])))

data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])

Append elements to two lists. Used in the definition of Unzip.

Instances

type Eval (Cons2 ((,) a3 b) ((,) as bs) :: ([a2], [a1]) -> Type)

Defined in Fcf.Data.List

type Eval (Cons2 ((,) a3 b) ((,) as bs) :: ([a2], [a1]) -> Type) = (,) (a3 ': as) (b ': bs)

data Init :: [a] -> Exp (Maybe [a])

Instances

type Eval (Init (a2 ': ([] :: [a1])) :: Maybe [a1] -> Type)

Defined in Fcf.Data.List

type Eval (Init (a2 ': ([] :: [a1])) :: Maybe [a1] -> Type) = Just ([] :: [a1])

type Eval (Init ([] :: [a]) :: Maybe [a] -> Type)

Defined in Fcf.Data.List

type Eval (Init ([] :: [a]) :: Maybe [a] -> Type) = (Nothing :: Maybe [a])

type Eval (Init (a2 ': (b ': as)) :: Maybe [a1] -> Type)

Defined in Fcf.Data.List

type Eval (Init (a2 ': (b ': as)) :: Maybe [a1] -> Type) = Eval ((Map (Cons a2) :: Maybe [a1] -> Maybe [a1] -> Type) =<< Init (b ': as))

data Null :: [a] -> Exp Bool

Instances

type Eval (Null (a2 ': as) :: Bool -> Type)

Defined in Fcf.Data.List

type Eval (Null (a2 ': as) :: Bool -> Type) = False

type Eval (Null ([] :: [a]) :: Bool -> Type)

Defined in Fcf.Data.List

type Eval (Null ([] :: [a]) :: Bool -> Type) = True

data Length :: [a] -> Exp Nat

Instances

type Eval (Length (a2 ': as) :: Nat -> Type)

Defined in Fcf.Data.List

type Eval (Length (a2 ': as) :: Nat -> Type) = 1 + Eval (Length as)

type Eval (Length ([] :: [a]) :: Nat -> Type)

Defined in Fcf.Data.List

type Eval (Length ([] :: [a]) :: Nat -> Type) = 0

List transformations

data Reverse :: [a] -> Exp [a]

Reverse a list.

Example

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

Instances

type Eval (Reverse l :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Reverse l :: [a] -> Type)

data Intersperse :: a -> [a] -> Exp [a]

Intersperse a separator between elements of a list.

Example

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

Instances

type Eval (Intersperse _ ([] :: [a]) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Intersperse _ ([] :: [a]) :: [a] -> Type) = ([] :: [a])

type Eval (Intersperse sep (x ': xs) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Intersperse sep (x ': xs) :: [a] -> Type)

data Intercalate :: [a] -> [[a]] -> Exp [a]

Join a list of words separated by some word.

Example

>>> :kind! Eval (Intercalate '[", "] '[ '["Lorem"], '["ipsum"], '["dolor"] ])
Eval (Intercalate '[", "] '[ '["Lorem"], '["ipsum"], '["dolor"] ]) :: [TL.Symbol]
= '["Lorem", ", ", "ipsum", ", ", "dolor"]

Instances

type Eval (Intercalate xs xss :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Intercalate xs xss :: [a] -> Type) = Eval ((Concat :: [[a]] -> [a] -> Type) =<< Intersperse xs xss)

Reducing lists

See also Fcf.Class.Foldable.

data Foldr :: (a -> b -> Exp b) -> b -> t a -> Exp b

Right fold.

Example

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

Instances

type Eval (Foldr f y (Right x :: Either a3 a1) :: a2 -> Type)

Defined in Fcf.Class.Foldable

type Eval (Foldr f y (Right x :: Either a3 a1) :: a2 -> Type) = Eval (f x y)

type Eval (Foldr f y (Left _a :: Either a3 a1) :: a2 -> Type)

Defined in Fcf.Class.Foldable

type Eval (Foldr f y (Left _a :: Either a3 a1) :: a2 -> Type) = y

type Eval (Foldr f y (Just x) :: a2 -> Type)

Defined in Fcf.Class.Foldable

type Eval (Foldr f y (Just x) :: a2 -> Type) = Eval (f x y)

type Eval (Foldr f y (Nothing :: Maybe a1) :: a2 -> Type)

Defined in Fcf.Class.Foldable

type Eval (Foldr f y (Nothing :: Maybe a1) :: a2 -> Type) = y

type Eval (Foldr f y (x ': xs) :: a2 -> Type)

Defined in Fcf.Class.Foldable

type Eval (Foldr f y (x ': xs) :: a2 -> Type) = Eval (f x (Eval (Foldr f y xs)))

type Eval (Foldr f y ([] :: [a1]) :: a2 -> Type)

Defined in Fcf.Class.Foldable

type Eval (Foldr f y ([] :: [a1]) :: a2 -> Type) = y

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

This is Foldr with its argument flipped.

Instances

type Eval (UnList y f xs :: a2 -> Type)

Defined in Fcf.Data.List

type Eval (UnList y f xs :: a2 -> Type) = Eval (Foldr f y xs)

data Concat :: t m -> Exp m

Concatenate a collection of elements from a monoid.

Example

For example, fold a list of lists.

Concat :: [[a]] -> Exp [a]

>>> :kind! Eval (Concat ( '[ '[1,2], '[3,4], '[5,6]]))
Eval (Concat ( '[ '[1,2], '[3,4], '[5,6]])) :: [Nat]
= '[1, 2, 3, 4, 5, 6]
>>> :kind! Eval (Concat ( '[ '[Int, Maybe Int], '[Maybe String, Either Double Int]]))
Eval (Concat ( '[ '[Int, Maybe Int], '[Maybe String, Either Double Int]])) :: [*]
= '[Int, Maybe Int, Maybe String, Either Double Int]

Instances

type Eval (Concat xs :: a -> Type)

Defined in Fcf.Class.Foldable

type Eval (Concat xs :: a -> Type) = Eval (FoldMap (Pure :: a -> a -> Type) xs)

data ConcatMap :: (a -> Exp [b]) -> t a -> Exp [b]

Map a function and concatenate the results.

This is FoldMap specialized to the list monoid.

Instances

type Eval (ConcatMap f xs :: [b] -> Type)

Defined in Fcf.Class.Foldable

type Eval (ConcatMap f xs :: [b] -> Type) = Eval (FoldMap f xs)

Unfolding and building

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

Unfold a generator into a list.

Example

>>> data ToThree :: Nat -> Exp (Maybe (Nat, Nat))
>>> :{
type instance Eval (ToThree b) =
  If (Eval (b Fcf.>= 4))
    'Nothing
    ('Just '(b, b TL.+ 1))
:}

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

See also the definition of Replicate.

Instances

type Eval (Unfoldr f c :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Unfoldr f c :: [a] -> Type)

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

Repeat the same element in a list.

Example

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

Instances

type Eval (Replicate n a2 :: [a1] -> Type)

Defined in Fcf.Data.List

type Eval (Replicate n a2 :: [a1] -> Type)

Sublists

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

Take a prefix of fixed length.

Example

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

Instances

type Eval (Take n as :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Take n as :: [a] -> Type)

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

Drop a prefix of fixed length, evaluate to the remaining suffix.

Example

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

Instances

type Eval (Drop n as :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Drop n as :: [a] -> Type)

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

Take the longest prefix of elements satisfying a predicate.

Example

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

Instances

type Eval (TakeWhile p (x ': xs) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (TakeWhile p (x ': xs) :: [a] -> Type) = Eval (If (Eval (p x)) ((:) x <$> TakeWhile p xs) (Pure ([] :: [a])))

type Eval (TakeWhile p ([] :: [a]) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (TakeWhile p ([] :: [a]) :: [a] -> Type) = ([] :: [a])

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

Drop the longest prefix of elements satisfying a predicate, evaluate to the remaining suffix.

Example

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

Instances

type Eval (DropWhile p (x ': xs) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (DropWhile p (x ': xs) :: [a] -> Type) = Eval (If (Eval (p x)) (DropWhile p xs) (Pure (x ': xs)))

type Eval (DropWhile p ([] :: [a]) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (DropWhile p ([] :: [a]) :: [a] -> Type) = ([] :: [a])

data Span :: (a -> Exp Bool) -> [a] -> Exp ([a], [a])

Span, applied to a predicate p and a list xs, returns a tuple: the first component is the longest prefix (possibly empty) of xs whose elements satisfy p; the second component is the remainder of the list.

See also TakeWhile, DropWhile, and Break.

Example

>>> :kind! Eval (Span (Flip (<) 3) '[1,2,3,4,1,2,3,4])
Eval (Span (Flip (<) 3) '[1,2,3,4,1,2,3,4]) :: ([Nat], [Nat])
= '( '[1, 2], '[3, 4, 1, 2, 3, 4])

>>> :kind! Eval (Span (Flip (<) 9) '[1,2,3])
Eval (Span (Flip (<) 9) '[1,2,3]) :: ([Nat], [Nat])
= '( '[1, 2, 3], '[])

>>> :kind! Eval (Span (Flip (<) 0) '[1,2,3])
Eval (Span (Flip (<) 0) '[1,2,3]) :: ([Nat], [Nat])
= '( '[], '[1, 2, 3])

Instances

type Eval (Span p lst :: ([a], [a]) -> Type)

Defined in Fcf.Data.List

type Eval (Span p lst :: ([a], [a]) -> Type) = (,) (Eval (TakeWhile p lst)) (Eval (DropWhile p lst))

data Break :: (a -> Exp Bool) -> [a] -> Exp ([a], [a])

Break, applied to a predicate p and a list xs, returns a tuple: the first component is the longest prefix (possibly empty) of xs whose elements do not satisfy p; the second component is the remainder of the list.

Example

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

>>> :kind! Eval (Break (Flip (<) 9) '[1,2,3])
Eval (Break (Flip (<) 9) '[1,2,3]) :: ([Nat], [Nat])
= '( '[], '[1, 2, 3])

>>> :kind! Eval (Break (Flip (>) 9) '[1,2,3])
Eval (Break (Flip (>) 9) '[1,2,3]) :: ([Nat], [Nat])
= '( '[1, 2, 3], '[])

Instances

type Eval (Break p lst :: ([a], [a]) -> Type)

Defined in Fcf.Data.List

type Eval (Break p lst :: ([a], [a]) -> Type) = Eval (Span (Not <=< p) lst)

data Tails :: [a] -> Exp [[a]]

List of suffixes of a list.

Example

>>> :kind! Eval (Tails '[0,1,2,3])
Eval (Tails '[0,1,2,3]) :: [[Nat]]
= '[ '[0, 1, 2, 3], '[1, 2, 3], '[2, 3], '[3]]

Instances

type Eval (Tails (a2 ': as) :: [[a1]] -> Type)

Defined in Fcf.Data.List

type Eval (Tails (a2 ': as) :: [[a1]] -> Type) = (a2 ': as) ': Eval (Tails as)

type Eval (Tails ([] :: [a]) :: [[a]] -> Type)

Defined in Fcf.Data.List

type Eval (Tails ([] :: [a]) :: [[a]] -> Type) = ([] :: [[a]])

Predicates

data IsPrefixOf :: [a] -> [a] -> Exp Bool

Return True when the first list is a prefix of the second.

Example

>>> :kind! Eval (IsPrefixOf '[0,1,2] '[0,1,2,3,4,5])
Eval (IsPrefixOf '[0,1,2] '[0,1,2,3,4,5]) :: Bool
= 'True

>>> :kind! Eval (IsPrefixOf '[0,1,2] '[0,1,3,2,4,5])
Eval (IsPrefixOf '[0,1,2] '[0,1,3,2,4,5]) :: Bool
= 'False

>>> :kind! Eval (IsPrefixOf '[] '[0,1,3,2,4,5])
Eval (IsPrefixOf '[] '[0,1,3,2,4,5]) :: Bool
= 'True

>>> :kind! Eval (IsPrefixOf '[0,1,3,2,4,5] '[])
Eval (IsPrefixOf '[0,1,3,2,4,5] '[]) :: Bool
= 'False

Instances

type Eval (IsPrefixOf xs ys :: Bool -> Type)

Defined in Fcf.Data.List

type Eval (IsPrefixOf xs ys :: Bool -> Type)

data IsSuffixOf :: [a] -> [a] -> Exp Bool

Return True when the first list is a suffix of the second.

Example

>>> :kind! Eval (IsSuffixOf '[3,4,5] '[0,1,2,3,4,5])
Eval (IsSuffixOf '[3,4,5] '[0,1,2,3,4,5]) :: Bool
= 'True

>>> :kind! Eval (IsSuffixOf '[3,4,5] '[0,1,3,2,4,5])
Eval (IsSuffixOf '[3,4,5] '[0,1,3,2,4,5]) :: Bool
= 'False

>>> :kind! Eval (IsSuffixOf '[] '[0,1,3,2,4,5])
Eval (IsSuffixOf '[] '[0,1,3,2,4,5]) :: Bool
= 'True

>>> :kind! Eval (IsSuffixOf '[0,1,3,2,4,5] '[])
Eval (IsSuffixOf '[0,1,3,2,4,5] '[]) :: Bool
= 'False

Instances

type Eval (IsSuffixOf xs ys :: Bool -> Type)

Defined in Fcf.Data.List

type Eval (IsSuffixOf xs ys :: Bool -> Type) = Eval (IsPrefixOf ((Reverse :: [a] -> [a] -> Type) @@ xs) ((Reverse :: [a] -> [a] -> Type) @@ ys))

data IsInfixOf :: [a] -> [a] -> Exp Bool

Return True when the first list is contained within the second.

Example

>>> :kind! Eval (IsInfixOf '[2,3,4] '[0,1,2,3,4,5,6])
Eval (IsInfixOf '[2,3,4] '[0,1,2,3,4,5,6]) :: Bool
= 'True

>>> :kind! Eval (IsInfixOf '[2,4,4] '[0,1,2,3,4,5,6])
Eval (IsInfixOf '[2,4,4] '[0,1,2,3,4,5,6]) :: Bool
= 'False

Instances

type Eval (IsInfixOf xs ys :: Bool -> Type)

Defined in Fcf.Data.List

type Eval (IsInfixOf xs ys :: Bool -> Type) = Eval ((Any (IsPrefixOf xs) :: [[a]] -> Bool -> Type) =<< Tails ys)

Searching

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

Return True if an element is in a list.

See also FindIndex.

Example

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

Instances

type Eval (Elem a2 as :: Bool -> Type)

Defined in Fcf.Data.List

type Eval (Elem a2 as :: Bool -> Type) = Eval ((IsJust :: Maybe Nat -> Bool -> Type) =<< FindIndex (TyEq a2 :: a1 -> Bool -> Type) as)

data Lookup :: k -> [(k, b)] -> Exp (Maybe b)

Find an element associated with a key in an association list.

Instances

type Eval (Lookup a as :: Maybe b -> Type)

Defined in Fcf.Data.List

type Eval (Lookup a as :: Maybe b -> Type) = Eval (Map (Snd :: (k, b) -> b -> Type) (Eval (Find ((TyEq a :: k -> Bool -> Type) <=< (Fst :: (k, b) -> k -> Type)) as)))

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

Find Just the first element satisfying a predicate, or evaluate to Nothing if no element satisfies the predicate.

Example

>>> :kind! Eval (Find (TyEq 0) '[1,2,3])
Eval (Find (TyEq 0) '[1,2,3]) :: Maybe Nat
= 'Nothing

>>> :kind! Eval (Find (TyEq 0) '[1,2,3,0])
Eval (Find (TyEq 0) '[1,2,3,0]) :: Maybe Nat
= 'Just 0

Instances

type Eval (Find p (a2 ': as) :: Maybe a1 -> Type)

Defined in Fcf.Data.List

type Eval (Find p (a2 ': as) :: Maybe a1 -> Type) = Eval (If (Eval (p a2)) (Pure (Just a2)) (Find p as))

type Eval (Find _p ([] :: [a]) :: Maybe a -> Type)

Defined in Fcf.Data.List

type Eval (Find _p ([] :: [a]) :: Maybe a -> Type) = (Nothing :: Maybe a)

data Filter :: (a -> Exp Bool) -> [a] -> Exp [a]

Keep all elements that satisfy a predicate, remove all that don't.

Example

>>> :kind! Eval (Filter ((>) 3) '[1,2,3,0])
Eval (Filter ((>) 3) '[1,2,3,0]) :: [Nat]
= '[1, 2, 0]

Instances

type Eval (Filter p (a2 ': as) :: [a1] -> Type)

Defined in Fcf.Data.List

type Eval (Filter p (a2 ': as) :: [a1] -> Type) = Eval (If (Eval (p a2)) ((:) a2 <$> Filter p as) (Filter p as))

type Eval (Filter _p ([] :: [a]) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Filter _p ([] :: [a]) :: [a] -> Type) = ([] :: [a])

data Partition :: (a -> Exp Bool) -> [a] -> Exp ([a], [a])

Split a list into one where all elements satisfy a predicate, and a second where no elements satisfy it.

Example

>>> :kind! Eval (Partition ((>=) 35) '[ 20, 30, 40, 50])
Eval (Partition ((>=) 35) '[ 20, 30, 40, 50]) :: ([Nat], [Nat])
= '( '[20, 30], '[40, 50])

Instances

type Eval (Partition p lst :: ([a], [a]) -> Type)

Defined in Fcf.Data.List

type Eval (Partition p lst :: ([a], [a]) -> Type)

Indexing lists

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

Find the index of an element satisfying the predicate.

Example

>>> :kind! Eval (FindIndex ((<=) 3) '[1,2,3,1,2,3])
Eval (FindIndex ((<=) 3) '[1,2,3,1,2,3]) :: Maybe Nat
= 'Just 2

>>> :kind! Eval (FindIndex ((>) 0) '[1,2,3,1,2,3])
Eval (FindIndex ((>) 0) '[1,2,3,1,2,3]) :: Maybe Nat
= 'Nothing

Instances

type Eval (FindIndex p (a2 ': as) :: Maybe Nat -> Type)

Defined in Fcf.Data.List

type Eval (FindIndex p (a2 ': as) :: Maybe Nat -> Type) = Eval (If (Eval (p a2)) (Pure (Just 0)) ((Map ((+) 1) :: Maybe Nat -> Maybe Nat -> Type) =<< FindIndex p as))

type Eval (FindIndex _p ([] :: [a]) :: Maybe Nat -> Type)

Defined in Fcf.Data.List

type Eval (FindIndex _p ([] :: [a]) :: Maybe Nat -> Type) = (Nothing :: Maybe Nat)

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

Modify an element at a given index.

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

Example

>>> :kind! Eval (SetIndex 2 7 '[1,2,3])
Eval (SetIndex 2 7 '[1,2,3]) :: [Nat]
= '[1, 2, 7]

Instances

type Eval (SetIndex n a' as :: [k] -> Type)

Defined in Fcf.Data.List

type Eval (SetIndex n a' as :: [k] -> Type)

Zipping and unzipping

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

Combine elements of two lists pairwise.

Example

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

Instances

type Eval (ZipWith f (a2 ': as) (b2 ': bs) :: [c] -> Type)

Defined in Fcf.Data.List

type Eval (ZipWith f (a2 ': as) (b2 ': bs) :: [c] -> Type) = Eval (f a2 b2) ': Eval (ZipWith f as bs)

type Eval (ZipWith _f _as ([] :: [b]) :: [c] -> Type)

Defined in Fcf.Data.List

type Eval (ZipWith _f _as ([] :: [b]) :: [c] -> Type) = ([] :: [c])

type Eval (ZipWith _f ([] :: [a]) _bs :: [c] -> Type)

Defined in Fcf.Data.List

type Eval (ZipWith _f ([] :: [a]) _bs :: [c] -> Type) = ([] :: [c])

data Zip :: [a] -> [b] -> Exp [(a, b)]

Instances

type Eval (Zip as bs :: [(a, b)] -> Type)

Defined in Fcf.Data.List

type Eval (Zip as bs :: [(a, b)] -> Type) = Eval (ZipWith (Pure2 ((,) :: a -> b -> (a, b))) as bs)

data Unzip :: Exp [(a, b)] -> Exp ([a], [b])

Instances

type Eval (Unzip as :: ([a], [b]) -> Type)

Defined in Fcf.Data.List

type Eval (Unzip as :: ([a], [b]) -> Type) = Eval (Foldr (Cons2 :: (a, b) -> ([a], [b]) -> ([a], [b]) -> Type) ((,) ([] :: [a]) ([] :: [b])) (Eval as))