first-class-families-0.8.0.1: First-class type families

Safe Haskell | Safe-Inferred
Language | Haskell2010

Fcf

Contents

- First-class type families
  - Functional combinators
- Operations on common types
  - Pairs
  - Either
  - Maybe
  - Lists
  - Bool
  - Case splitting
  - Nat
- 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,
        TypeInType,
        TypeOperators,
        UndecidableInstances #-}

Synopsis

- type Exp a = a -> Type
- type family Eval (e :: Exp a) :: a
- type (@@) f x = Eval (f x)
- data Pure :: a -> Exp a
- data Pure1 :: (a -> b) -> a -> Exp b
- data Pure2 :: (a -> b -> c) -> a -> b -> Exp c
- data Pure3 :: (a -> b -> c -> d) -> a -> b -> c -> Exp d
- data (=<<) :: (a -> Exp b) -> Exp a -> Exp b
- data (<=<) :: (b -> Exp c) -> (a -> Exp b) -> a -> Exp c
- type LiftM = (=<<)
- data LiftM2 :: (a -> b -> Exp c) -> Exp a -> Exp b -> Exp c
- data LiftM3 :: (a -> b -> c -> Exp d) -> Exp a -> Exp b -> Exp c -> Exp d
- data Join :: Exp (Exp a) -> Exp a
- data (<$>) :: (a -> b) -> Exp a -> Exp b
- data (<*>) :: Exp (a -> b) -> Exp a -> Exp b
- data Flip :: (a -> b -> Exp c) -> b -> a -> Exp c
- data ConstFn :: a -> b -> Exp a
- data ($) :: (a -> Exp b) -> a -> Exp b
- data Uncurry :: (a -> b -> Exp c) -> (a, b) -> Exp c
- data Fst :: (a, b) -> Exp a
- data Snd :: (a, b) -> Exp b
- data (***) :: (b -> Exp c) -> (b' -> Exp c') -> (b, b') -> Exp (c, c')
- data UnEither :: (a -> Exp c) -> (b -> Exp c) -> Either a b -> Exp c
- data IsLeft :: Either a b -> Exp Bool
- data IsRight :: Either a b -> Exp Bool
- data UnMaybe :: Exp b -> (a -> Exp b) -> Maybe a -> Exp b
- data FromMaybe :: k -> Maybe k -> Exp k
- data IsNothing :: Maybe a -> Exp Bool
- data IsJust :: Maybe a -> Exp Bool
- data Foldr :: (a -> b -> Exp b) -> b -> t a -> Exp b
- data UnList :: b -> (a -> b -> Exp b) -> [a] -> Exp b
- data (++) :: [a] -> [a] -> Exp [a]
- data Filter :: (a -> Exp Bool) -> [a] -> Exp [a]
- data Head :: [a] -> Exp (Maybe a)
- data Tail :: [a] -> Exp (Maybe [a])
- data Null :: [a] -> Exp Bool
- data Length :: [a] -> Exp Nat
- data Find :: (a -> Exp Bool) -> [a] -> Exp (Maybe a)
- data FindIndex :: (a -> Exp Bool) -> [a] -> Exp (Maybe Nat)
- data Lookup :: k -> [(k, b)] -> Exp (Maybe b)
- data SetIndex :: Nat -> a -> [a] -> Exp [a]
- data ZipWith :: (a -> b -> Exp c) -> [a] -> [b] -> Exp [c]
- data Zip :: [a] -> [b] -> Exp [(a, b)]
- data Unzip :: Exp [(a, b)] -> Exp ([a], [b])
- data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])
- data UnBool :: Exp a -> Exp a -> Bool -> Exp a
- data (||) :: Bool -> Bool -> Exp Bool
- data (&&) :: Bool -> Bool -> Exp Bool
- data Not :: Bool -> Exp Bool
- data Case :: [Match j k] -> j -> Exp 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 (+) :: Nat -> Nat -> Exp Nat
- data (-) :: Nat -> Nat -> Exp Nat
- data * :: Nat -> Nat -> Exp Nat
- data (^) :: Nat -> Nat -> Exp Nat
- data (<=) :: Nat -> Nat -> Exp Bool
- data (>=) :: Nat -> Nat -> Exp Bool
- data (<) :: Nat -> Nat -> Exp Bool
- data (>) :: Nat -> Nat -> Exp Bool
- data Map :: (a -> Exp b) -> f a -> Exp (f b)
- data Bimap :: (a -> Exp a') -> (b -> Exp b') -> f a b -> Exp (f a' b')
- data Error :: Symbol -> Exp a
- data Constraints :: [Constraint] -> Exp Constraint
- data TyEq :: a -> b -> Exp 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 ...

