-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/

-- | First-class type families
--   
--   A library for type-level programming.
--   
--   See README.
@package first-class-families
@version 0.8.0.1

-- | The Eval family.
module Fcf.Core

-- | Kind of type-level expressions indexed by their result type.
type Exp a = a -> Type

-- | Expression evaluator.
type family Eval (e :: Exp a) :: a

-- | Apply and evaluate a unary type function.
type f @@ x = Eval (f x)

-- | General fcf combinators.
--   
--   See also Fcf.Data.Function for more.
module Fcf.Combinators
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
infixr 1 =<<
data (<=<) :: (b -> Exp c) -> (a -> Exp b) -> a -> Exp c
infixr 1 <=<
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
infixl 4 <$>
data (<*>) :: Exp (a -> b) -> Exp a -> Exp b
infixl 4 <*>
data Flip :: (a -> b -> Exp c) -> b -> a -> Exp c
data ConstFn :: a -> b -> Exp a

-- | Note that this denotes the identity function, so ($) f can
--   usually be replaced with f.
data ($) :: (a -> Exp b) -> a -> Exp b
infixr 0 $

-- | Semigroups and monoids.
module Fcf.Class.Monoid

-- | Type-level semigroup composition (<>).
type family (<>) (x :: a) (y :: a) :: a

-- | Type-level monoid identity mempty.
--   
--   
Examples
--   
--   
--   >>> :kind! 'LT <> MEmpty
--   'LT <> MEmpty :: Ordering
--   = 'LT
--   
--   
--   
--   >>> :kind! MEmpty <> '( 'EQ, '[1, 2])
--   MEmpty <> '( 'EQ, '[1, 2]) :: (Ordering, [Nat])
--   = '( 'EQ, '[1, 2])
--   
--   
--   
--   >>> :kind! '( 'GT, 'Just '()) <> MEmpty
--   '( 'GT, 'Just '()) <> MEmpty :: (Ordering, Maybe ())
--   = '( 'GT, 'Just '())
--   
type family MEmpty :: a

-- | Type-level semigroup composition (<>).
--   
--   This is the fcf-encoding of (<>). To define a
--   new semigroup, add type instances to (<>).
data (.<>) :: a -> a -> Exp a

-- | Type-level monoid identity mempty.
--   
--   This is the fcf-encoding of MEmpty.
data MEmpty_ :: Exp a

-- | Carriers of useful monoid instances.
module Fcf.Class.Monoid.Types

-- | Endofunctions.
--   
--   
Details
--   
--   This is is used in the default implementation of Foldr in terms
--   of FoldMap.
newtype Endo a
Endo :: (a -> Exp a) -> Endo a

-- | Inverse of the Endo constructor.
type family UnEndo (e :: Endo a) :: a -> Exp a

module Fcf.Class.Functor

-- | 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
--   
--   
--   >>> 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]
--   
data Map :: (a -> Exp b) -> f a -> Exp (f b)

-- | Synonym of Map to avoid name clashes.
type FMap = Map

-- | Bifunctors.
--   
--   Bifunctors are "two-argument functors".
--   
--   This module is the type-level equivalent of Data.Bifunctor.
module Fcf.Class.Bifunctor

-- | Type-level bimap.
--   
--   
--   >>> :kind! Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4))
--   Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Nat, Nat)
--   = '(3, 3)
--   
data Bimap :: (a -> Exp a') -> (b -> Exp b') -> f a b -> Exp (f a' b')

-- | Type-level first. Apply a function along the first parameter of
--   a bifunctor.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (First ((+) 1) '(3,"a"))
--   Eval (First ((+) 1) '(3,"a")) :: (Nat, Symbol)
--   = '(4, "a")
--   
data First :: (a -> Exp b) -> f a c -> Exp (f b c)

-- | Type-level second. Apply a function along the second parameter
--   of a bifunctor.
--   
--   This is generally equivalent to Map.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Second ((+) 1) '("a",3))
--   Eval (Second ((+) 1) '("a",3)) :: (Symbol, Nat)
--   = '("a", 4)
--   
data Second :: (c -> Exp d) -> f a c -> Exp (f a d)

-- | Overloaded functions.

-- | Deprecated: Use Fcf.Class.Functor or Fcf.Class.Bifunctor
--   instead.
module Fcf.Classes

-- | 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
--   
--   
--   >>> 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]
--   
data Map :: (a -> Exp b) -> f a -> Exp (f b)

-- | Type-level bimap.
--   
--   
--   >>> :kind! Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4))
--   Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Nat, Nat)
--   = '(3, 3)
--   
data Bimap :: (a -> Exp a') -> (b -> Exp b') -> f a b -> Exp (f a' b')

