fcf-containers-0.1.0: Data structures and algorithms for first-class-families

Fcf.Alg.List

Description

Fcf.Alg.List

Type-level ListF to be used with Cata, Ana and Hylo.

This module also contains other list-related functions (that might move to other place some day).

Synopsis

Documentation

data ListF a b Source #

Base functor for a list of type [a].

Constructors

 ConsF a b NilF
Instances
 type Eval (ListToFix (a2 ': as) :: Fix (ListF a1) -> Type) Source # Instance detailsDefined in Fcf.Alg.List type Eval (ListToFix (a2 ': as) :: Fix (ListF a1) -> Type) = Fix (ConsF a2 (Eval (ListToFix as))) type Eval (ListToFix ([] :: [a]) :: Fix (ListF a) -> Type) Source # Instance detailsDefined in Fcf.Alg.List type Eval (ListToFix ([] :: [a]) :: Fix (ListF a) -> Type) = Fix (NilF :: ListF a (Fix (ListF a))) type Eval (Map f (ConsF a3 b2) :: ListF a2 b1 -> Type) Source # Instance detailsDefined in Fcf.Alg.List type Eval (Map f (ConsF a3 b2) :: ListF a2 b1 -> Type) = ConsF a3 (Eval (f b2)) type Eval (Map f (NilF :: ListF a2 a1) :: ListF a2 b -> Type) Source # Instance detailsDefined in Fcf.Alg.List type Eval (Map f (NilF :: ListF a2 a1) :: ListF a2 b -> Type) = (NilF :: ListF a2 b)

data ListToFix :: [a] -> Exp (Fix (ListF a)) Source #

ListToFix can be used to turn a norma type-level list into the base functor type ListF, to be used with e.g. Cata. For examples in use, see LenAlg and SumAlg.

Ideally, we would have one ToFix type-level function for which we could give type instances for different type-level types, like lists, trees etc. See TODO.md.

Instances
 type Eval (ListToFix (a2 ': as) :: Fix (ListF a1) -> Type) Source # Instance detailsDefined in Fcf.Alg.List type Eval (ListToFix (a2 ': as) :: Fix (ListF a1) -> Type) = Fix (ConsF a2 (Eval (ListToFix as))) type Eval (ListToFix ([] :: [a]) :: Fix (ListF a) -> Type) Source # Instance detailsDefined in Fcf.Alg.List type Eval (ListToFix ([] :: [a]) :: Fix (ListF a) -> Type) = Fix (NilF :: ListF a (Fix (ListF a)))

data LenAlg :: Algebra (ListF a) Nat Source #

Example algebra to calculate list length.

>>> :kind! Eval (Cata LenAlg =<< ListToFix '[1,2,3])
Eval (Cata LenAlg =<< ListToFix '[1,2,3]) :: Nat
= 3
Instances
 type Eval (LenAlg (ConsF a2 b) :: Nat -> Type) Source # Instance detailsDefined in Fcf.Alg.List type Eval (LenAlg (ConsF a2 b) :: Nat -> Type) = 1 + b type Eval (LenAlg (NilF :: ListF a Nat) :: Nat -> Type) Source # Instance detailsDefined in Fcf.Alg.List type Eval (LenAlg (NilF :: ListF a Nat) :: Nat -> Type) = 0

data SumAlg :: Algebra (ListF Nat) Nat Source #

Example algebra to calculate the sum of Nats in a list.

>>> :kind! Eval (Cata SumAlg =<< ListToFix '[1,2,3,4])
Eval (Cata SumAlg =<< ListToFix '[1,2,3,4]) :: Nat
= 10
Instances
 type Eval (SumAlg (ConsF a b) :: Nat -> Type) Source # Instance detailsDefined in Fcf.Alg.List type Eval (SumAlg (ConsF a b) :: Nat -> Type) = a + b type Eval (SumAlg (NilF :: ListF Nat Nat)) Source # Instance detailsDefined in Fcf.Alg.List type Eval (SumAlg (NilF :: ListF Nat Nat)) = 0

data ProdAlg :: Algebra (ListF Nat) Nat Source #

Example algebra to calculate the prod of Nats in a list.

>>> :kind! Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4])
Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4]) :: Nat
= 24
Instances
 type Eval (ProdAlg (ConsF a b) :: Nat -> Type) Source # Instance detailsDefined in Fcf.Alg.List type Eval (ProdAlg (ConsF a b) :: Nat -> Type) = a * b type Eval (ProdAlg (NilF :: ListF Nat Nat)) Source # Instance detailsDefined in Fcf.Alg.List type Eval (ProdAlg (NilF :: ListF Nat Nat)) = 1

data Sum :: [Nat] -> Exp Nat Source #

Sum a Nat-list.

Example

>>> :kind! Eval (Sum '[1,2,3])
Eval (Sum '[1,2,3]) :: Nat
= 6
Instances
 type Eval (Sum ns :: Nat -> Type) Source # Instance detailsDefined in Fcf.Alg.List type Eval (Sum ns :: Nat -> Type) = Eval (Foldr (+) 0 ns)

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

Partition

Example

>>> :kind! Eval (Fcf.Alg.List.Partition ((>=) 35) '[ 20, 30, 40, 50])
Eval (Fcf.Alg.List.Partition ((>=) 35) '[ 20, 30, 40, 50]) :: ([Nat],
[Nat])
= '( '[20, 30], '[40, 50])
Instances
 type Eval (Partition p lst :: ([a], [a]) -> Type) Source # Instance detailsDefined in Fcf.Alg.List type Eval (Partition p lst :: ([a], [a]) -> Type) = Eval (Foldr (PartHelp p) ((,) ([] :: [a]) ([] :: [a])) lst)

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

Instances
 type Eval (PartHelp p a2 ((,) xs ys) :: ([a1], [a1]) -> Type) Source # Instance detailsDefined in Fcf.Alg.List type Eval (PartHelp p a2 ((,) xs ys) :: ([a1], [a1]) -> Type) = If (Eval (p a2)) ((,) (a2 ': xs) ys) ((,) xs (a2 ': ys))

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

Note: Once Fcf releases a new version, I'll remove this, TODO

Instances
 type Eval (Elem a2 as :: Bool -> Type) Source # Instance detailsDefined in Fcf.Alg.List type Eval (Elem a2 as :: Bool -> Type) = Eval ((IsJust :: Maybe Nat -> Bool -> Type) =<< FindIndex (TyEq a2 :: a1 -> Bool -> Type) as)

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]

Note: Once Fcf releases a new version, I'll remove this, TODO

Instances
 type Eval (Concat lsts :: [a] -> Type) Source # Instance detailsDefined in Fcf.Alg.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.

Note: Once Fcf releases a new version, I'll remove this, TODO

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

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]

Note: Once Fcf releases a new version, I'll remove this, TODO

Instances
 type Eval (Unfoldr f c :: [a] -> Type) Source # Instance detailsDefined in Fcf.Alg.List type Eval (Unfoldr f c :: [a] -> Type) = Eval (UnfoldrCase f (f @@ c))

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

Instances
 type Eval (UnfoldrCase _ (Nothing :: Maybe (a, b)) :: [a] -> Type) Source # Instance detailsDefined in Fcf.Alg.List type Eval (UnfoldrCase _ (Nothing :: Maybe (a, b)) :: [a] -> Type) = ([] :: [a]) type Eval (UnfoldrCase f (Just ab) :: [a1] -> Type) Source # Instance detailsDefined in Fcf.Alg.List type Eval (UnfoldrCase f (Just ab) :: [a1] -> Type) = Eval (Fst ab) ': Eval (Unfoldr f (Eval (Snd ab)))