# 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 a b :: Ordering -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare a b :: Ordering -> Type) = 'EQ
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 '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 a b :: Ordering -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare a b :: Ordering -> Type) = CmpSymbol a b
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 ('[] :: [k]) (_y ': _ys) :: Ordering -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare ('[] :: [k]) (_y ': _ys) :: Ordering -> Type) = 'LT
type Eval (Compare ('[] :: [k]) ('[] :: [k]) :: Ordering -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare ('[] :: [k]) ('[] :: [k]) :: Ordering -> Type) = 'EQ
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 (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 (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 (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 (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 (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 (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 x = Eval (f x) Source #

Apply and evaluate a unary type function.

## Functional combinators

data Pure :: a -> Exp 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 :: (a -> b) -> a -> Exp 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 :: (a -> b -> c) -> a -> b -> Exp 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 :: (a -> b -> c -> d) -> a -> b -> c -> Exp 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 (=<<) :: (a -> Exp b) -> Exp a -> Exp 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 (<=<) :: (b -> Exp c) -> (a -> Exp b) -> a -> Exp 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 = (=<<) Source #

data LiftM2 :: (a -> b -> Exp c) -> Exp a -> Exp b -> Exp 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 :: (a -> b -> c -> Exp d) -> Exp a -> Exp b -> Exp c -> Exp 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 :: Exp (Exp a) -> Exp 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 (<$>) :: (a -> b) -> Exp a -> Exp 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 (<*>) :: Exp (a -> b) -> Exp a -> Exp 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 :: (a -> b -> Exp c) -> b -> a -> Exp 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 :: a -> b -> Exp 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 ($) :: (a -> Exp b) -> a -> Exp 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 :: (a -> b -> Exp c) -> (a, b) -> Exp 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 :: (a, b) -> Exp 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 :: (a, b) -> Exp 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 (***) :: (b -> Exp c) -> (b' -> Exp c') -> (b, b') -> Exp (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 :: (a -> Exp c) -> (b -> Exp c) -> Either a b -> Exp 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 :: Either a b -> Exp 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 :: Either a b -> Exp 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 :: Exp b -> (a -> Exp b) -> Maybe a -> Exp 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 :: k -> Maybe k -> Exp 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 :: Maybe a -> Exp 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 :: Maybe a -> Exp 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 Foldr :: (a -> b -> Exp b) -> b -> t a -> Exp b Source #

Right fold.

### Example

Expand

    >>> :kind! Eval (Foldr (+) 0 '[1, 2, 3, 4])
    Eval (Foldr (+) 0 '[1, 2, 3, 4]) :: Nat
    = 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 :: b -> (a -> b -> Exp b) -> [a] -> Exp 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 (++) :: [a] -> [a] -> Exp [a] Source #

List catenation.

### Example

Expand

    >>> :kind! Eval ('[1, 2] ++ '[3, 4])
    Eval ('[1, 2] ++ '[3, 4]) :: [Nat]
    = '[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 Filter :: (a -> Exp Bool) -> [a] -> Exp [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]) :: [Nat]
    = '[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 Head :: [a] -> Exp (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 Tail :: [a] -> Exp (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 Null :: [a] -> Exp 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 :: [a] -> Exp 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 Find :: (a -> Exp Bool) -> [a] -> Exp (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 Nat
    = 'Nothing

    >>> :kind! Eval (Find (TyEq 0) '[1,2,3,0])
    Eval (Find (TyEq 0) '[1,2,3,0]) :: Maybe Nat
    = '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 FindIndex :: (a -> Exp Bool) -> [a] -> Exp (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 Nat
    = 'Just 2

    >>> :kind! Eval (FindIndex ((>) 0) '[1,2,3,1,2,3])
    Eval (FindIndex ((>) 0) '[1,2,3,1,2,3]) :: Maybe Nat
    = '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 Lookup :: k -> [(k, b)] -> Exp (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 SetIndex :: Nat -> a -> [a] -> Exp [a] Source #

Modify an element at a given index.

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

### Example

Expand

    >>> :kind! Eval (SetIndex 2 7 '[1,2,3])
    Eval (SetIndex 2 7 '[1,2,3]) :: [Nat]
    = '[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 :: (a -> b -> Exp c) -> [a] -> [b] -> Exp [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]) :: [Nat]
    = '[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 :: [a] -> [b] -> Exp [(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 :: Exp [(a, b)] -> Exp ([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))

data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([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)

## Bool

data UnBool :: Exp a -> Exp a -> Bool -> Exp 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 (||) :: Bool -> Bool -> Exp 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 (&&) :: Bool -> Bool -> Exp 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 :: Bool -> Exp 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 :: [Match j k] -> j -> Exp 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 (+) :: Nat -> Nat -> Exp 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 (-) :: Nat -> Nat -> Exp 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 * :: Nat -> Nat -> Exp 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 (^) :: Nat -> Nat -> Exp 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 (<=) :: Nat -> Nat -> Exp 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 (>=) :: Nat -> Nat -> Exp 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 (<) :: Nat -> Nat -> Exp 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 (>) :: Nat -> Nat -> Exp 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 :: (a -> Exp b) -> f a -> Exp (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 AddMul :: Nat -> Nat -> Exp Nat
    >>> type instance Eval (AddMul x y) = (x TL.+ y) TL.* (x TL.+ y)
    >>> :kind! Eval (Map (AddMul 2) '[0, 1, 2, 3, 4])
    Eval (Map (AddMul 2) '[0, 1, 2, 3, 4]) :: [Nat]
    = '[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 :: (a -> Exp a') -> (b -> Exp b') -> f a b -> Exp (f a' b') Source #

Type-level `bimap`.

    >>> :kind! Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4))
    Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Nat, Nat)
    = '(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 :: Symbol -> Exp 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 :: [Constraint] -> Exp Constraint 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 :: a -> b -> Exp 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 ... Source #

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 |