-- | Booleans.
--   
--   Note that the operations from this module conflict with
--   Data.Type.Bool.
module Fcf.Data.Bool

-- | 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
--   
data UnBool :: Exp a -> Exp a -> Bool -> Exp a
data (||) :: Bool -> Bool -> Exp Bool
infixr 2 ||
data (&&) :: Bool -> Bool -> Exp Bool
infixr 3 &&
data Not :: Bool -> Exp Bool

-- | Common data types: tuples, Either, Maybe.
module Fcf.Data.Common
data Uncurry :: (a -> b -> Exp c) -> (a, b) -> Exp c
data Fst :: (a, b) -> Exp a
data Snd :: (a, b) -> Exp b

-- | Specialization of Bimap for pairs.
data (***) :: (b -> Exp c) -> (b' -> Exp c') -> (b, b') -> Exp (c, c')
infixr 3 ***
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

-- | Simple combinators for functions.
module Fcf.Data.Function

-- | Reverse function application, argument first.
--   
--   
Example
--   
--   
--   >>> :kind! Eval ('( 'True, 'Nothing) & Fst)
--   Eval ('( 'True, 'Nothing) & Fst) :: Bool
--   = 'True
--   
data (&) :: a -> (a -> Exp b) -> Exp b
infixl 1 &

-- | Lift a binary function to the domain of a projection.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (((&&) `On` Fst) '( 'True, 'Nothing) '( 'False, 'Just '()))
--   Eval (((&&) `On` Fst) '( 'True, 'Nothing) '( 'False, 'Just '())) :: Bool
--   = 'False
--   
data On :: (b -> b -> Exp c) -> (a -> Exp b) -> a -> a -> Exp c

-- | Pre-compose a binary function with a function for each argument.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Bicomap Fst Pure (||) '( 'False, 'Nothing) 'True)
--   Eval (Bicomap Fst Pure (||) '( 'False, 'Nothing) 'True) :: Bool
--   = 'True
--   
data Bicomap :: (a -> Exp c) -> (b -> Exp d) -> (c -> d -> Exp e) -> a -> b -> Exp e

-- | Natural numbers.
--   
--   Note that the operators from this module conflict with
--   GHC.TypeLits and GHC.TypeNats.
module Fcf.Data.Nat

-- | A type synonym for Natural.
--   
--   Prevously, this was an opaque data type, but it was changed to a type
--   synonym.
type Nat = Natural
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

-- | Foldable types.
--   
--   A minimal implementation of this interface is given by either
--   FoldMap or Foldr, but a default still needs to be given
--   explicitly for the other.
--   
--   
--   data MyType a = ... {- Some custom Foldable type -}
--   
--   -- Method 1: Implement Foldr, default FoldMap.
--   type instance Eval (Foldr f y xs) = ... {- Explicit implementation -}
--   type instance Eval (FoldMap f xs) = FoldMapDefault_ f xs {- Default -}
--   
--   -- Method 2: Implement FoldMap, default Foldr.
--   type instance Eval (FoldMap f xs) = ... {- Explicit implementation -}
--   type instance Eval (Foldr f y xs) = FoldrDefault_ f y xs {- Default -}
--   
module Fcf.Class.Foldable

-- | Right fold.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Foldr (+) 0 '[1, 2, 3, 4])
--   Eval (Foldr (+) 0 '[1, 2, 3, 4]) :: Nat
--   = 10
--   
data Foldr :: (a -> b -> Exp b) -> b -> t a -> Exp b

-- | Type-level foldMap.
data FoldMap :: (a -> Exp m) -> t a -> Exp m

-- | Default implementation of FoldMap.
--   
--   
Usage
--   
--   To define an instance of FoldMap for a custom MyType
--   for which you already have an instance of Foldr:
--   
--   
--   type instance Eval (FoldMap f (xs :: MyType a)) = FoldMapDefault_ f xs
--   
--   
--   
Example
--   
--   
--   >>> :kind! FoldMapDefault_ Pure '[ 'EQ, 'LT, 'GT ]
--   FoldMapDefault_ Pure '[ 'EQ, 'LT, 'GT ] :: Ordering
--   = 'LT
--   
type FoldMapDefault_ f xs = Eval (Foldr (Bicomap f Pure (.<>)) MEmpty xs)

-- | Default implementation of Foldr.
--   
--   
Usage
--   
--   To define an instance of Foldr for a custom MyType for
--   which you already have an instance of FoldMap:
--   
--   
--   type instance Eval (Foldr f y (xs :: MyType a)) = FoldrDefault_ f y xs
--   
--   
--   
Example
--   
--   
--   >>> :kind! FoldrDefault_ (.<>) 'EQ '[ 'EQ, 'LT, 'GT ]
--   FoldrDefault_ (.<>) 'EQ '[ 'EQ, 'LT, 'GT ] :: Ordering
--   = 'LT
--   
type FoldrDefault_ f y xs = Eval (UnEndo (Eval (FoldMap (Pure1 'Endo <=< Pure1 f) xs)) y)

-- | Give True if all of the booleans in the list are
--   True.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (And '[ 'True, 'True])
--   Eval (And '[ 'True, 'True]) :: Bool
--   = 'True
--   
--   
--   
--   >>> :kind! Eval (And '[ 'True, 'True, 'False])
--   Eval (And '[ 'True, 'True, 'False]) :: Bool
--   = 'False
--   
data And :: t Bool -> Exp Bool

-- | Give True if any of the booleans in the list are
--   True.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Or '[ 'True, 'True])
--   Eval (Or '[ 'True, 'True]) :: Bool
--   = 'True
--   
--   
--   
--   >>> :kind! Eval (Or '[ 'False, 'False])
--   Eval (Or '[ 'False, 'False]) :: Bool
--   = 'False
--   
data Or :: t Bool -> Exp Bool

-- | Whether all elements of the list satisfy a predicate.
--   
--   Note: this identifier conflicts with All (from
--   Data.Monoid).
--   
--   
Example
--   
--   
--   >>> :kind! Eval (All (Flip (<) 6) '[0,1,2,3,4,5])
--   Eval (All (Flip (<) 6) '[0,1,2,3,4,5]) :: Bool
--   = 'True
--   
--   
--   
--   >>> :kind! Eval (All (Flip (<) 5) '[0,1,2,3,4,5])
--   Eval (All (Flip (<) 5) '[0,1,2,3,4,5]) :: Bool
--   = 'False
--   
data All :: (a -> Exp Bool) -> t a -> Exp Bool

-- | Whether any element of the list satisfies a predicate.
--   
--   Note: this identifier conflicts with Any (from
--   Fcf.Utils), Any (from Data.Monoid), and
--   Any (from GHC.Exts).
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Any (Flip (<) 5) '[0,1,2,3,4,5])
--   Eval (Any (Flip (<) 5) '[0,1,2,3,4,5]) :: Bool
--   = 'True
--   
--   
--   
--   >>> :kind! Eval (Any (Flip (<) 0) '[0,1,2,3,4,5])
--   Eval (Any (Flip (<) 0) '[0,1,2,3,4,5]) :: Bool
--   = 'False
--   
data Any :: (a -> Exp Bool) -> t a -> Exp Bool

-- | Sum a Nat-list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Sum '[1,2,3])
--   Eval (Sum '[1,2,3]) :: Nat
--   = 6
--   
data Sum :: t Nat -> Exp Nat

-- | Concatenate a collection of elements from a monoid.
--   
--   
Example
--   
--   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]])) :: [Nat]
--   = '[1, 2, 3, 4, 5, 6]
--   
--   >>> :kind! Eval (Concat ( '[ '[Int, Maybe Int], '[Maybe String, Either Double Int]]))
--   Eval (Concat ( '[ '[Int, Maybe Int], '[Maybe String, Either Double Int]])) :: [*]
--   = '[Int, Maybe Int, Maybe String, Either Double Int]
--   
data Concat :: t m -> Exp m

-- | Map a function and concatenate the results.
--   
--   This is FoldMap specialized to the list monoid.
data ConcatMap :: (a -> Exp [b]) -> t a -> Exp [b]

-- | 
Symbols
--   
--   Type-level strings.
--   
--   Note that the operators from this module conflict with
--   GHC.TypeLits.
--   
--   Symbol also has instances of (<>) and
--   MEmpty.
module Fcf.Data.Symbol

-- | (Kind) This is the kind of type-level symbols. Declared here because
--   class IP needs it
data () => Symbol

-- | Miscellaneous families.
module Fcf.Utils

-- | Type-level error.
data Error :: Symbol -> Exp a

-- | TypeError as a fcf.
data TError :: ErrorMessage -> Exp a

-- | Conjunction of a list of constraints.
data Constraints :: [Constraint] -> Exp Constraint

-- | Type equality.
--   
--   
Details
--   
--   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.
--   
data TyEq :: a -> b -> Exp Bool

-- | A stuck type that can be used like a type-level undefined.
type family Stuck :: a
class IsBool (b :: Bool)
_If :: IsBool b => (b ~ 'True => r) -> (b ~ 'False => r) -> r

-- | (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)
--     ]
--   
data Case :: [Match j k] -> j -> Exp k
data Match j k

-- | Match concrete type in Case.
type (-->) = ('Match_ :: j -> k -> Match j k)
infix 0 -->

-- | Match on predicate being successful with type in Case.
type Is = ('Is_ :: (j -> Exp Bool) -> k -> Match j k)

-- | 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 Any = ('Any_ :: k -> Match j k)

-- | Pass type being matched in Case to subcomputation. Should be
--   used as a final branch.
type Else = ('Else_ :: (j -> Exp k) -> Match j k)

-- | Type-level If. If True a b ==> a; If
--   False a b ==> b
type family If (cond :: Bool) (tru :: k) (fls :: k) :: k
instance Fcf.Utils.IsBool 'GHC.Types.True
instance Fcf.Utils.IsBool 'GHC.Types.False

-- | Lists.
--   
--   See also Fcf.Class.Foldable for additional functions.
module Fcf.Data.List

-- | List catenation.
--   
--   
Example
--   
--   
--   >>> :kind! Eval ('[1, 2] ++ '[3, 4])
--   Eval ('[1, 2] ++ '[3, 4]) :: [Nat]
--   = '[1, 2, 3, 4]
--   
data (++) :: [a] -> [a] -> Exp [a]
data Head :: [a] -> Exp (Maybe a)
data Last :: [a] -> Exp (Maybe a)
data Tail :: [a] -> Exp (Maybe [a])

-- | Append an element to a list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Cons 1 '[2, 3])
--   Eval (Cons 1 '[2, 3]) :: [Nat]
--   = '[1, 2, 3]
--   
--   >>> :kind! Eval (Cons Int '[Char, Maybe Double])
--   Eval (Cons Int '[Char, Maybe Double]) :: [*]
--   = '[Int, Char, Maybe Double]
--   
data Cons :: a -> [a] -> Exp [a]

-- | Append an element to the end of a list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Snoc '[1,2,3] 4)
--   Eval (Snoc '[1,2,3] 4) :: [Nat]
--   = '[1, 2, 3, 4]
--   
data Snoc :: [a] -> a -> Exp [a]

-- | Append elements to two lists. Used in the definition of Unzip.
data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])
data Init :: [a] -> Exp (Maybe [a])
data Null :: [a] -> Exp Bool
data Length :: [a] -> Exp Nat

-- | Reverse a list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Reverse '[1,2,3,4,5])
--   Eval (Reverse '[1,2,3,4,5]) :: [Nat]
--   = '[5, 4, 3, 2, 1]
--   
data Reverse :: [a] -> Exp [a]

-- | Intersperse a separator between elements of a list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Intersperse 0 '[1,2,3,4])
--   Eval (Intersperse 0 '[1,2,3,4]) :: [Nat]
--   = '[1, 0, 2, 0, 3, 0, 4]
--   
data Intersperse :: a -> [a] -> Exp [a]

-- | Join a list of words separated by some word.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Intercalate '[", "] '[ '["Lorem"], '["ipsum"], '["dolor"] ])
--   Eval (Intercalate '[", "] '[ '["Lorem"], '["ipsum"], '["dolor"] ]) :: [TL.Symbol]
--   = '["Lorem", ", ", "ipsum", ", ", "dolor"]
--   
data Intercalate :: [a] -> [[a]] -> Exp [a]

-- | Right fold.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Foldr (+) 0 '[1, 2, 3, 4])
--   Eval (Foldr (+) 0 '[1, 2, 3, 4]) :: Nat
--   = 10
--   
data Foldr :: (a -> b -> Exp b) -> b -> t a -> Exp b

-- | This is Foldr with its argument flipped.
data UnList :: b -> (a -> b -> Exp b) -> [a] -> Exp b

-- | Concatenate a collection of elements from a monoid.
--   
--   
Example
--   
--   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]])) :: [Nat]
--   = '[1, 2, 3, 4, 5, 6]
--   
--   >>> :kind! Eval (Concat ( '[ '[Int, Maybe Int], '[Maybe String, Either Double Int]]))
--   Eval (Concat ( '[ '[Int, Maybe Int], '[Maybe String, Either Double Int]])) :: [*]
--   = '[Int, Maybe Int, Maybe String, Either Double Int]
--   
data Concat :: t m -> Exp m

-- | Map a function and concatenate the results.
--   
--   This is FoldMap specialized to the list monoid.
data ConcatMap :: (a -> Exp [b]) -> t a -> Exp [b]

-- | Unfold a generator into a list.
--   
--   
Example
--   
--   
--   >>> data ToThree :: Nat -> Exp (Maybe (Nat, Nat))
--   
--   >>> :{
--   type instance Eval (ToThree b) =
--     If (Eval (b Fcf.>= 4))
--       'Nothing
--       ('Just '(b, b TL.+ 1))
--   :}
--   
--   
--   
--   >>> :kind! Eval (Unfoldr ToThree 0)
--   Eval (Unfoldr ToThree 0) :: [Nat]
--   = '[0, 1, 2, 3]
--   
--   
--   See also the definition of Replicate.
data Unfoldr :: (b -> Exp (Maybe (a, b))) -> b -> Exp [a]

-- | Repeat the same element in a list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Replicate 4 '("ok", 2))
--   Eval (Replicate 4 '("ok", 2)) :: [(TL.Symbol, Nat)]
--   = '[ '("ok", 2), '("ok", 2), '("ok", 2), '("ok", 2)]
--   
data Replicate :: Nat -> a -> Exp [a]

-- | Take a prefix of fixed length.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Take 2 '[1,2,3,4,5])
--   Eval (Take 2 '[1,2,3,4,5]) :: [Nat]
--   = '[1, 2]
--   
data Take :: Nat -> [a] -> Exp [a]

-- | Drop a prefix of fixed length, evaluate to the remaining suffix.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Drop 2 '[1,2,3,4,5])
--   Eval (Drop 2 '[1,2,3,4,5]) :: [Nat]
--   = '[3, 4, 5]
--   
data Drop :: Nat -> [a] -> Exp [a]

-- | Take the longest prefix of elements satisfying a predicate.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (TakeWhile ((>=) 3) '[1, 2, 3, 4, 5])
--   Eval (TakeWhile ((>=) 3) '[1, 2, 3, 4, 5]) :: [Nat]
--   = '[1, 2, 3]
--   
data TakeWhile :: (a -> Exp Bool) -> [a] -> Exp [a]

-- | Drop the longest prefix of elements satisfying a predicate, evaluate
--   to the remaining suffix.
--   
--   
Example
--   
--   :kind! Eval (DropWhile ((>=) 3) '[1, 2, 3, 4, 5]) Eval (DropWhile
--   ((>=) 3) '[1, 2, 3, 4, 5]) :: [Nat] = '[4, 5]
data DropWhile :: (a -> Exp Bool) -> [a] -> Exp [a]

-- | 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
--   
--   
--   >>> :kind! Eval (Span (Flip (<) 3) '[1,2,3,4,1,2,3,4])
--   Eval (Span (Flip (<) 3) '[1,2,3,4,1,2,3,4]) :: ([Nat], [Nat])
--   = '( '[1, 2], '[3, 4, 1, 2, 3, 4])
--   
--   
--   
--   >>> :kind! Eval (Span (Flip (<) 9) '[1,2,3])
--   Eval (Span (Flip (<) 9) '[1,2,3]) :: ([Nat], [Nat])
--   = '( '[1, 2, 3], '[])
--   
--   
--   
--   >>> :kind! Eval (Span (Flip (<) 0) '[1,2,3])
--   Eval (Span (Flip (<) 0) '[1,2,3]) :: ([Nat], [Nat])
--   = '( '[], '[1, 2, 3])
--   
data Span :: (a -> Exp Bool) -> [a] -> Exp ([a], [a])

-- | 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
--   
--   
--   >>> :kind! Eval (Break (Flip (>) 3) '[1,2,3,4,1,2,3,4])
--   Eval (Break (Flip (>) 3) '[1,2,3,4,1,2,3,4]) :: ([Nat], [Nat])
--   = '( '[1, 2, 3], '[4, 1, 2, 3, 4])
--   
--   
--   
--   >>> :kind! Eval (Break (Flip (<) 9) '[1,2,3])
--   Eval (Break (Flip (<) 9) '[1,2,3]) :: ([Nat], [Nat])
--   = '( '[], '[1, 2, 3])
--   
--   
--   
--   >>> :kind! Eval (Break (Flip (>) 9) '[1,2,3])
--   Eval (Break (Flip (>) 9) '[1,2,3]) :: ([Nat], [Nat])
--   = '( '[1, 2, 3], '[])
--   
data Break :: (a -> Exp Bool) -> [a] -> Exp ([a], [a])

-- | List of suffixes of a list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Tails '[0,1,2,3])
--   Eval (Tails '[0,1,2,3]) :: [[Nat]]
--   = '[ '[0, 1, 2, 3], '[1, 2, 3], '[2, 3], '[3]]
--   
data Tails :: [a] -> Exp [[a]]

-- | Return True when the first list is a prefix of the second.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (IsPrefixOf '[0,1,2] '[0,1,2,3,4,5])
--   Eval (IsPrefixOf '[0,1,2] '[0,1,2,3,4,5]) :: Bool
--   = 'True
--   
--   
--   
--   >>> :kind! Eval (IsPrefixOf '[0,1,2] '[0,1,3,2,4,5])
--   Eval (IsPrefixOf '[0,1,2] '[0,1,3,2,4,5]) :: Bool
--   = 'False
--   
--   
--   
--   >>> :kind! Eval (IsPrefixOf '[] '[0,1,3,2,4,5])
--   Eval (IsPrefixOf '[] '[0,1,3,2,4,5]) :: Bool
--   = 'True
--   
--   
--   
--   >>> :kind! Eval (IsPrefixOf '[0,1,3,2,4,5] '[])
--   Eval (IsPrefixOf '[0,1,3,2,4,5] '[]) :: Bool
--   = 'False
--   
data IsPrefixOf :: [a] -> [a] -> Exp Bool

-- | Return True when the first list is a suffix of the second.
--   
--   
Example
--   
--   
--   >>> :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
--   
data IsSuffixOf :: [a] -> [a] -> Exp Bool

-- | Return True when the first list is contained within the
--   second.
--   
--   
Example
--   
--   
--   >>> :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
--   
data IsInfixOf :: [a] -> [a] -> Exp Bool

-- | Return True if an element is in a list.
--   
--   See also FindIndex.
--   
--   
Example
--   
--   
--   >>> :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
--   
data Elem :: a -> [a] -> Exp Bool

-- | Find an element associated with a key in an association list.
data Lookup :: k -> [(k, b)] -> Exp (Maybe b)

-- | Find Just the first element satisfying a predicate, or
--   evaluate to Nothing if no element satisfies the predicate.
--   
--   
Example
--   
--   
--   >>> :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
--   
data Find :: (a -> Exp Bool) -> [a] -> Exp (Maybe a)

-- | Keep all elements that satisfy a predicate, remove all that don't.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Filter ((>) 3) '[1,2,3,0])
--   Eval (Filter ((>) 3) '[1,2,3,0]) :: [Nat]
--   = '[1, 2, 0]
--   
data Filter :: (a -> Exp Bool) -> [a] -> Exp [a]

-- | Split a list into one where all elements satisfy a predicate, and a
--   second where no elements satisfy it.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Partition ((>=) 35) '[ 20, 30, 40, 50])
--   Eval (Partition ((>=) 35) '[ 20, 30, 40, 50]) :: ([Nat], [Nat])
--   = '( '[20, 30], '[40, 50])
--   
data Partition :: (a -> Exp Bool) -> [a] -> Exp ([a], [a])

-- | Find the index of an element satisfying the predicate.
--   
--   
Example
--   
--   
--   >>> :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
--   
data FindIndex :: (a -> Exp Bool) -> [a] -> Exp (Maybe Nat)

-- | Modify an element at a given index.
--   
--   The list is unchanged if the index is out of bounds.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (SetIndex 2 7 '[1,2,3])
--   Eval (SetIndex 2 7 '[1,2,3]) :: [Nat]
--   = '[1, 2, 7]
--   
data SetIndex :: Nat -> a -> [a] -> Exp [a]

-- | Combine elements of two lists pairwise.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (ZipWith (+) '[1,2,3] '[1,1,1])
--   Eval (ZipWith (+) '[1,2,3] '[1,1,1]) :: [Nat]
--   = '[2, 3, 4]
--   
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])

-- | Equality and ordering.
--   
--   Note that equality doesn't really require a class, it can be defined
--   uniformly as TyEq.
module Fcf.Class.Ord

-- | Type-level compare for totally ordered data types.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Compare "a" "b")
--   Eval (Compare "a" "b") :: Ordering
--   = 'LT
--   
--   
--   
--   >>> :kind! Eval (Compare '[1, 2, 3] '[1, 2, 3])
--   Eval (Compare '[1, 2, 3] '[1, 2, 3]) :: Ordering
--   = 'EQ
--   
--   
--   
--   >>> :kind! Eval (Compare '[1, 3] '[1, 2])
--   Eval (Compare '[1, 3] '[1, 2]) :: Ordering
--   = 'GT
--   
data Compare :: a -> a -> Exp Ordering

-- | "Smaller than or equal to". Type-level version of
--   (<=).
--   
--   
Example
--   
--   
--   >>> :kind! Eval ("b" <= "a")
--   Eval ("b" <= "a") :: Bool
--   = 'False
--   
data (<=) :: a -> a -> Exp Bool

-- | "Greater than or equal to". Type-level version of
--   (>=).
--   
--   
Example
--   
--   
--   >>> :kind! Eval ("b" >= "a")
--   Eval ("b" >= "a") :: Bool
--   = 'True
--   
data (>=) :: a -> a -> Exp Bool

-- | "Smaller than". Type-level version of (<).
--   
--   
Example
--   
--   
--   >>> :kind! Eval ("a" < "b")
--   Eval ("a" < "b") :: Bool
--   = 'True
--   
data (<) :: a -> a -> Exp Bool

-- | "Greater than". Type-level version of (>).
--   
--   
Example
--   
--   
--   >>> :kind! Eval ("b" > "a")
--   Eval ("b" > "a") :: Bool
--   = 'True
--   
data (>) :: a -> a -> Exp Bool

-- | Type equality.
--   
--   
Details
--   
--   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.
--   
data TyEq :: a -> b -> Exp Bool

-- | 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 #-}
--   
module Fcf

-- | Kind of type-level expressions indexed by their result type.
type Exp a = a -> Type

-- | Expression evaluator.
type family Eval (e :: Exp a) :: a

-- | Apply and evaluate a unary type function.
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
infixr 1 =<<
data (<=<) :: (b -> Exp c) -> (a -> Exp b) -> a -> Exp c
infixr 1 <=<
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
infixl 4 <$>
data (<*>) :: Exp (a -> b) -> Exp a -> Exp b
infixl 4 <*>
data Flip :: (a -> b -> Exp c) -> b -> a -> Exp c
data ConstFn :: a -> b -> Exp a

-- | Note that this denotes the identity function, so ($) f can
--   usually be replaced with f.
data ($) :: (a -> Exp b) -> a -> Exp b
infixr 0 $
data Uncurry :: (a -> b -> Exp c) -> (a, b) -> Exp c
data Fst :: (a, b) -> Exp a
data Snd :: (a, b) -> Exp b

-- | Specialization of Bimap for pairs.
data (***) :: (b -> Exp c) -> (b' -> Exp c') -> (b, b') -> Exp (c, c')
infixr 3 ***
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

-- | Right fold.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Foldr (+) 0 '[1, 2, 3, 4])
--   Eval (Foldr (+) 0 '[1, 2, 3, 4]) :: Nat
--   = 10
--   
data Foldr :: (a -> b -> Exp b) -> b -> t a -> Exp b

-- | This is Foldr with its argument flipped.
data UnList :: b -> (a -> b -> Exp b) -> [a] -> Exp b

-- | List catenation.
--   
--   
Example
--   
--   
--   >>> :kind! Eval ('[1, 2] ++ '[3, 4])
--   Eval ('[1, 2] ++ '[3, 4]) :: [Nat]
--   = '[1, 2, 3, 4]
--   
data (++) :: [a] -> [a] -> Exp [a]

-- | Keep all elements that satisfy a predicate, remove all that don't.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Filter ((>) 3) '[1,2,3,0])
--   Eval (Filter ((>) 3) '[1,2,3,0]) :: [Nat]
--   = '[1, 2, 0]
--   
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

-- | Find Just the first element satisfying a predicate, or
--   evaluate to Nothing if no element satisfies the predicate.
--   
--   
Example
--   
--   
--   >>> :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
--   
data Find :: (a -> Exp Bool) -> [a] -> Exp (Maybe a)

-- | Find the index of an element satisfying the predicate.
--   
--   
Example
--   
--   
--   >>> :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
--   
data FindIndex :: (a -> Exp Bool) -> [a] -> Exp (Maybe Nat)

-- | Find an element associated with a key in an association list.
data Lookup :: k -> [(k, b)] -> Exp (Maybe b)

-- | Modify an element at a given index.
--   
--   The list is unchanged if the index is out of bounds.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (SetIndex 2 7 '[1,2,3])
--   Eval (SetIndex 2 7 '[1,2,3]) :: [Nat]
--   = '[1, 2, 7]
--   
data SetIndex :: Nat -> a -> [a] -> Exp [a]

-- | Combine elements of two lists pairwise.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (ZipWith (+) '[1,2,3] '[1,1,1])
--   Eval (ZipWith (+) '[1,2,3] '[1,1,1]) :: [Nat]
--   = '[2, 3, 4]
--   
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])

-- | Append elements to two lists. Used in the definition of Unzip.
data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])

-- | 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
--   
data UnBool :: Exp a -> Exp a -> Bool -> Exp a
data (||) :: Bool -> Bool -> Exp Bool
infixr 2 ||
data (&&) :: Bool -> Bool -> Exp Bool
infixr 3 &&
data Not :: Bool -> Exp Bool

-- | (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)
--     ]
--   
data Case :: [Match j k] -> j -> Exp k
data Match j k

-- | Match concrete type in Case.
type (-->) = ('Match_ :: j -> k -> Match j k)
infix 0 -->

-- | Match on predicate being successful with type in Case.
type Is = ('Is_ :: (j -> Exp Bool) -> k -> Match j k)

-- | 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 Any = ('Any_ :: k -> Match j k)

-- | Pass type being matched in Case to subcomputation. Should be
--   used as a final branch.
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

-- | 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
--   
--   
--   >>> 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]
--   
data Map :: (a -> Exp b) -> f a -> Exp (f b)

-- | Type-level bimap.
--   
--   
--   >>> :kind! Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4))
--   Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Nat, Nat)
--   = '(3, 3)
--   
data Bimap :: (a -> Exp a') -> (b -> Exp b') -> f a b -> Exp (f a' b')

-- | Type-level error.
data Error :: Symbol -> Exp a

-- | Conjunction of a list of constraints.
data Constraints :: [Constraint] -> Exp Constraint

-- | Type equality.
--   
--   
Details
--   
--   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.
--   
data TyEq :: a -> b -> Exp Bool

-- | A stuck type that can be used like a type-level undefined.
type family Stuck :: a
class IsBool (b :: Bool)
_If :: IsBool b => (b ~ 'True => r) -> (b ~ 'False => r) -> r

-- | Type-level If. If True a b ==> a; If
--   False a b ==> b
type family If (cond :: Bool) (tru :: k) (fls :: k) :: k
