Safe Haskell	Safe
Language	Haskell2010

Fcf.Data.List

Description

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

Expand

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

Instances

type Eval (Foldr f y (x ': xs) :: a2 -> Type) Source #
Instance details Defined in Fcf.Data.List 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) Source #
Instance details Defined in Fcf.Data.List type Eval (Foldr f y ([] :: [a1]) :: a2 -> Type) = y

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

Type-level Unfoldr.

Example

Expand

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

Example

Expand

>>> :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) Source #
Instance details Defined in Fcf.Data.List type Eval (Cons a2 as :: [a1] -> Type) = a2 ': as

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

Type-level list catenation.

Example

Expand

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

Instances

type Eval ((x ': xs) ++ ys :: [a] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval ((x ': xs) ++ ys :: [a] -> Type) = x ': Eval (xs ++ ys)
type Eval (([] :: [a]) ++ ys :: [a] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (([] :: [a]) ++ ys :: [a] -> Type) = ys

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

Concat for lists.

Example

Expand

>>> :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 lsts :: [a] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Concat lsts :: [a] -> Type) = Eval (Foldr ((++) :: [a] -> [a] -> [a] -> Type) ([] :: [a]) lsts)

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

ConcatMap for lists.

Instances

type Eval (ConcatMap f lst :: [a2] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (ConcatMap f lst :: [a2] -> Type) = Eval (Concat (Eval (Map f lst)))

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

Instances

type Eval (Filter p (a2 ': as) :: [a1] -> Type) Source #
Instance details 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) Source #
Instance details Defined in Fcf.Data.List type Eval (Filter _p ([] :: [a]) :: [a] -> Type) = ([] :: [a])

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

Instances

type Eval (Head (a2 ': _as) :: Maybe a1 -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Head (a2 ': _as) :: Maybe a1 -> Type) = Just a2
type Eval (Head ([] :: [a]) :: Maybe a -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Head ([] :: [a]) :: Maybe a -> Type) = (Nothing :: Maybe a)

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

Instances

type Eval (Last (a2 ': (b ': as)) :: Maybe a1 -> Type) Source #
Instance details 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) Source #
Instance details Defined in Fcf.Data.List type Eval (Last (a2 ': ([] :: [a1])) :: Maybe a1 -> Type) = Just a2
type Eval (Last ([] :: [a]) :: Maybe a -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Last ([] :: [a]) :: Maybe a -> Type) = (Nothing :: Maybe a)

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

Instances

type Eval (Tail (_a ': as) :: Maybe [a] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Tail (_a ': as) :: Maybe [a] -> Type) = Just as
type Eval (Tail ([] :: [a]) :: Maybe [a] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Tail ([] :: [a]) :: Maybe [a] -> Type) = (Nothing :: Maybe [a])

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

Instances

type Eval (Init (a2 ': (b ': as)) :: Maybe [a1] -> Type) Source #
Instance details 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))
type Eval (Init (a2 ': ([] :: [a1])) :: Maybe [a1] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Init (a2 ': ([] :: [a1])) :: Maybe [a1] -> Type) = Just ([] :: [a1])
type Eval (Init ([] :: [a]) :: Maybe [a] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Init ([] :: [a]) :: Maybe [a] -> Type) = (Nothing :: Maybe [a])

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

Instances

type Eval (Null (a2 ': as) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Null (a2 ': as) :: Bool -> Type) = False
type Eval (Null ([] :: [a]) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Null ([] :: [a]) :: Bool -> Type) = True

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

Instances

type Eval (Length (a2 ': as) :: Nat -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Length (a2 ': as) :: Nat -> Type) = 1 + Eval (Length as)
type Eval (Length ([] :: [a]) :: Nat -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Length ([] :: [a]) :: Nat -> Type) = 0

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

Type-level Replicate for lists.

Example

Expand

>>> :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) Source #
Instance details Defined in Fcf.Data.List type Eval (Replicate n a2 :: [a1] -> Type)

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

Instances

type Eval (Find p (a2 ': as) :: Maybe a1 -> Type) Source #
Instance details 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) Source #
Instance details Defined in Fcf.Data.List type Eval (Find _p ([] :: [a]) :: Maybe a -> Type) = (Nothing :: Maybe a)

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

Find the index of an element satisfying the predicate.

Instances

type Eval (FindIndex p (a2 ': as) :: Maybe Nat -> Type) Source #
Instance details 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) Source #
Instance details Defined in Fcf.Data.List type Eval (FindIndex _p ([] :: [a]) :: Maybe Nat -> Type) = (Nothing :: Maybe Nat)

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

Type-level Elem for lists.

Example

Expand

>>> :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) Source #
Instance details 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) Source #

Find an element associated with a key.

Instances

type Eval (Lookup a as :: Maybe b -> Type) Source #
Instance details 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 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.

Instances

type Eval (SetIndex n a' as :: [k] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (SetIndex n a' as :: [k] -> Type)

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

Instances

type Eval (ZipWith f (a2 ': as) (b2 ': bs) :: [c] -> Type) Source #
Instance details 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) Source #
Instance details Defined in Fcf.Data.List type Eval (ZipWith _f _as ([] :: [b]) :: [c] -> Type) = ([] :: [c])
type Eval (ZipWith _f ([] :: [a]) _bs :: [c] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (ZipWith _f ([] :: [a]) _bs :: [c] -> Type) = ([] :: [c])

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

Instances

type Eval (Zip as bs :: [(a, b)] -> Type) Source #
Instance details 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]) Source #

Instances

type Eval (Unzip as :: ([a], [b]) -> Type) Source #
Instance details 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))

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

Instances

type Eval (Cons2 ((,) a3 b) ((,) as bs) :: ([a2], [a1]) -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Cons2 ((,) a3 b) ((,) as bs) :: ([a2], [a1]) -> Type) = (,) (a3 ': as) (b ': bs)

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

Type-level list take.

Example

Expand

>>> :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) Source #
Instance details Defined in Fcf.Data.List type Eval (Take n as :: [a] -> Type)

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

Type-level list drop.

Example

Expand

>>> :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) Source #
Instance details Defined in Fcf.Data.List type Eval (Drop n as :: [a] -> Type)

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

Type-level list takeWhile.

Example

Expand

>>> :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) Source #
Instance details 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) Source #
Instance details Defined in Fcf.Data.List type Eval (TakeWhile p ([] :: [a]) :: [a] -> Type) = ([] :: [a])

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

Type-level list dropWhile.

Example

Expand

: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) Source #
Instance details 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) Source #
Instance details Defined in Fcf.Data.List type Eval (DropWhile p ([] :: [a]) :: [a] -> Type) = ([] :: [a])

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

Type-level list reverse.

Example

Expand

>>> :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) Source #
Instance details Defined in Fcf.Data.List type Eval (Reverse l :: [a] -> Type)

type Eval (Unfoldr f c :: [a] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Unfoldr f c :: [a] -> Type)

type Eval (UnList y f xs :: a2 -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (UnList y f xs :: a2 -> Type) = Eval (Foldr f y xs)