Fcf.Alg.List

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

Documentation

>>> import           Fcf.Combinators

data ListF a b

Base functor for a list of type [a].

Constructors

ConsF a b

NilF

Instances

type Eval (ListToFix (a2 ': as) :: Fix (ListF a1) -> Type)

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

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

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

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

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)

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

Defined 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

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)

Defined in Fcf.Alg.List

type Eval (LenAlg ('ConsF a2 b) :: Nat -> Type) = 1 + b

type Eval (LenAlg ('NilF :: ListF a Nat) :: Nat -> Type)

Defined in Fcf.Alg.List

type Eval (LenAlg ('NilF :: ListF a Nat) :: Nat -> Type) = 0

data SumAlg :: Algebra (ListF Nat) Nat

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)

Defined in Fcf.Alg.List

type Eval (SumAlg ('ConsF a b) :: Nat -> Type) = a + b

type Eval (SumAlg ('NilF :: ListF Nat Nat))

Defined in Fcf.Alg.List

type Eval (SumAlg ('NilF :: ListF Nat Nat)) = 0

data ProdAlg :: Algebra (ListF Nat) Nat

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)

Defined in Fcf.Alg.List

type Eval (ProdAlg ('ConsF a b) :: Nat -> Type) = a * b

type Eval (ProdAlg ('NilF :: ListF Nat Nat))

Defined in Fcf.Alg.List

type Eval (ProdAlg ('NilF :: ListF Nat Nat)) = 1

data Sum :: [Nat] -> Exp Nat

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)

Defined in Fcf.Alg.List

type Eval (Sum ns :: Nat -> Type) = Eval (Foldr (+) 0 ns)

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

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)

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

Instances

type Eval (PartHelp p a2 '(xs, ys) :: ([a1], [a1]) -> Type)

Defined 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 All :: [Bool] -> Exp Bool

Give true if all of the booleans in the list are true.

Example

>>> :kind! Eval (All '[ 'True, 'True])
Eval (All '[ 'True, 'True]) :: Bool
= 'True

>>> :kind! Eval (All '[ 'True, 'True, 'False])
Eval (All '[ 'True, 'True, 'False]) :: Bool
= 'False

Instances

type Eval (All lst :: Bool -> Type)

Defined in Fcf.Alg.List

type Eval (All lst :: Bool -> Type) = Eval (Foldr (&&) 'True lst)

data Any :: [Bool] -> Exp Bool

Give true if any of the booleans in the list is true.

Example

>>> :kind! Eval (Any '[ 'True, 'True])
Eval (Any '[ 'True, 'True]) :: Bool
= 'True

>>> :kind! Eval (Any '[ 'False, 'False])
Eval (Any '[ 'False, 'False]) :: Bool
= 'False

Instances

type Eval (Any lst :: Bool -> Type)

Defined in Fcf.Alg.List

type Eval (Any lst :: Bool -> Type) = Eval (Foldr (||) 'False lst)