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

Copyright(c) gspia 2020-
LicenseBSD
Maintainergspia
Safe HaskellSafe
LanguageHaskell2010

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

>>> import           Fcf.Combinators

data ListF a b Source #

Base functor for a list of type [a].

Constructors

ConsF a b 
NilF 
Instances
type Eval (DedupAlg (ConsF ((,) a2 as) ((,) _fxs past)) :: [a1] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (DedupAlg (ConsF ((,) a2 as) ((,) _fxs past)) :: [a1] -> Type) = Eval (If (Eval (TyEq (Eval (Elem a2 past)) True)) (Pure past) (Pure (a2 ': as)))
type Eval (DedupAlg (NilF :: ListF (a, [a]) (Fix (ListF (a, [a])), [a])) :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (DedupAlg (NilF :: ListF (a, [a]) (Fix (ListF (a, [a])), [a])) :: [a] -> Type) = ([] :: [a])
type Eval (EvensStrip (ConsF x y) :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (EvensStrip (ConsF x y) :: [a] -> Type) = x ': Eval (Attr y)
type Eval (EvensStrip (NilF :: ListF a (Ann (ListF a) [a])) :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (EvensStrip (NilF :: ListF a (Ann (ListF a) [a])) :: [a] -> Type) = ([] :: [a])
type Eval (EvensAlg (ConsF _ rst) :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (EvensAlg (ConsF _ rst) :: [a] -> Type) = Eval ((EvensStrip :: ListF a (Ann (ListF a) [a]) -> [a] -> Type) =<< Strip rst)
type Eval (EvensAlg (NilF :: ListF a (Ann (ListF a) [a])) :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (EvensAlg (NilF :: ListF a (Ann (ListF a) [a])) :: [a] -> Type) = ([] :: [a])
type Eval (ListToParaFix (a2 ': as) :: Fix (ListF (a1, [a1])) -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (ListToParaFix (a2 ': as) :: Fix (ListF (a1, [a1])) -> Type) = Fix (ConsF ((,) a2 as) (Eval (ListToParaFix as)))
type Eval (ListToParaFix ([] :: [a]) :: Fix (ListF (a, [a])) -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (ListToParaFix ([] :: [a]) :: Fix (ListF (a, [a])) -> Type) = Fix (NilF :: ListF (a, [a]) (Fix (ListF (a, [a]))))
type Eval (ListToFix (a2 ': as) :: Fix (ListF a1) -> Type) Source # 
Instance details

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

Defined in Fcf.Alg.List

type Eval (ListToFix ([] :: [a]) :: Fix (ListF a) -> Type) = Fix (NilF :: ListF a (Fix (ListF a)))
type Eval (SlidingAlg n (ConsF ((,) a2 as) ((,) _fxs past)) :: [[a1]] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (SlidingAlg n (ConsF ((,) a2 as) ((,) _fxs past)) :: [[a1]] -> Type) = Eval (Take n (a2 ': as)) ': past
type Eval (SlidingAlg _ (NilF :: ListF (a, [a]) (Fix (ListF (a, [a])), [[a]])) :: [[a]] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (SlidingAlg _ (NilF :: ListF (a, [a]) (Fix (ListF (a, [a])), [[a]])) :: [[a]] -> Type) = ([] :: [[a]])
type Eval (Map f (ConsF a3 b2) :: ListF a2 b1 -> Type) Source # 
Instance details

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

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

Example

Expand
>>> :kind! Eval (ListToFix '[1,2,3])
Eval (ListToFix '[1,2,3]) :: Fix (ListF Nat)
= 'Fix ('ConsF 1 ('Fix ('ConsF 2 ('Fix ('ConsF 3 ('Fix 'NilF))))))
Instances
type Eval (ListToFix (a2 ': as) :: Fix (ListF a1) -> Type) Source # 
Instance details

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

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 Source #

Example algebra to calculate list length.

Example

Expand
>>> :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 details

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

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

Example

Expand
>>> :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 details

Defined in Fcf.Alg.List

type Eval (SumAlg (ConsF a b) :: Nat -> Type) = a + b
type Eval (SumAlg (NilF :: ListF Nat Nat)) Source # 
Instance details

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

Example

Expand
>>> :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 details

Defined in Fcf.Alg.List

type Eval (ProdAlg (ConsF a b) :: Nat -> Type) = a * b
type Eval (ProdAlg (NilF :: ListF Nat Nat)) Source # 
Instance details

Defined in Fcf.Alg.List

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

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

Form a Fix-structure that can be used with Para.

Example

Expand
>>> :kind! Eval (ListToParaFix '[1,2,3])
Eval (ListToParaFix '[1,2,3]) :: Fix (ListF (Nat, [Nat]))
= 'Fix
    ('ConsF
       '(1, '[2, 3])
       ('Fix ('ConsF '(2, '[3]) ('Fix ('ConsF '(3, '[]) ('Fix 'NilF))))))
Instances
type Eval (ListToParaFix (a2 ': as) :: Fix (ListF (a1, [a1])) -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (ListToParaFix (a2 ': as) :: Fix (ListF (a1, [a1])) -> Type) = Fix (ConsF ((,) a2 as) (Eval (ListToParaFix as)))
type Eval (ListToParaFix ([] :: [a]) :: Fix (ListF (a, [a])) -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (ListToParaFix ([] :: [a]) :: Fix (ListF (a, [a])) -> Type) = Fix (NilF :: ListF (a, [a]) (Fix (ListF (a, [a]))))

data DedupAlg :: RAlgebra (ListF (a, [a])) [a] Source #

Example from recursion-package by Vanessa McHale.

This removes duplicates from a list (by keeping the right-most one).

Example

Expand
>>> :kind! Eval (Para DedupAlg =<< ListToParaFix '[1,1,3,2,5,1,3,2])
Eval (Para DedupAlg =<< ListToParaFix '[1,1,3,2,5,1,3,2]) :: [Nat]
= '[5, 1, 3, 2]
Instances
type Eval (DedupAlg (ConsF ((,) a2 as) ((,) _fxs past)) :: [a1] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (DedupAlg (ConsF ((,) a2 as) ((,) _fxs past)) :: [a1] -> Type) = Eval (If (Eval (TyEq (Eval (Elem a2 past)) True)) (Pure past) (Pure (a2 ': as)))
type Eval (DedupAlg (NilF :: ListF (a, [a]) (Fix (ListF (a, [a])), [a])) :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (DedupAlg (NilF :: ListF (a, [a]) (Fix (ListF (a, [a])), [a])) :: [a] -> Type) = ([] :: [a])

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

Example from Recursion Schemes by example by Tim Williams.

Example

Expand
>>> :kind! Eval (Sliding 3 '[1,2,3,4,5,6])
Eval (Sliding 3 '[1,2,3,4,5,6]) :: [[Nat]]
= '[ '[1, 2, 3], '[2, 3, 4], '[3, 4, 5], '[4, 5, 6], '[5, 6], '[6]]
Instances
type Eval (Sliding n lst :: [[a]] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (Sliding n lst :: [[a]] -> Type) = Eval (Para (SlidingAlg n :: ListF (a, [a]) (Fix (ListF (a, [a])), [[a]]) -> [[a]] -> Type) =<< ListToParaFix lst)

data SlidingAlg :: Nat -> RAlgebra (ListF (a, [a])) [[a]] Source #

Tim Williams, Recursion Schemes by example, example for Para. See Sliding-function.

Instances
type Eval (SlidingAlg n (ConsF ((,) a2 as) ((,) _fxs past)) :: [[a1]] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (SlidingAlg n (ConsF ((,) a2 as) ((,) _fxs past)) :: [[a1]] -> Type) = Eval (Take n (a2 ': as)) ': past
type Eval (SlidingAlg _ (NilF :: ListF (a, [a]) (Fix (ListF (a, [a])), [[a]])) :: [[a]] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (SlidingAlg _ (NilF :: ListF (a, [a]) (Fix (ListF (a, [a])), [[a]])) :: [[a]] -> Type) = ([] :: [[a]])

data EvensStrip :: ListF a (Ann (ListF a) [a]) -> Exp [a] Source #

Tim Williams, Recursion Schemes by example, example for Histo.

Instances
type Eval (EvensStrip (ConsF x y) :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (EvensStrip (ConsF x y) :: [a] -> Type) = x ': Eval (Attr y)
type Eval (EvensStrip (NilF :: ListF a (Ann (ListF a) [a])) :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (EvensStrip (NilF :: ListF a (Ann (ListF a) [a])) :: [a] -> Type) = ([] :: [a])

data EvensAlg :: ListF a (Ann (ListF a) [a]) -> Exp [a] Source #

Tim Williams, Recursion Schemes by example, example for Histo.

Instances
type Eval (EvensAlg (ConsF _ rst) :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (EvensAlg (ConsF _ rst) :: [a] -> Type) = Eval ((EvensStrip :: ListF a (Ann (ListF a) [a]) -> [a] -> Type) =<< Strip rst)
type Eval (EvensAlg (NilF :: ListF a (Ann (ListF a) [a])) :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (EvensAlg (NilF :: ListF a (Ann (ListF a) [a])) :: [a] -> Type) = ([] :: [a])

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

This picks up the elements on even positions on a list and is an example on how to use Histo. This example is from Tim Williams, Recursion Schemes by example.

Example

Expand
>>> :kind! Eval (Evens =<< RunInc 8)
Eval (Evens =<< RunInc 8) :: [Nat]
= '[2, 4, 6, 8]
Instances
type Eval (Evens lst :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (Evens lst :: [a] -> Type) = Eval (Histo (EvensAlg :: ListF a (Ann (ListF a) [a]) -> [a] -> Type) =<< ListToFix lst)

data NumIter :: a -> Nat -> Exp (Maybe (a, Nat)) Source #

For the ListRunAlg

Instances
type Eval (NumIter a s :: Maybe (k, Nat) -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (NumIter a s :: Maybe (k, Nat) -> Type) = If (Eval (s > 0)) (Just ((,) a (s - 1))) (Nothing :: Maybe (k, Nat))

data ListRunAlg :: Nat -> Exp (Maybe (Nat, Nat)) Source #

For the RunInc

Instances
type Eval (ListRunAlg s :: Maybe (Nat, Nat) -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (ListRunAlg s :: Maybe (Nat, Nat) -> Type) = Eval (NumIter s s)

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

Construct a run (that is, a natuaral number sequence from 1 to arg).

Example

Expand
>>> :kind! Eval (RunInc 8)
Eval (RunInc 8) :: [Nat]
= '[1, 2, 3, 4, 5, 6, 7, 8]
Instances
type Eval (RunInc n :: [Nat] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (RunInc n :: [Nat] -> Type) = Eval ((Reverse :: [Nat] -> [Nat] -> Type) =<< Unfoldr ListRunAlg n)

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

Sum a Nat-list.

Example

Expand
>>> :kind! Eval (Sum '[1,2,3])
Eval (Sum '[1,2,3]) :: Nat
= 6
Instances
type Eval (Sum ns :: Nat -> Type) Source # 
Instance details

Defined 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

Expand
>>> :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 details

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

Instances
type Eval (PartHelp p a2 ((,) xs ys) :: ([a1], [a1]) -> Type) Source # 
Instance details

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 Intersperse :: a -> [a] -> Exp [a] Source #

Intersperse for type-level lists.

Example

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

Defined in Fcf.Alg.List

type Eval (Intersperse _ ([] :: [a]) :: [a] -> Type) = ([] :: [a])
type Eval (Intersperse sep (x ': xs) :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

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

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

Instances
type Eval (PrependToAll sep (x ': xs) :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (PrependToAll sep (x ': xs) :: [a] -> Type) = sep ': (x ': Eval (PrependToAll sep xs))
type Eval (PrependToAll _ ([] :: [a]) :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

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

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

Intercalate for type-level lists.

Example

Expand
>>> :kind! Eval (Intercalate '[", "] '[ '["Lorem"], '["ipsum"], '["dolor"] ])
Eval (Intercalate '[", "] '[ '["Lorem"], '["ipsum"], '["dolor"] ]) :: [TL.Symbol]
= '["Lorem", ", ", "ipsum", ", ", "dolor"]
Instances
type Eval (Intercalate xs xss :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

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

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

Span, applied to a predicate p and a type-level list xs, returns a type-level tuple where first element is longest prefix (possibly empty) of xs of elements that satisfy p and second element is the remainder of the list:

Example

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

Defined in Fcf.Alg.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]) Source #

Break, applied to a predicate p and a type-level list xs, returns a type-level tuple where first element is longest prefix (possibly empty) of xs of elements that do not satisfy p and second element is the remainder of the list:

Example

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

Defined in Fcf.Alg.List

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

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

IsPrefixOf takes two type-level lists and returns true iff the first list is a prefix of the second.

Example

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

Defined in Fcf.Alg.List

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

type family IsPrefixOf_ (xs :: [a]) (ys :: [a]) :: Bool where ... Source #

Equations

IsPrefixOf_ '[] _ = True 
IsPrefixOf_ _ '[] = False 
IsPrefixOf_ (x ': xs) (y ': ys) = Eval (Eval (TyEq x y) && IsPrefixOf_ xs ys) 

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

IsSuffixOf take two type-level lists and returns true iff the first list is a suffix of the second.

Example

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

Defined in Fcf.Alg.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 Source #

IsInfixOf take two type-level lists and returns true iff the first list is a infix of the second.

Example

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

Defined in Fcf.Alg.List

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

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

Tails

Example

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

Defined in Fcf.Alg.List

type Eval (Tails (a2 ': as) :: [[a1]] -> Type) = (a2 ': as) ': Eval (Tails as)
type Eval (Tails ([] :: [a]) :: [[a]] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

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

data And :: [Bool] -> Exp Bool Source #

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

Example

Expand
>>> :kind! Eval (And '[ 'True, 'True])
Eval (And '[ 'True, 'True]) :: Bool
= 'True
>>> :kind! Eval (And '[ 'True, 'True, 'False])
Eval (And '[ 'True, 'True, 'False]) :: Bool
= 'False
Instances
type Eval (And lst :: Bool -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

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

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

Type-level All.

Example

Expand
>>> :kind! Eval (All (Flip (<) 6) '[0,1,2,3,4,5])
Eval (All (Flip (<) 6) '[0,1,2,3,4,5]) :: Bool
= 'True
>>> :kind! Eval (All (Flip (<) 5) '[0,1,2,3,4,5])
Eval (All (Flip (<) 5) '[0,1,2,3,4,5]) :: Bool
= 'False
Instances
type Eval (All p lst :: Bool -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (All p lst :: Bool -> Type) = Eval (And =<< Map p lst)

data Or :: [Bool] -> Exp Bool Source #

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

Example

Expand
>>> :kind! Eval (Or '[ 'True, 'True])
Eval (Or '[ 'True, 'True]) :: Bool
= 'True
>>> :kind! Eval (Or '[ 'False, 'False])
Eval (Or '[ 'False, 'False]) :: Bool
= 'False
Instances
type Eval (Or lst :: Bool -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

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

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

Type-level Any.

Example

Expand
>>> :kind! Eval (Any (Flip (<) 5) '[0,1,2,3,4,5])
Eval (Any (Flip (<) 5) '[0,1,2,3,4,5]) :: Bool
= 'True
>>> :kind! Eval (Any (Flip (<) 0) '[0,1,2,3,4,5])
Eval (Any (Flip (<) 0) '[0,1,2,3,4,5]) :: Bool
= 'False
Instances
type Eval (Any p lst :: Bool -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (Any p lst :: Bool -> Type) = Eval (Or =<< Map p lst)

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

Snoc for type-level lists.

Example

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

Defined in Fcf.Alg.List

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

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

ToList for type-level lists.

Example

Expand
>>> :kind! Eval (ToList 1)
Eval (ToList 1) :: [Nat]
= '[1]
Instances
type Eval (ToList a :: [k] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (ToList a :: [k] -> Type) = a ': ([] :: [k])

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

Equal tests for list equality. We may change the name to (==).

Example

Expand
>>> :kind! Eval (Equal '[1,2,3] '[1,2,3])
Eval (Equal '[1,2,3] '[1,2,3]) :: Bool
= 'True
>>> :kind! Eval (Equal '[1,2,3] '[1,3,2])
Eval (Equal '[1,2,3] '[1,3,2]) :: Bool
= 'False
Instances
type Eval (Equal as bs :: Bool -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (Equal as bs :: Bool -> Type) = Eval (And =<< ZipWith (TyEq :: b -> b -> Bool -> Type) as bs)