Safe Haskell	Safe-Inferred
Language	Haskell2010

Fcf

Contents

First-class type families
- Functional combinators
Operations on common types
Overloaded operations
Miscellaneous

Description

First-class type families

For example, here is a regular type family:

type family   FromMaybe (a :: k) (m :: Maybe k) :: k
type instance FromMaybe a 'Nothing  = a
type instance FromMaybe a ('Just b) = b

With Fcf, it translates to a data declaration:

data FromMaybe :: k -> Maybe k -> Exp k
type instance Eval (FromMaybe a 'Nothing)  = a
type instance Eval (FromMaybe a ('Just b)) = b

Fcfs can be higher-order.
The kind constructor Exp is a monad: there's (=<<) and Pure.

Essential language extensions for Fcf:

{-# LANGUAGE
    DataKinds,
    PolyKinds,
    TypeFamilies,
    TypeOperators,
    UndecidableInstances #-}

Synopsis

type Exp a = a -> Type
type family Eval (e :: Exp a) :: a
type (@@) (f :: k1 -> Exp k) (x :: k1) = Eval (f x)
data Pure (b :: a) (c :: a)
data Pure1 (c :: a -> b) (d :: a) (e :: b)
data Pure2 (d :: a -> b -> c) (e :: a) (f :: b) (g :: c)
data Pure3 (e :: a -> b -> c -> d) (f :: a) (g :: b) (h :: c) (i :: d)
data Pure4 (f :: a -> b -> c -> d -> e) (g :: a) (h :: b) (i :: c) (j :: d) (k :: e)
data Pure5 (g :: a -> b -> c -> d -> e -> f) (h :: a) (i :: b) (j :: c) (k :: d) (l :: e) (m :: f)
data Pure6 (h :: a -> b -> c -> d -> e -> f -> g) (i :: a) (j :: b) (k :: c) (l :: d) (m :: e) (n :: f) (o :: g)
data Pure7 (i :: a -> b -> c -> d -> e -> f -> g -> h) (j :: a) (k :: b) (l :: c) (m :: d) (n :: e) (o :: f) (p :: g) (q :: h)
data Pure8 (j :: a -> b -> c -> d -> e -> f -> g -> h -> i) (k :: a) (l :: b) (m :: c) (n :: d) (o :: e) (p :: f) (q :: g) (r :: h) (s :: i)
data Pure9 (k :: a -> b -> c -> d -> e -> f -> g -> h -> i -> j) (l :: a) (m :: b) (n :: c) (o :: d) (p :: e) (q :: f) (r :: g) (s :: h) (t :: i) (u :: j)
data ((c :: a -> Exp b) =<< (d :: Exp a)) (e :: b)
data ((c :: Exp a) >>= (d :: a -> Exp b)) (e :: b)
data ((d :: b -> Exp c) <=< (e :: a -> Exp b)) (f :: a) (g :: c)
type LiftM = (=<<) :: (a -> Exp b) -> Exp a -> b -> Type
data LiftM2 (d :: a -> b -> Exp c) (e :: Exp a) (f :: Exp b) (g :: c)
data LiftM3 (e :: a -> b -> c -> Exp d) (f :: Exp a) (g :: Exp b) (h :: Exp c) (i :: d)
data Join (b :: Exp (Exp a)) (c :: a)
data ((c :: a -> b) <$> (d :: Exp a)) (e :: b)
data ((c :: Exp (a -> b)) <*> (d :: Exp a)) (e :: b)
data Flip (d :: a -> b -> Exp c) (e :: b) (f :: a) (g :: c)
data ConstFn (c :: a) (d :: b) (e :: a)
data ((c :: a -> Exp b) $ (d :: a)) (e :: b)
data Uncurry (d :: a -> b -> Exp c) (e :: (a, b)) (f :: c)
data Fst (c :: (a, b)) (d :: a)
data Snd (c :: (a, b)) (d :: b)
data ((a :: b -> Exp c) *** (d :: b' -> Exp c')) (e :: (b, b')) (f :: (c, c'))
data UnEither (d :: a -> Exp c) (e :: b -> Exp c) (f :: Either a b) (g :: c)
data IsLeft (c :: Either a b) (d :: Bool)
data IsRight (c :: Either a b) (d :: Bool)
data UnMaybe (c :: Exp b) (d :: a -> Exp b) (e :: Maybe a) (f :: b)
data FromMaybe (a :: k) (b :: Maybe k) (c :: k)
data IsNothing (b :: Maybe a) (c :: Bool)
data IsJust (b :: Maybe a) (c :: Bool)
data ((b :: [a]) ++ (c :: [a])) (d :: [a])
data Head (b :: [a]) (c :: Maybe a)
data Last (b :: [a]) (c :: Maybe a)
data Tail (b :: [a]) (c :: Maybe [a])
data Cons (b :: a) (c :: [a]) (d :: [a])
data Snoc (b :: [a]) (c :: a) (d :: [a])
data Cons2 (c :: (a, b)) (d :: ([a], [b])) (e :: ([a], [b]))
data Init (b :: [a]) (c :: Maybe [a])
data Uncons (b :: [a]) (c :: Maybe (a, [a]))
data Unsnoc (b :: [a]) (c :: Maybe ([a], a))
data Singleton (b :: a) (c :: [a])
data Null (b :: [a]) (c :: Bool)
data Length (b :: [a]) (c :: Nat)
data Reverse (b :: [a]) (c :: [a])
data Intersperse (b :: a) (c :: [a]) (d :: [a])
data Intercalate (b :: [a]) (c :: [[a]]) (d :: [a])
data Foldr (c :: a -> b -> Exp b) (d :: b) (e :: t a) (f :: b)
data UnList (c :: b) (d :: a -> b -> Exp b) (e :: [a]) (f :: b)
data Concat (a :: t m) (b :: m)
data ConcatMap (c :: a -> Exp [b]) (d :: t a) (e :: [b])
data Unfoldr (c :: b -> Exp (Maybe (a, b))) (d :: b) (e :: [a])
data Replicate (b :: Nat) (c :: a) (d :: [a])
data Take (b :: Nat) (c :: [a]) (d :: [a])
data Drop (b :: Nat) (c :: [a]) (d :: [a])
data SplitAt (b :: Nat) (c :: [a]) (d :: ([a], [a]))
data TakeWhile (b :: a -> Exp Bool) (c :: [a]) (d :: [a])
data DropWhile (b :: a -> Exp Bool) (c :: [a]) (d :: [a])
data Span (b :: a -> Exp Bool) (c :: [a]) (d :: ([a], [a]))
data Break (b :: a -> Exp Bool) (c :: [a]) (d :: ([a], [a]))
data Tails (b :: [a]) (c :: [[a]])
data IsPrefixOf (b :: [a]) (c :: [a]) (d :: Bool)
data IsSuffixOf (b :: [a]) (c :: [a]) (d :: Bool)
data IsInfixOf (b :: [a]) (c :: [a]) (d :: Bool)
data Elem (b :: a) (c :: [a]) (d :: Bool)
data Lookup (a :: k) (c :: [(k, b)]) (d :: Maybe b)
data Find (b :: a -> Exp Bool) (c :: [a]) (d :: Maybe a)
data Filter (b :: a -> Exp Bool) (c :: [a]) (d :: [a])
data Partition (b :: a -> Exp Bool) (c :: [a]) (d :: ([a], [a]))
data FindIndex (b :: a -> Exp Bool) (c :: [a]) (d :: Maybe Nat)
data SetIndex (b :: Nat) (c :: a) (d :: [a]) (e :: [a])
data ZipWith (d :: a -> b -> Exp c) (e :: [a]) (f :: [b]) (g :: [c])
data Zip (c :: [a]) (d :: [b]) (e :: [(a, b)])
data Unzip (c :: Exp [(a, b)]) (d :: ([a], [b]))
data UnBool (b :: Exp a) (c :: Exp a) (d :: Bool) (e :: a)
data ((a :: Bool) || (b :: Bool)) (c :: Bool)
data ((a :: Bool) && (b :: Bool)) (c :: Bool)
data Not (a :: Bool) (b :: Bool)
data Case (a :: [Match j k]) (b :: j) (c :: k)
data Match j k
type (-->) = 'Match_ :: j -> k -> Match j k
type Is = 'Is_ :: (j -> Exp Bool) -> k -> Match j k
type Any = 'Any_ :: k -> Match j k
type Else = 'Else_ :: (j -> Exp k) -> Match j k
data ((a :: Nat) + (b :: Nat)) (c :: Nat)
data ((a :: Nat) - (b :: Nat)) (c :: Nat)
data ((a :: Nat) * (b :: Nat)) (c :: Nat)
data ((a :: Nat) ^ (b :: Nat)) (c :: Nat)
data ((a :: Nat) <= (b :: Nat)) (c :: Bool)
data ((a :: Nat) >= (b :: Nat)) (c :: Bool)
data ((a :: Nat) < (b :: Nat)) (c :: Bool)
data ((a :: Nat) > (b :: Nat)) (c :: Bool)
data Map (c :: a -> Exp b) (d :: f a) (e :: f b)
data Bimap (c :: a -> Exp a') (d :: b -> Exp b') (e :: f a b) (g :: f a' b')
data Error (b :: Symbol) (c :: a)
data Constraints (a :: [Constraint]) b
data TyEq (c :: a) (d :: b) (e :: Bool)
type family Stuck :: a
class IsBool (b :: Bool) where
- _If :: (b ~ 'True => r) -> (b ~ 'False => r) -> r
type family If (cond :: Bool) (tru :: k) (fls :: k) :: k where ...
data Assert (a :: ErrorMessage) (b :: Exp Bool) (c :: r) (d :: r)
data AssertNot (a :: ErrorMessage) (b :: Exp Bool) (c :: r) (d :: r)

First-class type families

type Exp a = a -> Type Source #

Kind of type-level expressions indexed by their result type.

type family Eval (e :: Exp a) :: a Source #

Expression evaluator.

Instances

Instances details

type Eval (Not 'False) Source #
Instance details Defined in Fcf.Data.Bool type Eval (Not 'False) = 'True
type Eval (Not 'True) Source #
Instance details Defined in Fcf.Data.Bool type Eval (Not 'True) = 'False
type Eval (Constraints (a ': as) :: Constraint -> Type) Source #
Instance details Defined in Fcf.Utils type Eval (Constraints (a ': as) :: Constraint -> Type) = (a, Eval (Constraints as))
type Eval (Constraints ('[] :: [Constraint])) Source #
Instance details Defined in Fcf.Utils type Eval (Constraints ('[] :: [Constraint])) = ()
type Eval (MEmpty_ :: a -> Type) Source #
Instance details Defined in Fcf.Class.Monoid type Eval (MEmpty_ :: a -> Type) = MEmpty :: a
type Eval (Sum ns :: Nat -> Type) Source #
Instance details Defined in Fcf.Class.Foldable type Eval (Sum ns :: Nat -> Type) = Eval (Foldr (+) 0 ns)
type Eval (Length ('[] :: [a]) :: Nat -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Length ('[] :: [a]) :: Nat -> Type) = 0
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 (a * b :: Nat -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a * b :: Nat -> Type) = a * b
type Eval (a + b :: Nat -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a + b :: Nat -> Type) = a + b
type Eval (a - b :: Nat -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a - b :: Nat -> Type) = a - b
type Eval (a ^ b :: Nat -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a ^ b :: Nat -> Type) = a ^ b
type Eval (And lst :: Bool -> Type) Source #
Instance details Defined in Fcf.Class.Foldable type Eval (And lst :: Bool -> Type) = Eval (Foldr (&&) 'True lst)
type Eval (Or lst :: Bool -> Type) Source #
Instance details Defined in Fcf.Class.Foldable type Eval (Or lst :: Bool -> Type) = Eval (Foldr (\|\|) 'False lst)
type Eval ('False && b :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval ('False && b :: Bool -> Type) = 'False
type Eval ('True && b :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval ('True && b :: Bool -> Type) = b
type Eval (a && 'False :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval (a && 'False :: Bool -> Type) = 'False
type Eval (a && 'True :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval (a && 'True :: Bool -> Type) = a
type Eval ('False \|\| b :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval ('False \|\| b :: Bool -> Type) = b
type Eval ('True \|\| b :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval ('True \|\| b :: Bool -> Type) = 'True
type Eval (a \|\| 'False :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval (a \|\| 'False :: Bool -> Type) = a
type Eval (a \|\| 'True :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval (a \|\| 'True :: Bool -> Type) = 'True
type Eval (IsJust ('Just _a) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (IsJust ('Just _a) :: Bool -> Type) = 'True
type Eval (IsJust ('Nothing :: Maybe a) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (IsJust ('Nothing :: Maybe a) :: Bool -> Type) = 'False
type Eval (IsNothing ('Just _a) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (IsNothing ('Just _a) :: Bool -> Type) = 'False
type Eval (IsNothing ('Nothing :: Maybe a) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (IsNothing ('Nothing :: Maybe a) :: Bool -> Type) = 'True
type Eval (Null ('[] :: [a]) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Null ('[] :: [a]) :: Bool -> Type) = 'True
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 (a < b :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a < b :: Bool -> Type) = Eval (Not =<< (a >= b))
type Eval (a <= b :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a <= b :: Bool -> Type) = a <=? b
type Eval (a > b :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a > b :: Bool -> Type) = Eval (Not =<< (a <= b))
type Eval (a >= b :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a >= b :: Bool -> Type) = b <=? a
type Eval (Join e :: a -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Join e :: a -> Type) = Eval (Eval e)
type Eval (Pure x :: a -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Pure x :: a -> Type) = x
type Eval (Error msg :: a -> Type) Source #
Instance details Defined in Fcf.Utils type Eval (Error msg :: a -> Type) = TypeError ('Text msg) :: a
type Eval (TError msg :: a -> Type) Source #
Instance details Defined in Fcf.Utils type Eval (TError msg :: a -> Type) = TypeError msg :: a
type Eval (Compare ('Left _a :: Either a b) ('Right _b :: Either a b) :: Ordering -> Type) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare ('Left _a :: Either a b) ('Right _b :: Either a b) :: Ordering -> Type) = 'LT
type Eval (Compare ('Right _a :: Either a b) ('Left _b :: Either a b) :: Ordering -> Type) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare ('Right _a :: Either a b) ('Left _b :: Either a b) :: Ordering -> Type) = 'GT
type Eval (Compare ('Left a2 :: Either a1 b1) ('Left b2 :: Either a1 b1) :: Ordering -> Type) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare ('Left a2 :: Either a1 b1) ('Left b2 :: Either a1 b1) :: Ordering -> Type) = Eval (Compare a2 b2)
type Eval (Compare ('Right a3 :: Either a2 a1) ('Right b :: Either a2 a1) :: Ordering -> Type) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare ('Right a3 :: Either a2 a1) ('Right b :: Either a2 a1) :: Ordering -> Type) = Eval (Compare a3 b)
type Eval (Compare 'EQ 'GT) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare 'EQ 'GT) = 'LT
type Eval (Compare 'EQ 'LT) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare 'EQ 'LT) = 'GT
type Eval (Compare 'GT 'EQ) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare 'GT 'EQ) = 'GT
type Eval (Compare 'GT 'LT) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare 'GT 'LT) = 'GT
type Eval (Compare 'LT 'EQ) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare 'LT 'EQ) = 'LT
type Eval (Compare 'LT 'GT) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare 'LT 'GT) = 'LT
type Eval (Compare a a :: Ordering -> Type) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare a a :: Ordering -> Type) = 'EQ
type Eval (Compare ('Just _a) ('Nothing :: Maybe a) :: Ordering -> Type) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare ('Just _a) ('Nothing :: Maybe a) :: Ordering -> Type) = 'GT
type Eval (Compare ('Nothing :: Maybe a) ('Just _b) :: Ordering -> Type) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare ('Nothing :: Maybe a) ('Just _b) :: Ordering -> Type) = 'LT
type Eval (Compare ('Nothing :: Maybe a) ('Nothing :: Maybe a) :: Ordering -> Type) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare ('Nothing :: Maybe a) ('Nothing :: Maybe a) :: Ordering -> Type) = 'EQ
type Eval (Compare ('Just a2) ('Just b) :: Ordering -> Type) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare ('Just a2) ('Just b) :: Ordering -> Type) = Eval (Compare a2 b)
type Eval (Compare a b :: Ordering -> Type) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare a b :: Ordering -> Type) = CmpNat a b
type Eval (Compare '(a3, a4) '(b1, b2) :: Ordering -> Type) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare '(a3, a4) '(b1, b2) :: Ordering -> Type) = Eval (Compare a3 b1) <> Eval (Compare a4 b2)
type Eval (Compare '(a4, a5, a6) '(b1, b2, b3) :: Ordering -> Type) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare '(a4, a5, a6) '(b1, b2, b3) :: Ordering -> Type) = (Eval (Compare a4 b1) <> Eval (Compare a5 b2)) <> Eval (Compare a6 b3)
type Eval (Compare a b :: Ordering -> Type) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare a b :: Ordering -> Type) = 'EQ
type Eval (Compare 'False 'True) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare 'False 'True) = 'GT
type Eval (Compare 'True 'False) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare 'True 'False) = 'GT
type Eval (Compare a a :: Ordering -> Type) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare a a :: Ordering -> Type) = 'EQ
type Eval (Compare (_x ': _xs) ('[] :: [a]) :: Ordering -> Type) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare (_x ': _xs) ('[] :: [a]) :: Ordering -> Type) = 'GT
type Eval (Compare (x ': xs) (y ': ys) :: Ordering -> Type) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare (x ': xs) (y ': ys) :: Ordering -> Type) = Eval (Compare x y) <> Eval (Compare xs ys)
type Eval (Compare ('[] :: [a]) (_y ': _ys) :: Ordering -> Type) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare ('[] :: [a]) (_y ': _ys) :: Ordering -> Type) = 'LT
type Eval (Compare ('[] :: [a]) ('[] :: [a]) :: Ordering -> Type) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare ('[] :: [a]) ('[] :: [a]) :: Ordering -> Type) = 'EQ
type Eval (Compare a b :: Ordering -> Type) Source #
Instance details Defined in Fcf.Class.Ord type Eval (Compare a b :: Ordering -> Type) = CmpSymbol a b
type Eval (a2 < b :: Bool -> Type) Source #
Instance details Defined in Fcf.Class.Ord type Eval (a2 < b :: Bool -> Type)
type Eval (a2 <= b :: Bool -> Type) Source #
Instance details Defined in Fcf.Class.Ord type Eval (a2 <= b :: Bool -> Type)
type Eval (a2 > b :: Bool -> Type) Source #
Instance details Defined in Fcf.Class.Ord type Eval (a2 > b :: Bool -> Type)
type Eval (a2 >= b :: Bool -> Type) Source #
Instance details Defined in Fcf.Class.Ord type Eval (a2 >= b :: Bool -> Type)
type Eval (IsLeft ('Left _a :: Either a b) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (IsLeft ('Left _a :: Either a b) :: Bool -> Type) = 'True
type Eval (IsLeft ('Right _a :: Either a b) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (IsLeft ('Right _a :: Either a b) :: Bool -> Type) = 'False
type Eval (IsRight ('Left _a :: Either a b) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (IsRight ('Left _a :: Either a b) :: Bool -> Type) = 'False
type Eval (IsRight ('Right _a :: Either a b) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (IsRight ('Right _a :: Either a b) :: Bool -> Type) = 'True
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)
type Eval (IsInfixOf xs ys :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (IsInfixOf xs ys :: Bool -> Type) = Eval ((Any (IsPrefixOf xs) :: [[a]] -> Bool -> Type) =<< Tails ys)
type Eval (IsPrefixOf xs ys :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (IsPrefixOf xs ys :: Bool -> Type)
type Eval (IsSuffixOf xs ys :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (IsSuffixOf xs ys :: Bool -> Type) = Eval (IsPrefixOf ((Reverse :: [a] -> [a] -> Type) @@ xs) ((Reverse :: [a] -> [a] -> Type) @@ ys))
type Eval (Concat xs :: a -> Type) Source #
Instance details Defined in Fcf.Class.Foldable type Eval (Concat xs :: a -> Type) = Eval (FoldMap (Pure :: a -> a -> Type) xs)
type Eval (x .<> y :: a -> Type) Source #
Instance details Defined in Fcf.Class.Monoid type Eval (x .<> y :: a -> Type) = x <> y
type Eval (FromMaybe _a ('Just b) :: a -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (FromMaybe _a ('Just b) :: a -> Type) = b
type Eval (FromMaybe a2 ('Nothing :: Maybe a1) :: a1 -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (FromMaybe a2 ('Nothing :: Maybe a1) :: a1 -> Type) = a2
type Eval (Fst '(a2, _b) :: a1 -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (Fst '(a2, _b) :: a1 -> Type) = a2
type Eval (Snd '(_a, b) :: a2 -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (Snd '(_a, b) :: a2 -> Type) = b
type Eval (All p lst :: Bool -> Type) Source #
Instance details Defined in Fcf.Class.Foldable type Eval (All p lst :: Bool -> Type) = Eval (Foldr (Bicomap p (Pure :: Bool -> Bool -> Type) (&&)) 'True lst)
type Eval (Any p lst :: Bool -> Type) Source #
Instance details Defined in Fcf.Class.Foldable type Eval (Any p lst :: Bool -> Type) = Eval (Foldr (Bicomap p (Pure :: Bool -> Bool -> Type) (\|\|)) 'False lst)
type Eval (TyEq a b :: Bool -> Type) Source #
Instance details Defined in Fcf.Utils type Eval (TyEq a b :: Bool -> Type)
type Eval (UnBool fal tru 'False :: a -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval (UnBool fal tru 'False :: a -> Type) = Eval fal
type Eval (UnBool fal tru 'True :: a -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval (UnBool fal tru 'True :: a -> Type) = Eval tru
type Eval (Assert msg mcond k :: a -> Type) Source #
Instance details Defined in Fcf.Utils type Eval (Assert msg mcond k :: a -> Type) = Eval (If (Eval mcond) (Pure k) (TError msg :: a -> Type))
type Eval (AssertNot err mcond k :: a -> Type) Source #
Instance details Defined in Fcf.Utils type Eval (AssertNot err mcond k :: a -> Type) = Eval (Assert err (Not =<< mcond) k)
type Eval (ConstFn a2 _b :: a1 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (ConstFn a2 _b :: a1 -> Type) = a2
type Eval (f $ a3 :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (f $ a3 :: a2 -> Type) = Eval (f a3)
type Eval (f <$> e :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (f <$> e :: a2 -> Type) = f (Eval e)
type Eval (f <*> e :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (f <*> e :: a2 -> Type) = Eval f (Eval e)
type Eval (k =<< e :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (k =<< e :: a2 -> Type) = Eval (k (Eval e))
type Eval (e >>= k :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (e >>= k :: a2 -> Type) = Eval (k (Eval e))
type Eval (Pure1 f x :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Pure1 f x :: a2 -> Type) = f x
type Eval (x & f :: a2 -> Type) Source #
Instance details Defined in Fcf.Data.Function type Eval (x & f :: a2 -> Type) = Eval (f x)
type Eval (Case ms a :: k -> Type) Source #
Instance details Defined in Fcf.Utils type Eval (Case ms a :: k -> Type)
type Eval (UnMaybe y f ('Just x) :: a1 -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (UnMaybe y f ('Just x) :: a1 -> Type) = Eval (f x)
type Eval (UnMaybe y f ('Nothing :: Maybe a2) :: a1 -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (UnMaybe y f ('Nothing :: Maybe a2) :: a1 -> Type) = Eval y
type Eval (UnList y f xs :: a1 -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (UnList y f xs :: a1 -> Type) = Eval (Foldr f y xs)
type Eval (FoldMap f ('Left _a :: Either a3 a1) :: a2 -> Type) Source #
Instance details Defined in Fcf.Class.Foldable type Eval (FoldMap f ('Left _a :: Either a3 a1) :: a2 -> Type) = MEmpty :: a2
type Eval (FoldMap f ('Right x :: Either a3 a1) :: a2 -> Type) Source #
Instance details Defined in Fcf.Class.Foldable type Eval (FoldMap f ('Right x :: Either a3 a1) :: a2 -> Type) = Eval (f x)
type Eval (FoldMap f ('Just x) :: a2 -> Type) Source #
Instance details Defined in Fcf.Class.Foldable type Eval (FoldMap f ('Just x) :: a2 -> Type) = Eval (f x)
type Eval (FoldMap f ('Nothing :: Maybe a1) :: a2 -> Type) Source #
Instance details Defined in Fcf.Class.Foldable type Eval (FoldMap f ('Nothing :: Maybe a1) :: a2 -> Type) = MEmpty :: a2
type Eval (FoldMap f (x ': xs) :: a2 -> Type) Source #
Instance details Defined in Fcf.Class.Foldable type Eval (FoldMap f (x ': xs) :: a2 -> Type) = Eval (f x) <> Eval (FoldMap f xs)
type Eval (FoldMap f ('[] :: [a1]) :: a2 -> Type) Source #
Instance details Defined in Fcf.Class.Foldable type Eval (FoldMap f ('[] :: [a1]) :: a2 -> Type) = MEmpty :: a2
type Eval (Uncurry f '(x, y) :: a2 -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (Uncurry f '(x, y) :: a2 -> Type) = Eval (f x y)
type Eval (Foldr f y ('Left _a :: Either a3 a1) :: a2 -> Type) Source #
Instance details Defined in Fcf.Class.Foldable type Eval (Foldr f y ('Left _a :: Either a3 a1) :: a2 -> Type) = y
type Eval (Foldr f y ('Right x :: Either a3 a1) :: a2 -> Type) Source #
Instance details Defined in Fcf.Class.Foldable type Eval (Foldr f y ('Right x :: Either a3 a1) :: a2 -> Type) = Eval (f x y)
type Eval (Foldr f y ('Just x) :: a2 -> Type) Source #
Instance details Defined in Fcf.Class.Foldable type Eval (Foldr f y ('Just x) :: a2 -> Type) = Eval (f x y)
type Eval (Foldr f y ('Nothing :: Maybe a1) :: a2 -> Type) Source #
Instance details Defined in Fcf.Class.Foldable type Eval (Foldr f y ('Nothing :: Maybe a1) :: a2 -> Type) = y
type Eval (Foldr f y (x ': xs) :: a2 -> Type) Source #
Instance details Defined in Fcf.Class.Foldable 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.Class.Foldable type Eval (Foldr f y ('[] :: [a1]) :: a2 -> Type) = y
type Eval ((f <=< g) x :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval ((f <=< g) x :: a2 -> Type) = Eval (f (Eval (g x)))
type Eval (Flip f y x :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Flip f y x :: a2 -> Type) = Eval (f x y)
type Eval (Pure2 f x y :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Pure2 f x y :: a2 -> Type) = f x y
type Eval (UnEither f g ('Left x :: Either a1 b) :: a2 -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (UnEither f g ('Left x :: Either a1 b) :: a2 -> Type) = Eval (f x)
type Eval (UnEither f g ('Right y :: Either a1 b) :: a2 -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (UnEither f g ('Right y :: Either a1 b) :: a2 -> Type) = Eval (g y)
type Eval (LiftM2 f x y :: a3 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (LiftM2 f x y :: a3 -> Type) = Eval (f (Eval x) (Eval y))
type Eval (On r f x y :: a2 -> Type) Source #
Instance details Defined in Fcf.Data.Function type Eval (On r f x y :: a2 -> Type) = Eval (r (Eval (f x)) (Eval (f y)))
type Eval (Pure3 f x y z :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Pure3 f x y z :: a2 -> Type) = f x y z
type Eval (LiftM3 f x y z :: a4 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (LiftM3 f x y z :: a4 -> Type) = Eval (f (Eval x) (Eval y) (Eval z))
type Eval (Pure4 f w x y z :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Pure4 f w x y z :: a2 -> Type) = f w x y z
type Eval (Bicomap f g r x y :: a4 -> Type) Source #
Instance details Defined in Fcf.Data.Function type Eval (Bicomap f g r x y :: a4 -> Type) = Eval (r (Eval (f x)) (Eval (g y)))
type Eval (Pure5 f v w x y z :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Pure5 f v w x y z :: a2 -> Type) = f v w x y z
type Eval (Pure6 f2 u v w x y z :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Pure6 f2 u v w x y z :: a2 -> Type) = f2 u v w x y z
type Eval (Pure7 f2 t u v w x y z :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Pure7 f2 t u v w x y z :: a2 -> Type) = f2 t u v w x y z
type Eval (Pure8 f2 s t u v w x y z :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Pure8 f2 s t u v w x y z :: a2 -> Type) = f2 s t u v w x y z
type Eval (Pure9 f2 r s t u v w x y z :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Pure9 f2 r s t u v w x y z :: a2 -> Type) = f2 r s t u v w x y z
type Eval (Unsnoc (x ': (y ': ys)) :: Maybe ([a], a) -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Unsnoc (x ': (y ': ys)) :: Maybe ([a], a) -> Type)
type Eval (Unsnoc ('[] :: [a]) :: Maybe ([a], a) -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Unsnoc ('[] :: [a]) :: Maybe ([a], a) -> Type) = 'Nothing :: Maybe ([a], a)
type Eval (Unsnoc '[x] :: Maybe ([k], k) -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Unsnoc '[x] :: Maybe ([k], k) -> Type) = 'Just '('[] :: [k], x)
type Eval (Uncons ('[] :: [a]) :: Maybe (a, [a]) -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Uncons ('[] :: [a]) :: Maybe (a, [a]) -> Type) = 'Nothing :: Maybe (a, [a])
type Eval (Uncons (a ': xs) :: Maybe (k, [k]) -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Uncons (a ': xs) :: Maybe (k, [k]) -> Type) = 'Just '(a, xs)
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]
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]
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] :: Maybe [a1] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Init '[a2] :: Maybe [a1] -> Type) = 'Just ('[] :: [a1])
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
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
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 (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] :: Maybe a1 -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Last '[a2] :: Maybe a1 -> Type) = 'Just a2
type Eval (Tails ('[] :: [a]) :: [[a]] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Tails ('[] :: [a]) :: [[a]] -> Type) = '[] :: [[a]]
type Eval (Tails (a2 ': as) :: [[a1]] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Tails (a2 ': as) :: [[a1]] -> Type) = (a2 ': as) ': Eval (Tails as)
type Eval (Reverse l :: [a] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Reverse l :: [a] -> Type)
type Eval (Singleton x :: [k] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Singleton x :: [k] -> Type) = '[x]
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 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 (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
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 (xs ++ ys :: [a] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (xs ++ ys :: [a] -> Type) = xs <> ys
type Eval (Drop n as :: [a] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Drop n as :: [a] -> Type)
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]
type Eval (Filter _p ('[] :: [a]) :: [a] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Filter _p ('[] :: [a]) :: [a] -> Type) = '[] :: [a]
type Eval (Intercalate xs xss :: [a] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Intercalate xs xss :: [a] -> Type) = Eval ((Concat :: [[a]] -> [a] -> Type) =<< Intersperse xs xss)
type Eval (Intersperse _1 ('[] :: [a]) :: [a] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Intersperse _1 ('[] :: [a]) :: [a] -> Type) = '[] :: [a]
type Eval (Intersperse sep (x ': xs) :: [a] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Intersperse sep (x ': xs) :: [a] -> Type)
type Eval (Take n as :: [a] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Take n as :: [a] -> Type)
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]
type Eval (Cons a2 as :: [a1] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Cons a2 as :: [a1] -> Type) = a2 ': as
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 (Replicate n a2 :: [a1] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Replicate n a2 :: [a1] -> Type)
type Eval (Snoc lst a :: [k] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Snoc lst a :: [k] -> Type) = Eval (lst ++ '[a])
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)))
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)
type Eval (Unfoldr f c :: [a] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Unfoldr f c :: [a] -> Type)
type Eval (SetIndex n a' as :: [k] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (SetIndex n a' as :: [k] -> Type)
type Eval (Map f ('Just a3) :: Maybe a2 -> Type) Source #
Instance details Defined in Fcf.Class.Functor type Eval (Map f ('Just a3) :: Maybe a2 -> Type) = 'Just (Eval (f a3))
type Eval (Map f ('Nothing :: Maybe a) :: Maybe b -> Type) Source #
Instance details Defined in Fcf.Class.Functor type Eval (Map f ('Nothing :: Maybe a) :: Maybe b -> Type) = 'Nothing :: Maybe b
type Eval (ConcatMap f xs :: [b] -> Type) Source #
Instance details Defined in Fcf.Class.Foldable type Eval (ConcatMap f xs :: [b] -> Type) = Eval (FoldMap f xs)
type Eval (Map f ('[] :: [a]) :: [b] -> Type) Source #
Instance details Defined in Fcf.Class.Functor type Eval (Map f ('[] :: [a]) :: [b] -> Type) = '[] :: [b]
type Eval (Map f (a2 ': as) :: [b] -> Type) Source #
Instance details Defined in Fcf.Class.Functor type Eval (Map f (a2 ': as) :: [b] -> Type) = Eval (f a2) ': Eval (Map f as)
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 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 (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 (Break p lst :: ([a], [a]) -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Break p lst :: ([a], [a]) -> Type) = Eval (Span (Not <=< p) lst)
type Eval (Partition p lst :: ([a], [a]) -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Partition p lst :: ([a], [a]) -> Type)
type Eval (Span p lst :: ([a], [a]) -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Span p lst :: ([a], [a]) -> Type) = '(Eval (TakeWhile p lst), Eval (DropWhile p lst))
type Eval (SplitAt n xs :: ([a], [a]) -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (SplitAt n xs :: ([a], [a]) -> Type) = '(Eval (Take n xs), Eval (Drop n xs))
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))
type Eval (Cons2 '(a3, b) '(as, bs) :: ([a1], [a2]) -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Cons2 '(a3, b) '(as, bs) :: ([a1], [a2]) -> Type) = '(a3 ': as, b ': bs)
type Eval (Map f ('Left x :: Either a2 a1) :: Either a2 b -> Type) Source #
Instance details Defined in Fcf.Class.Functor type Eval (Map f ('Left x :: Either a2 a1) :: Either a2 b -> Type) = 'Left x :: Either a2 b
type Eval (Map f ('Right a3 :: Either a2 a1) :: Either a2 b -> Type) Source #
Instance details Defined in Fcf.Class.Functor type Eval (Map f ('Right a3 :: Either a2 a1) :: Either a2 b -> Type) = 'Right (Eval (f a3)) :: Either a2 b
type Eval (Map f '(x, a2) :: (k2, k1) -> Type) Source #
Instance details Defined in Fcf.Class.Functor type Eval (Map f '(x, a2) :: (k2, k1) -> Type) = '(x, Eval (f a2))
type Eval ((f *** f') '(b2, b'2) :: (k1, k2) -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval ((f *** f') '(b2, b'2) :: (k1, k2) -> Type) = '(Eval (f b2), Eval (f' b'2))
type Eval (Second g x :: f a' b' -> Type) Source #
Instance details Defined in Fcf.Class.Bifunctor type Eval (Second g x :: f a' b' -> Type) = Eval (Bimap (Pure :: a' -> a' -> Type) g x)
type Eval (First f2 x :: f1 a' b' -> Type) Source #
Instance details Defined in Fcf.Class.Bifunctor type Eval (First f2 x :: f1 a' b' -> Type) = Eval (Bimap f2 (Pure :: b' -> b' -> Type) x)
type Eval (Bimap f g ('Right y :: Either a b1) :: Either a' b2 -> Type) Source #
Instance details Defined in Fcf.Class.Bifunctor type Eval (Bimap f g ('Right y :: Either a b1) :: Either a' b2 -> Type) = 'Right (Eval (g y)) :: Either a' b2
type Eval (Bimap f g ('Left x :: Either a1 b) :: Either a2 b' -> Type) Source #
Instance details Defined in Fcf.Class.Bifunctor type Eval (Bimap f g ('Left x :: Either a1 b) :: Either a2 b' -> Type) = 'Left (Eval (f x)) :: Either a2 b'
type Eval (Bimap f g '(x, y) :: (k1, k2) -> Type) Source #
Instance details Defined in Fcf.Class.Bifunctor type Eval (Bimap f g '(x, y) :: (k1, k2) -> Type) = '(Eval (f x), Eval (g y))
type Eval (Map f '(x, y, a2) :: (k2, k3, k1) -> Type) Source #
Instance details Defined in Fcf.Class.Functor type Eval (Map f '(x, y, a2) :: (k2, k3, k1) -> Type) = '(x, y, Eval (f a2))
type Eval (Map f '(x, y, z, a2) :: (k2, k3, k4, k1) -> Type) Source #
Instance details Defined in Fcf.Class.Functor type Eval (Map f '(x, y, z, a2) :: (k2, k3, k4, k1) -> Type) = '(x, y, z, Eval (f a2))
type Eval (Map f '(x, y, z, w, a2) :: (k2, k3, k4, k5, k1) -> Type) Source #
Instance details Defined in Fcf.Class.Functor type Eval (Map f '(x, y, z, w, a2) :: (k2, k3, k4, k5, k1) -> Type) = '(x, y, z, w, Eval (f a2))

type (@@) (f :: k1 -> Exp k) (x :: k1) = Eval (f x) Source #

Apply and evaluate a unary type function.

Functional combinators

data Pure (b :: a) (c :: a) Source #

Instances

Instances details

type Eval (Pure x :: a -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Pure x :: a -> Type) = x

data Pure1 (c :: a -> b) (d :: a) (e :: b) Source #

Instances

Instances details

type Eval (Pure1 f x :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Pure1 f x :: a2 -> Type) = f x

data Pure2 (d :: a -> b -> c) (e :: a) (f :: b) (g :: c) Source #

Instances

Instances details

type Eval (Pure2 f x y :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Pure2 f x y :: a2 -> Type) = f x y

data Pure3 (e :: a -> b -> c -> d) (f :: a) (g :: b) (h :: c) (i :: d) Source #

Instances

Instances details

type Eval (Pure3 f x y z :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Pure3 f x y z :: a2 -> Type) = f x y z

data Pure4 (f :: a -> b -> c -> d -> e) (g :: a) (h :: b) (i :: c) (j :: d) (k :: e) Source #

Instances

Instances details

type Eval (Pure4 f w x y z :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Pure4 f w x y z :: a2 -> Type) = f w x y z

data Pure5 (g :: a -> b -> c -> d -> e -> f) (h :: a) (i :: b) (j :: c) (k :: d) (l :: e) (m :: f) Source #

Instances

Instances details

type Eval (Pure5 f v w x y z :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Pure5 f v w x y z :: a2 -> Type) = f v w x y z

data Pure6 (h :: a -> b -> c -> d -> e -> f -> g) (i :: a) (j :: b) (k :: c) (l :: d) (m :: e) (n :: f) (o :: g) Source #

Instances

Instances details

type Eval (Pure6 f2 u v w x y z :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Pure6 f2 u v w x y z :: a2 -> Type) = f2 u v w x y z

data Pure7 (i :: a -> b -> c -> d -> e -> f -> g -> h) (j :: a) (k :: b) (l :: c) (m :: d) (n :: e) (o :: f) (p :: g) (q :: h) Source #

Instances

Instances details

type Eval (Pure7 f2 t u v w x y z :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Pure7 f2 t u v w x y z :: a2 -> Type) = f2 t u v w x y z

data Pure8 (j :: a -> b -> c -> d -> e -> f -> g -> h -> i) (k :: a) (l :: b) (m :: c) (n :: d) (o :: e) (p :: f) (q :: g) (r :: h) (s :: i) Source #

Instances

Instances details

type Eval (Pure8 f2 s t u v w x y z :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Pure8 f2 s t u v w x y z :: a2 -> Type) = f2 s t u v w x y z

data Pure9 (k :: a -> b -> c -> d -> e -> f -> g -> h -> i -> j) (l :: a) (m :: b) (n :: c) (o :: d) (p :: e) (q :: f) (r :: g) (s :: h) (t :: i) (u :: j) Source #

Instances

Instances details

type Eval (Pure9 f2 r s t u v w x y z :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Pure9 f2 r s t u v w x y z :: a2 -> Type) = f2 r s t u v w x y z

data ((c :: a -> Exp b) =<< (d :: Exp a)) (e :: b) infixr 1 Source #

Instances

Instances details

type Eval (k =<< e :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (k =<< e :: a2 -> Type) = Eval (k (Eval e))

data ((c :: Exp a) >>= (d :: a -> Exp b)) (e :: b) infixl 1 Source #

Instances

Instances details

type Eval (e >>= k :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (e >>= k :: a2 -> Type) = Eval (k (Eval e))

data ((d :: b -> Exp c) <=< (e :: a -> Exp b)) (f :: a) (g :: c) infixr 1 Source #

Instances

Instances details

type Eval ((f <=< g) x :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval ((f <=< g) x :: a2 -> Type) = Eval (f (Eval (g x)))

type LiftM = (=<<) :: (a -> Exp b) -> Exp a -> b -> Type Source #

data LiftM2 (d :: a -> b -> Exp c) (e :: Exp a) (f :: Exp b) (g :: c) Source #

Instances

Instances details

type Eval (LiftM2 f x y :: a3 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (LiftM2 f x y :: a3 -> Type) = Eval (f (Eval x) (Eval y))

data LiftM3 (e :: a -> b -> c -> Exp d) (f :: Exp a) (g :: Exp b) (h :: Exp c) (i :: d) Source #

Instances

Instances details

type Eval (LiftM3 f x y z :: a4 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (LiftM3 f x y z :: a4 -> Type) = Eval (f (Eval x) (Eval y) (Eval z))

data Join (b :: Exp (Exp a)) (c :: a) Source #

Instances

Instances details

type Eval (Join e :: a -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Join e :: a -> Type) = Eval (Eval e)

data ((c :: a -> b) <$> (d :: Exp a)) (e :: b) infixl 4 Source #

Instances

Instances details

type Eval (f <$> e :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (f <$> e :: a2 -> Type) = f (Eval e)

data ((c :: Exp (a -> b)) <*> (d :: Exp a)) (e :: b) infixl 4 Source #

Instances

Instances details

type Eval (f <*> e :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (f <*> e :: a2 -> Type) = Eval f (Eval e)

data Flip (d :: a -> b -> Exp c) (e :: b) (f :: a) (g :: c) Source #

Instances

Instances details

type Eval (Flip f y x :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (Flip f y x :: a2 -> Type) = Eval (f x y)

data ConstFn (c :: a) (d :: b) (e :: a) Source #

Instances

Instances details

type Eval (ConstFn a2 _b :: a1 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (ConstFn a2 _b :: a1 -> Type) = a2

data ((c :: a -> Exp b) $ (d :: a)) (e :: b) infixr 0 Source #

Note that this denotes the identity function, so ($) f can usually be replaced with f.

Instances

Instances details

type Eval (f $ a3 :: a2 -> Type) Source #
Instance details Defined in Fcf.Combinators type Eval (f $ a3 :: a2 -> Type) = Eval (f a3)

Operations on common types

Pairs

data Uncurry (d :: a -> b -> Exp c) (e :: (a, b)) (f :: c) Source #

Instances

Instances details

type Eval (Uncurry f '(x, y) :: a2 -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (Uncurry f '(x, y) :: a2 -> Type) = Eval (f x y)

data Fst (c :: (a, b)) (d :: a) Source #

Instances

Instances details

type Eval (Fst '(a2, _b) :: a1 -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (Fst '(a2, _b) :: a1 -> Type) = a2

data Snd (c :: (a, b)) (d :: b) Source #

Instances

Instances details

type Eval (Snd '(_a, b) :: a2 -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (Snd '(_a, b) :: a2 -> Type) = b

data ((a :: b -> Exp c) *** (d :: b' -> Exp c')) (e :: (b, b')) (f :: (c, c')) infixr 3 Source #

Specialization of Bimap for pairs.

Instances

Instances details

type Eval ((f *** f') '(b2, b'2) :: (k1, k2) -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval ((f *** f') '(b2, b'2) :: (k1, k2) -> Type) = '(Eval (f b2), Eval (f' b'2))

Either

data UnEither (d :: a -> Exp c) (e :: b -> Exp c) (f :: Either a b) (g :: c) Source #

Instances

Instances details

type Eval (UnEither f g ('Left x :: Either a1 b) :: a2 -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (UnEither f g ('Left x :: Either a1 b) :: a2 -> Type) = Eval (f x)
type Eval (UnEither f g ('Right y :: Either a1 b) :: a2 -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (UnEither f g ('Right y :: Either a1 b) :: a2 -> Type) = Eval (g y)

data IsLeft (c :: Either a b) (d :: Bool) Source #

Instances

Instances details

type Eval (IsLeft ('Left _a :: Either a b) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (IsLeft ('Left _a :: Either a b) :: Bool -> Type) = 'True
type Eval (IsLeft ('Right _a :: Either a b) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (IsLeft ('Right _a :: Either a b) :: Bool -> Type) = 'False

data IsRight (c :: Either a b) (d :: Bool) Source #

Instances

Instances details

type Eval (IsRight ('Left _a :: Either a b) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (IsRight ('Left _a :: Either a b) :: Bool -> Type) = 'False
type Eval (IsRight ('Right _a :: Either a b) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (IsRight ('Right _a :: Either a b) :: Bool -> Type) = 'True

Maybe

data UnMaybe (c :: Exp b) (d :: a -> Exp b) (e :: Maybe a) (f :: b) Source #

Instances

Instances details

type Eval (UnMaybe y f ('Just x) :: a1 -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (UnMaybe y f ('Just x) :: a1 -> Type) = Eval (f x)
type Eval (UnMaybe y f ('Nothing :: Maybe a2) :: a1 -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (UnMaybe y f ('Nothing :: Maybe a2) :: a1 -> Type) = Eval y

data FromMaybe (a :: k) (b :: Maybe k) (c :: k) Source #

Instances

Instances details

type Eval (FromMaybe _a ('Just b) :: a -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (FromMaybe _a ('Just b) :: a -> Type) = b
type Eval (FromMaybe a2 ('Nothing :: Maybe a1) :: a1 -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (FromMaybe a2 ('Nothing :: Maybe a1) :: a1 -> Type) = a2

data IsNothing (b :: Maybe a) (c :: Bool) Source #

Instances

Instances details

type Eval (IsNothing ('Just _a) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (IsNothing ('Just _a) :: Bool -> Type) = 'False
type Eval (IsNothing ('Nothing :: Maybe a) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (IsNothing ('Nothing :: Maybe a) :: Bool -> Type) = 'True

data IsJust (b :: Maybe a) (c :: Bool) Source #

Instances

Instances details

type Eval (IsJust ('Just _a) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (IsJust ('Just _a) :: Bool -> Type) = 'True
type Eval (IsJust ('Nothing :: Maybe a) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Common type Eval (IsJust ('Nothing :: Maybe a) :: Bool -> Type) = 'False

Lists

data ((b :: [a]) ++ (c :: [a])) (d :: [a]) Source #

List catenation.

Example

Expand

>>> data Example where Ex :: a -> Example  -- Hide the type of examples to avoid brittleness in different GHC versions
>>> :kind! Ex (Eval ([1, 2] ++ [3, 4]) :: [Natural])
Ex (Eval ([1, 2] ++ [3, 4]) :: [Natural]) :: Example
= Ex [1, 2, 3, 4]

Instances

Instances details

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

data Head (b :: [a]) (c :: Maybe a) Source #

Instances

Instances details

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

data Last (b :: [a]) (c :: Maybe a) Source #

Instances

Instances details

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

data Tail (b :: [a]) (c :: Maybe [a]) Source #

Instances

Instances details

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 Cons (b :: a) (c :: [a]) (d :: [a]) Source #

Append an element to a list.

Example

Expand

>>> :kind! Eval (Cons 1 [2, 3])
Eval (Cons 1 [2, 3]) :: [Natural]
= [1, 2, 3]
>>> :kind! Eval (Cons Int [Char, Maybe Double])
Eval (Cons Int [Char, Maybe Double]) :: [*]
= [Int, Char, Maybe Double]

Instances

Instances details

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 Snoc (b :: [a]) (c :: a) (d :: [a]) Source #

Append an element to the end of a list.

Example

Expand

>>> :kind! Eval (Snoc [1,2,3] 4)
Eval (Snoc [1,2,3] 4) :: [Natural]
= [1, 2, 3, 4]

Instances

Instances details

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

data Cons2 (c :: (a, b)) (d :: ([a], [b])) (e :: ([a], [b])) Source #

Append elements to two lists. Used in the definition of Unzip.

Instances

Instances details

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

data Init (b :: [a]) (c :: Maybe [a]) Source #

Instances

Instances details

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

data Uncons (b :: [a]) (c :: Maybe (a, [a])) Source #

Instances

Instances details

type Eval (Uncons ('[] :: [a]) :: Maybe (a, [a]) -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Uncons ('[] :: [a]) :: Maybe (a, [a]) -> Type) = 'Nothing :: Maybe (a, [a])
type Eval (Uncons (a ': xs) :: Maybe (k, [k]) -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Uncons (a ': xs) :: Maybe (k, [k]) -> Type) = 'Just '(a, xs)

data Unsnoc (b :: [a]) (c :: Maybe ([a], a)) Source #

Decompose a list into init and last

Example

Expand

>>> :kind! Eval (Unsnoc '[])
Eval (Unsnoc '[]) :: Maybe ([a], a)
= Nothing

>>> :kind! Eval (Unsnoc '[1])
Eval (Unsnoc '[1]) :: Maybe ([Natural], Natural)
= Just '( '[], 1)

>>> :kind! Eval (Unsnoc '[1,2,3])
Eval (Unsnoc '[1,2,3]) :: Maybe ([Natural], Natural)
= Just '([1, 2], 3)

Instances

Instances details

type Eval (Unsnoc (x ': (y ': ys)) :: Maybe ([a], a) -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Unsnoc (x ': (y ': ys)) :: Maybe ([a], a) -> Type)
type Eval (Unsnoc ('[] :: [a]) :: Maybe ([a], a) -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Unsnoc ('[] :: [a]) :: Maybe ([a], a) -> Type) = 'Nothing :: Maybe ([a], a)
type Eval (Unsnoc '[x] :: Maybe ([k], k) -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Unsnoc '[x] :: Maybe ([k], k) -> Type) = 'Just '('[] :: [k], x)

data Singleton (b :: a) (c :: [a]) Source #

Instances

Instances details

type Eval (Singleton x :: [k] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Singleton x :: [k] -> Type) = '[x]

data Null (b :: [a]) (c :: Bool) Source #

Instances

Instances details

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

data Length (b :: [a]) (c :: Nat) Source #

Instances

Instances details

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

data Reverse (b :: [a]) (c :: [a]) Source #

Reverse a list.

Example

Expand

>>> :kind! Eval (Reverse [1,2,3,4,5])
Eval (Reverse [1,2,3,4,5]) :: [Natural]
= [5, 4, 3, 2, 1]

Instances

Instances details

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

data Intersperse (b :: a) (c :: [a]) (d :: [a]) Source #

Intersperse a separator between elements of a list.

Example

Expand

>>> :kind! Eval (Intersperse 0 [1,2,3,4])
Eval (Intersperse 0 [1,2,3,4]) :: [Natural]
= [1, 0, 2, 0, 3, 0, 4]

Instances

Instances details

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

data Intercalate (b :: [a]) (c :: [[a]]) (d :: [a]) Source #

Join a list of words separated by some word.

Example

Expand

>>> :kind! Eval (Intercalate '[", "] [ '["Lorem"], '["ipsum"], '["dolor"] ])
Eval (Intercalate '[", "] [ '["Lorem"], '["ipsum"], '["dolor"] ]) :: [TL.Symbol]
= ["Lorem", ", ", "ipsum", ", ", "dolor"]

Instances

Instances details

type Eval (Intercalate xs xss :: [a] -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Intercalate xs xss :: [a] -> Type) = Eval ((Concat :: [[a]] -> [a] -> Type) =<< Intersperse xs xss)

data Foldr (c :: a -> b -> Exp b) (d :: b) (e :: t a) (f :: b) Source #

Right fold.

Example

Expand

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

Instances

Instances details

type Eval (Foldr f y ('Left _a :: Either a3 a1) :: a2 -> Type) Source #
Instance details Defined in Fcf.Class.Foldable type Eval (Foldr f y ('Left _a :: Either a3 a1) :: a2 -> Type) = y
type Eval (Foldr f y ('Right x :: Either a3 a1) :: a2 -> Type) Source #
Instance details Defined in Fcf.Class.Foldable type Eval (Foldr f y ('Right x :: Either a3 a1) :: a2 -> Type) = Eval (f x y)
type Eval (Foldr f y ('Just x) :: a2 -> Type) Source #
Instance details Defined in Fcf.Class.Foldable type Eval (Foldr f y ('Just x) :: a2 -> Type) = Eval (f x y)
type Eval (Foldr f y ('Nothing :: Maybe a1) :: a2 -> Type) Source #
Instance details Defined in Fcf.Class.Foldable type Eval (Foldr f y ('Nothing :: Maybe a1) :: a2 -> Type) = y
type Eval (Foldr f y (x ': xs) :: a2 -> Type) Source #
Instance details Defined in Fcf.Class.Foldable 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.Class.Foldable type Eval (Foldr f y ('[] :: [a1]) :: a2 -> Type) = y

data UnList (c :: b) (d :: a -> b -> Exp b) (e :: [a]) (f :: b) Source #

This is Foldr with its argument flipped.

Instances

Instances details

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

data Concat (a :: t m) (b :: m) Source #

Concatenate a collection of elements from a monoid.

Example

Expand

For example, fold a list of lists.

Concat :: [[a]] -> Exp [a]

>>> :kind! Eval (Concat ([[1,2], [3,4], [5,6]]))
Eval (Concat ([[1,2], [3,4], [5,6]])) :: [Natural]
= [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 [Char], Either Double Int]

Instances

Instances details

type Eval (Concat xs :: a -> Type) Source #
Instance details Defined in Fcf.Class.Foldable type Eval (Concat xs :: a -> Type) = Eval (FoldMap (Pure :: a -> a -> Type) xs)

data ConcatMap (c :: a -> Exp [b]) (d :: t a) (e :: [b]) Source #

Map a function and concatenate the results.

This is FoldMap specialized to the list monoid.

Instances

Instances details

type Eval (ConcatMap f xs :: [b] -> Type) Source #
Instance details Defined in Fcf.Class.Foldable type Eval (ConcatMap f xs :: [b] -> Type) = Eval (FoldMap f xs)

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

Unfold a generator into a list.

Example

Expand

>>> data ToThree :: Nat -> Exp (Maybe (Nat, Nat))
>>> :{
type instance Eval (ToThree b) =
  If (4 TL.<=? b)
    Nothing
    (Just '(b, b TL.+ 1))
:}

>>> :kind! Eval (Unfoldr ToThree 0)
Eval (Unfoldr ToThree 0) :: [Natural]
= [0, 1, 2, 3]

Instances

Instances details

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

data Replicate (b :: Nat) (c :: a) (d :: [a]) Source #

Repeat the same element in a list.

Example

Expand

>>> :kind! Eval (Replicate 4 '("ok", 2))
Eval (Replicate 4 '("ok", 2)) :: [(TL.Symbol, Natural)]
= ['("ok", 2), '("ok", 2), '("ok", 2), '("ok", 2)]

Instances

Instances details

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

data Take (b :: Nat) (c :: [a]) (d :: [a]) Source #

Take a prefix of fixed length.

Example

Expand

>>> :kind! Eval (Take 2 [1,2,3,4,5])
Eval (Take 2 [1,2,3,4,5]) :: [Natural]
= [1, 2]

Instances

Instances details

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

data Drop (b :: Nat) (c :: [a]) (d :: [a]) Source #

Drop a prefix of fixed length, evaluate to the remaining suffix.

Example

Expand

>>> :kind! Eval (Drop 2 [1,2,3,4,5])
Eval (Drop 2 [1,2,3,4,5]) :: [Natural]
= [3, 4, 5]

Instances

Instances details

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

data SplitAt (b :: Nat) (c :: [a]) (d :: ([a], [a])) Source #

Return a tuple where first element is xs prefix of length n and second element is the remainder of the list.

Example

Expand

>>> :kind! Eval (SplitAt 3 '[1,2,3,4,5])
Eval (SplitAt 3 '[1,2,3,4,5]) :: ([Natural], [Natural])
= '([1, 2, 3], [4, 5])

Instances

Instances details

type Eval (SplitAt n xs :: ([a], [a]) -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (SplitAt n xs :: ([a], [a]) -> Type) = '(Eval (Take n xs), Eval (Drop n xs))

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

Take the longest prefix of elements satisfying a predicate.

Example

Expand

>>> :kind! Eval (TakeWhile ((>=) 3) [1, 2, 3, 4, 5])
Eval (TakeWhile ((>=) 3) [1, 2, 3, 4, 5]) :: [Natural]
= [1, 2, 3]

Instances

Instances details

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

Drop the longest prefix of elements satisfying a predicate, evaluate to the remaining suffix.

Example

Expand

:kind! Eval (DropWhile ((>=) 3) [1, 2, 3, 4, 5]) Eval (DropWhile ((>=) 3) [1, 2, 3, 4, 5]) :: [Natural] = [4, 5]

Instances

Instances details

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 Span (b :: a -> Exp Bool) (c :: [a]) (d :: ([a], [a])) Source #

Span, applied to a predicate p and a list xs, returns a tuple: the first component is the longest prefix (possibly empty) of xs whose elements satisfy p; the second component is the remainder of the list.

See also TakeWhile, DropWhile, and Break.

Example

Expand

>>> :kind! Eval (Span (Flip (<) 3) [1,2,3,4,1,2])
Eval (Span (Flip (<) 3) [1,2,3,4,1,2]) :: ([Natural], [Natural])
= '([1, 2], [3, 4, 1, 2])

>>> :kind! Eval (Span (Flip (<) 9) [1,2,3])
Eval (Span (Flip (<) 9) [1,2,3]) :: ([Natural], [Natural])
= '([1, 2, 3], '[])

>>> :kind! Eval (Span (Flip (<) 0) [1,2,3])
Eval (Span (Flip (<) 0) [1,2,3]) :: ([Natural], [Natural])
= '( '[], [1, 2, 3])

Instances

Instances details

type Eval (Span p lst :: ([a], [a]) -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Span p lst :: ([a], [a]) -> Type) = '(Eval (TakeWhile p lst), Eval (DropWhile p lst))

data Break (b :: a -> Exp Bool) (c :: [a]) (d :: ([a], [a])) Source #

Break, applied to a predicate p and a list xs, returns a tuple: the first component is the longest prefix (possibly empty) of xs whose elements do not satisfy p; the second component is the remainder of the list.

Example

Expand

>>> :kind! Eval (Break (Flip (>) 3) [1,2,3,4,1,2])
Eval (Break (Flip (>) 3) [1,2,3,4,1,2]) :: ([Natural], [Natural])
= '([1, 2, 3], [4, 1, 2])

>>> :kind! Eval (Break (Flip (<) 9) [1,2,3])
Eval (Break (Flip (<) 9) [1,2,3]) :: ([Natural], [Natural])
= '( '[], [1, 2, 3])

>>> :kind! Eval (Break (Flip (>) 9) [1,2,3])
Eval (Break (Flip (>) 9) [1,2,3]) :: ([Natural], [Natural])
= '([1, 2, 3], '[])

Instances

Instances details

type Eval (Break p lst :: ([a], [a]) -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Break p lst :: ([a], [a]) -> Type) = Eval (Span (Not <=< p) lst)

data Tails (b :: [a]) (c :: [[a]]) Source #

List of suffixes of a list.

Example

Expand

>>> :kind! Eval (Tails [0,1,2,3])
Eval (Tails [0,1,2,3]) :: [[Natural]]
= [[0, 1, 2, 3], [1, 2, 3], [2, 3], '[3]]

Instances

Instances details

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

data IsPrefixOf (b :: [a]) (c :: [a]) (d :: Bool) Source #

Return True when the first list is a prefix of the second.

Example

Expand

>>> :kind! Eval ([0,1,2] `IsPrefixOf` [0,1,2,3,4,5])
Eval ([0,1,2] `IsPrefixOf` [0,1,2,3,4,5]) :: Bool
= True

>>> :kind! Eval ([0,1,2] `IsPrefixOf` [0,1,3,2,4,5])
Eval ([0,1,2] `IsPrefixOf` [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 ([0,1,3,2,4,5] `IsPrefixOf` '[])
Eval ([0,1,3,2,4,5] `IsPrefixOf` '[]) :: Bool
= False

Instances

Instances details

type Eval (IsPrefixOf xs ys :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (IsPrefixOf xs ys :: Bool -> Type)

data IsSuffixOf (b :: [a]) (c :: [a]) (d :: Bool) Source #

Return True when 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

Instances details

type Eval (IsSuffixOf xs ys :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (IsSuffixOf xs ys :: Bool -> Type) = Eval (IsPrefixOf ((Reverse :: [a] -> [a] -> Type) @@ xs) ((Reverse :: [a] -> [a] -> Type) @@ ys))

data IsInfixOf (b :: [a]) (c :: [a]) (d :: Bool) Source #

Return True when the first list is contained within 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

Instances details

type Eval (IsInfixOf xs ys :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (IsInfixOf xs ys :: Bool -> Type) = Eval ((Any (IsPrefixOf xs) :: [[a]] -> Bool -> Type) =<< Tails ys)

data Elem (b :: a) (c :: [a]) (d :: Bool) Source #

Return True if an element is in a list.

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

Instances details

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 (a :: k) (c :: [(k, b)]) (d :: Maybe b) Source #

Find an element associated with a key in an association list.

Instances

Instances details

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 Find (b :: a -> Exp Bool) (c :: [a]) (d :: Maybe a) Source #

Find Just the first element satisfying a predicate, or evaluate to Nothing if no element satisfies the predicate.

Example

Expand

>>> :kind! Eval (Find (TyEq 0) [1,2,3])
Eval (Find (TyEq 0) [1,2,3]) :: Maybe Natural
= Nothing

>>> :kind! Eval (Find (TyEq 0) [1,2,3,0])
Eval (Find (TyEq 0) [1,2,3,0]) :: Maybe Natural
= Just 0

Instances

Instances details

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

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

Keep all elements that satisfy a predicate, remove all that don't.

Example

Expand

>>> :kind! Eval (Filter ((>) 3) [1,2,3,0])
Eval (Filter ((>) 3) [1,2,3,0]) :: [Natural]
= [1, 2, 0]

Instances

Instances details

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

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

Split a list into one where all elements satisfy a predicate, and a second where no elements satisfy it.

Example

Expand

>>> :kind! Eval (Partition ((>=) 35) [20, 30, 40, 50])
Eval (Partition ((>=) 35) [20, 30, 40, 50]) :: ([Natural],
                                                [Natural])
= '([20, 30], [40, 50])

Instances

Instances details

type Eval (Partition p lst :: ([a], [a]) -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Partition p lst :: ([a], [a]) -> Type)

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

Find the index of an element satisfying the predicate.

Example

Expand

>>> :kind! Eval (FindIndex ((<=) 3) [1,2,3,1,2,3])
Eval (FindIndex ((<=) 3) [1,2,3,1,2,3]) :: Maybe Natural
= Just 2

>>> :kind! Eval (FindIndex ((>) 0) [1,2,3,1,2,3])
Eval (FindIndex ((>) 0) [1,2,3,1,2,3]) :: Maybe Natural
= Nothing

Instances

Instances details

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

data SetIndex (b :: Nat) (c :: a) (d :: [a]) (e :: [a]) Source #

Modify an element at a given index.

The list is unchanged if the index is out of bounds.

Example

Expand

>>> :kind! Eval (SetIndex 2 7 [1,2,3])
Eval (SetIndex 2 7 [1,2,3]) :: [Natural]
= [1, 2, 7]

Instances

Instances details

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 (d :: a -> b -> Exp c) (e :: [a]) (f :: [b]) (g :: [c]) Source #

Combine elements of two lists pairwise.

Example

Expand

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

Instances

Instances details

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

data Zip (c :: [a]) (d :: [b]) (e :: [(a, b)]) Source #

Instances

Instances details

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

Instances

Instances details

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

Bool

data UnBool (b :: Exp a) (c :: Exp a) (d :: Bool) (e :: a) Source #

N.B.: The order of the two branches is the opposite of "if": UnBool ifFalse ifTrue bool.

This mirrors the default order of constructors:

data Bool = False | True
----------- False < True

Instances

Instances details

type Eval (UnBool fal tru 'False :: a -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval (UnBool fal tru 'False :: a -> Type) = Eval fal
type Eval (UnBool fal tru 'True :: a -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval (UnBool fal tru 'True :: a -> Type) = Eval tru

data ((a :: Bool) || (b :: Bool)) (c :: Bool) infixr 2 Source #

Instances

Instances details

type Eval ('False \|\| b :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval ('False \|\| b :: Bool -> Type) = b
type Eval ('True \|\| b :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval ('True \|\| b :: Bool -> Type) = 'True
type Eval (a \|\| 'False :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval (a \|\| 'False :: Bool -> Type) = a
type Eval (a \|\| 'True :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval (a \|\| 'True :: Bool -> Type) = 'True

data ((a :: Bool) && (b :: Bool)) (c :: Bool) infixr 3 Source #

Instances

Instances details

type Eval ('False && b :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval ('False && b :: Bool -> Type) = 'False
type Eval ('True && b :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval ('True && b :: Bool -> Type) = b
type Eval (a && 'False :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval (a && 'False :: Bool -> Type) = 'False
type Eval (a && 'True :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval (a && 'True :: Bool -> Type) = a

data Not (a :: Bool) (b :: Bool) Source #

Instances

Instances details

type Eval (Not 'False) Source #
Instance details Defined in Fcf.Data.Bool type Eval (Not 'False) = 'True
type Eval (Not 'True) Source #
Instance details Defined in Fcf.Data.Bool type Eval (Not 'True) = 'False

Case splitting

data Case (a :: [Match j k]) (b :: j) (c :: k) Source #

(Limited) equivalent of \case { .. } syntax. Supports matching of exact values (-->) and final matches for any value (Any) or for passing value to subcomputation (Else). Examples:

type BoolToNat = Case
  [ 'True  --> 0
  , 'False --> 1
  ]

type NatToBool = Case
  [ 0 --> 'False
  , Any   'True
  ]

type ZeroOneOrSucc = Case
  [ 0  --> 0
  , 1  --> 1
  , Else   ((+) 1)
  ]

Instances

Instances details

type Eval (Case ms a :: k -> Type) Source #
Instance details Defined in Fcf.Utils type Eval (Case ms a :: k -> Type)

data Match j k Source #

type (-->) = 'Match_ :: j -> k -> Match j k infix 0 Source #

Match concrete type in Case.

type Is = 'Is_ :: (j -> Exp Bool) -> k -> Match j k Source #

Match on predicate being successful with type in Case.

type Any = 'Any_ :: k -> Match j k Source #

Match any type in Case. Should be used as a final branch.

Note: this identifier conflicts with Any (from Fcf.Class.Foldable) Any (from Data.Monoid), and Any (from GHC.Exts).

We recommend importing this one qualified.

type Else = 'Else_ :: (j -> Exp k) -> Match j k Source #

Pass type being matched in Case to subcomputation. Should be used as a final branch.

Nat

data ((a :: Nat) + (b :: Nat)) (c :: Nat) Source #

Instances

Instances details

type Eval (a + b :: Nat -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a + b :: Nat -> Type) = a + b

data ((a :: Nat) - (b :: Nat)) (c :: Nat) Source #

Instances

Instances details

type Eval (a - b :: Nat -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a - b :: Nat -> Type) = a - b

data ((a :: Nat) * (b :: Nat)) (c :: Nat) Source #

Instances

Instances details

type Eval (a * b :: Nat -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a * b :: Nat -> Type) = a * b

data ((a :: Nat) ^ (b :: Nat)) (c :: Nat) Source #

Instances

Instances details

type Eval (a ^ b :: Nat -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a ^ b :: Nat -> Type) = a ^ b

data ((a :: Nat) <= (b :: Nat)) (c :: Bool) Source #

Instances

Instances details

type Eval (a <= b :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a <= b :: Bool -> Type) = a <=? b

data ((a :: Nat) >= (b :: Nat)) (c :: Bool) Source #

Instances

Instances details

type Eval (a >= b :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a >= b :: Bool -> Type) = b <=? a

data ((a :: Nat) < (b :: Nat)) (c :: Bool) Source #

Instances

Instances details

type Eval (a < b :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a < b :: Bool -> Type) = Eval (Not =<< (a >= b))

data ((a :: Nat) > (b :: Nat)) (c :: Bool) Source #

Instances

Instances details

type Eval (a > b :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a > b :: Bool -> Type) = Eval (Not =<< (a <= b))

Overloaded operations

data Map (c :: a -> Exp b) (d :: f a) (e :: f b) Source #

Type-level fmap for type-level functors.

Note: this name clashes with Map from containers. FMap is provided as a synonym to avoid this.

Example

Expand

>>> data Example where Ex :: a -> Example  -- Hide the type of examples to avoid brittleness in different GHC versions
>>> data AddMul :: Nat -> Nat -> Exp Nat
>>> type instance Eval (AddMul x y) = (x TL.+ y) TL.* (x TL.+ y)
>>> :kind! Ex (Eval (Map (AddMul 2) '[0, 1, 2, 3, 4]) :: [Nat])
Ex (Eval (Map (AddMul 2) '[0, 1, 2, 3, 4]) :: [Nat]) :: Example
= Ex [4, 9, 16, 25, 36]

Instances

Instances details

type Eval (Map f ('Just a3) :: Maybe a2 -> Type) Source #
Instance details Defined in Fcf.Class.Functor type Eval (Map f ('Just a3) :: Maybe a2 -> Type) = 'Just (Eval (f a3))
type Eval (Map f ('Nothing :: Maybe a) :: Maybe b -> Type) Source #
Instance details Defined in Fcf.Class.Functor type Eval (Map f ('Nothing :: Maybe a) :: Maybe b -> Type) = 'Nothing :: Maybe b
type Eval (Map f ('[] :: [a]) :: [b] -> Type) Source #
Instance details Defined in Fcf.Class.Functor type Eval (Map f ('[] :: [a]) :: [b] -> Type) = '[] :: [b]
type Eval (Map f (a2 ': as) :: [b] -> Type) Source #
Instance details Defined in Fcf.Class.Functor type Eval (Map f (a2 ': as) :: [b] -> Type) = Eval (f a2) ': Eval (Map f as)
type Eval (Map f ('Left x :: Either a2 a1) :: Either a2 b -> Type) Source #
Instance details Defined in Fcf.Class.Functor type Eval (Map f ('Left x :: Either a2 a1) :: Either a2 b -> Type) = 'Left x :: Either a2 b
type Eval (Map f ('Right a3 :: Either a2 a1) :: Either a2 b -> Type) Source #
Instance details Defined in Fcf.Class.Functor type Eval (Map f ('Right a3 :: Either a2 a1) :: Either a2 b -> Type) = 'Right (Eval (f a3)) :: Either a2 b
type Eval (Map f '(x, a2) :: (k2, k1) -> Type) Source #
Instance details Defined in Fcf.Class.Functor type Eval (Map f '(x, a2) :: (k2, k1) -> Type) = '(x, Eval (f a2))
type Eval (Map f '(x, y, a2) :: (k2, k3, k1) -> Type) Source #
Instance details Defined in Fcf.Class.Functor type Eval (Map f '(x, y, a2) :: (k2, k3, k1) -> Type) = '(x, y, Eval (f a2))
type Eval (Map f '(x, y, z, a2) :: (k2, k3, k4, k1) -> Type) Source #
Instance details Defined in Fcf.Class.Functor type Eval (Map f '(x, y, z, a2) :: (k2, k3, k4, k1) -> Type) = '(x, y, z, Eval (f a2))
type Eval (Map f '(x, y, z, w, a2) :: (k2, k3, k4, k5, k1) -> Type) Source #
Instance details Defined in Fcf.Class.Functor type Eval (Map f '(x, y, z, w, a2) :: (k2, k3, k4, k5, k1) -> Type) = '(x, y, z, w, Eval (f a2))

data Bimap (c :: a -> Exp a') (d :: b -> Exp b') (e :: f a b) (g :: f a' b') Source #

Type-level bimap.

Example

Expand

>>> data Example where Ex :: a -> Example  -- Hide the type of examples to avoid brittleness in different GHC versions
>>> :kind! Ex (Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Natural, Natural))
Ex (Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Natural, Natural)) :: Example
= Ex '(3, 3)

Instances

Instances details

type Eval (Bimap f g ('Right y :: Either a b1) :: Either a' b2 -> Type) Source #
Instance details Defined in Fcf.Class.Bifunctor type Eval (Bimap f g ('Right y :: Either a b1) :: Either a' b2 -> Type) = 'Right (Eval (g y)) :: Either a' b2
type Eval (Bimap f g ('Left x :: Either a1 b) :: Either a2 b' -> Type) Source #
Instance details Defined in Fcf.Class.Bifunctor type Eval (Bimap f g ('Left x :: Either a1 b) :: Either a2 b' -> Type) = 'Left (Eval (f x)) :: Either a2 b'
type Eval (Bimap f g '(x, y) :: (k1, k2) -> Type) Source #
Instance details Defined in Fcf.Class.Bifunctor type Eval (Bimap f g '(x, y) :: (k1, k2) -> Type) = '(Eval (f x), Eval (g y))

Miscellaneous

data Error (b :: Symbol) (c :: a) Source #

Type-level error.

Instances

Instances details

type Eval (Error msg :: a -> Type) Source #
Instance details Defined in Fcf.Utils type Eval (Error msg :: a -> Type) = TypeError ('Text msg) :: a

data Constraints (a :: [Constraint]) b Source #

Conjunction of a list of constraints.

Instances

Instances details

type Eval (Constraints (a ': as) :: Constraint -> Type) Source #
Instance details Defined in Fcf.Utils type Eval (Constraints (a ': as) :: Constraint -> Type) = (a, Eval (Constraints as))
type Eval (Constraints ('[] :: [Constraint])) Source #
Instance details Defined in Fcf.Utils type Eval (Constraints ('[] :: [Constraint])) = ()

data TyEq (c :: a) (d :: b) (e :: Bool) Source #

Type equality.

Details

Expand

The base library also defines a similar (==); it differs from TyEq in the following ways:

TyEq is heterogeneous: its arguments may have different kinds;
TyEq is reflexive: TyEq a a always reduces to True even if a is a variable.

Instances

Instances details

type Eval (TyEq a b :: Bool -> Type) Source #
Instance details Defined in Fcf.Utils type Eval (TyEq a b :: Bool -> Type)

type family Stuck :: a Source #

A stuck type that can be used like a type-level undefined.

class IsBool (b :: Bool) where Source #

Methods

_If :: (b ~ 'True => r) -> (b ~ 'False => r) -> r Source #

Instances

Instances details

IsBool 'False Source #
Instance details Defined in Fcf.Utils Methods _If :: ('False ~ 'True => r) -> ('False ~ 'False => r) -> r Source #
IsBool 'True Source #
Instance details Defined in Fcf.Utils Methods _If :: ('True ~ 'True => r) -> ('True ~ 'False => r) -> r Source #

type family If (cond :: Bool) (tru :: k) (fls :: k) :: k where ... #

Type-level If. If True a b ==> a; If False a b ==> b

Equations

If 'True (tru :: k) (fls :: k) = tru
If 'False (tru :: k) (fls :: k) = fls

data Assert (a :: ErrorMessage) (b :: Exp Bool) (c :: r) (d :: r) Source #

A compile-time assert.

Raises the provided TypeError, whenever the condition evaluates to False.

Usage example: type ExampleAssertionFailure = Eval ( Pure '["foo", "bar"] >>= Length >>= Assert ('Text Assertion) (TyEq Int Void) )

Instances

Instances details

type Eval (Assert msg mcond k :: a -> Type) Source #
Instance details Defined in Fcf.Utils type Eval (Assert msg mcond k :: a -> Type) = Eval (If (Eval mcond) (Pure k) (TError msg :: a -> Type))

data AssertNot (a :: ErrorMessage) (b :: Exp Bool) (c :: r) (d :: r) Source #

Compile-time assert, with condition negated.

Raises the provided TypeError, whenever the condition evaluates to True.

Also see Assert.

Instances

Instances details

type Eval (AssertNot err mcond k :: a -> Type) Source #
Instance details Defined in Fcf.Utils type Eval (AssertNot err mcond k :: a -> Type) = Eval (Assert err (Not =<< mcond) k)

type Eval ('False \|\| b :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval ('False \|\| b :: Bool -> Type) = b
type Eval ('True \|\| b :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval ('True \|\| b :: Bool -> Type) = 'True
type Eval (a \|\| 'False :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval (a \|\| 'False :: Bool -> Type) = a
type Eval (a \|\| 'True :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Bool type Eval (a \|\| 'True :: Bool -> Type) = 'True