first-class-families-0.6.0.0: First class type families

Safe Haskell | Safe
Language | Haskell2010

Fcf.Data.List

Description

Lists.

Synopsis

- data Foldr :: (a -> b -> Exp b) -> b -> [a] -> Exp b
- data UnList :: b -> (a -> b -> Exp b) -> [a] -> Exp b
- data Cons :: a -> [a] -> Exp [a]
- data (++) :: [a] -> [a] -> Exp [a]
- 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 Find :: (a -> Exp Bool) -> [a] -> Exp (Maybe a)
- data FindIndex :: (a -> Exp Bool) -> [a] -> Exp (Maybe Nat)
- type Elem a as = IsJust =<< FindIndex (TyEq a) as
- type Lookup (a :: k) (as :: [(k, b)]) = (Map Snd (Eval (Find (TyEq a <=< Fst) as)) :: Exp (Maybe b))
- data SetIndex :: Nat -> a -> [a] -> Exp [a]
- data ZipWith :: (a -> b -> Exp c) -> [a] -> [b] -> Exp [c]
- type Zip = ZipWith (Pure2 (,))
- data Unzip :: Exp [(a, b)] -> Exp ([a], [b])
- data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])

# Documentation

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

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 UnList :: b -> (a -> b -> Exp b) -> [a] -> Exp b Source #

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

Instances

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)

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

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 #

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 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) = If (Eval (p a2)) (a2 ': Eval (Filter p as)) (Eval (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 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) = If (Eval (p a2)) (Just a2) (Eval (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)

type Elem a as = IsJust =<< FindIndex (TyEq a) as Source #

type Lookup (a :: k) (as :: [(k, b)]) = (Map Snd (Eval (Find (TyEq a <=< Fst) as)) :: Exp (Maybe b)) Source #

Find an element associated with a key. ``Lookup` :: k -> [(k, b)] -> `Exp` (`Maybe` b)`

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

type Zip = ZipWith (Pure2 (,)) Source #

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

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)