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


-- | First class type families
--   
--   First class type families, eval-style defunctionalization
--   
--   See <a>Fcf</a>.
@package first-class-families
@version 0.8.0.0


-- | The <a>Eval</a> 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 <a>Fcf.Data.Function</a> 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 <tt>($) f</tt> can
--   usually be replaced with <tt>f</tt>.
data ($) :: (a -> Exp b) -> a -> Exp b
infixr 0 $


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

-- | Type-level semigroup composition <tt>(<a>&lt;&gt;</a>)</tt>.
type family (<>) (x :: a) (y :: a) :: a

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

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

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


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

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

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

module Fcf.Class.Functor

-- | Type-level <a>fmap</a> for type-level functors.
--   
--   Note: this name clashes with <a>Map</a> from <i>containers</i>.
--   <a>FMap</a> is provided as a synonym to avoid this.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; import Fcf.Data.Nat
--   
--   &gt;&gt;&gt; import qualified GHC.TypeLits as TL
--   
--   &gt;&gt;&gt; data AddMul :: Nat -&gt; Nat -&gt; Exp Nat
--   
--   &gt;&gt;&gt; type instance Eval (AddMul x y) = (x TL.+ y) TL.* (x TL.+ y)
--   
--   &gt;&gt;&gt; :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]
--   </pre>
data Map :: (a -> Exp b) -> f a -> Exp (f b)

-- | Synonym of <a>Map</a> to avoid name clashes.
type FMap = Map


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

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

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

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


-- | Overloaded functions.

-- | <i>Deprecated: Use Fcf.Class.Functor or Fcf.Class.Bifunctor
--   instead.</i>
module Fcf.Classes

-- | Type-level <a>fmap</a> for type-level functors.
--   
--   Note: this name clashes with <a>Map</a> from <i>containers</i>.
--   <a>FMap</a> is provided as a synonym to avoid this.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; import Fcf.Data.Nat
--   
--   &gt;&gt;&gt; import qualified GHC.TypeLits as TL
--   
--   &gt;&gt;&gt; data AddMul :: Nat -&gt; Nat -&gt; Exp Nat
--   
--   &gt;&gt;&gt; type instance Eval (AddMul x y) = (x TL.+ y) TL.* (x TL.+ y)
--   
--   &gt;&gt;&gt; :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]
--   </pre>
data Map :: (a -> Exp b) -> f a -> Exp (f b)

-- | Type-level <a>bimap</a>.
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4))
--   Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Nat, Nat)
--   = '(3, 3)
--   </pre>
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
--   <a>Data.Type.Bool</a>.
module Fcf.Data.Bool

-- | N.B.: The order of the two branches is the opposite of "if":
--   <tt>UnBool ifFalse ifTrue bool</tt>.
--   
--   This mirrors the default order of constructors:
--   
--   <pre>
--   data Bool = False | True
--   ----------- False &lt; True
--   </pre>
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, <a>Either</a>, <a>Maybe</a>.
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 <a>Bimap</a> 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.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval ('( 'True, 'Nothing) &amp; Fst)
--   Eval ('( 'True, 'Nothing) &amp; Fst) :: Bool
--   = 'True
--   </pre>
data (&) :: a -> (a -> Exp b) -> Exp b
infixl 1 &

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

-- | Pre-compose a binary function with a function for each argument.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Bicomap Fst Pure (||) '( 'False, 'Nothing) 'True)
--   Eval (Bicomap Fst Pure (||) '( 'False, 'Nothing) 'True) :: Bool
--   = 'True
--   </pre>
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
--   <a>GHC.TypeLits</a> and <a>GHC.TypeNats</a>.
module Fcf.Data.Nat
data Nat
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
--   <a>FoldMap</a> or <a>Foldr</a>, but a default still needs to be given
--   explicitly for the other.
--   
--   <pre>
--   data MyType a = ... {- Some custom Foldable type -}
--   
--   -- Method 1: Implement Foldr, default FoldMap.
--   type instance <a>Eval</a> (<a>Foldr</a> f y xs) = ... {- Explicit implementation -}
--   type instance <a>Eval</a> (<a>FoldMap</a> f xs) = <a>FoldMapDefault_</a> f xs {- Default -}
--   
--   -- Method 2: Implement FoldMap, default Foldr.
--   type instance <a>Eval</a> (<a>FoldMap</a> f xs) = ... {- Explicit implementation -}
--   type instance <a>Eval</a> (<a>Foldr</a> f y xs) = <a>FoldrDefault_</a> f y xs {- Default -}
--   </pre>
module Fcf.Class.Foldable

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

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

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

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

-- | Give <tt>True</tt> if all of the booleans in the list are
--   <tt>True</tt>.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (And '[ 'True, 'True])
--   Eval (And '[ 'True, 'True]) :: Bool
--   = 'True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (And '[ 'True, 'True, 'False])
--   Eval (And '[ 'True, 'True, 'False]) :: Bool
--   = 'False
--   </pre>
data And :: t Bool -> Exp Bool

-- | Give <tt>True</tt> if any of the booleans in the list are
--   <tt>True</tt>.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Or '[ 'True, 'True])
--   Eval (Or '[ 'True, 'True]) :: Bool
--   = 'True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Or '[ 'False, 'False])
--   Eval (Or '[ 'False, 'False]) :: Bool
--   = 'False
--   </pre>
data Or :: t Bool -> Exp Bool

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

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

-- | Sum a <tt>Nat</tt>-list.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Sum '[1,2,3])
--   Eval (Sum '[1,2,3]) :: Nat
--   = 6
--   </pre>
data Sum :: t Nat -> Exp Nat

-- | Concatenate a collection of elements from a monoid.
--   
--   <h3><b>Example</b></h3>
--   
--   For example, fold a list of lists.
--   
--   <pre>
--   Concat :: [[a]] -&gt; Exp [a]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Concat ( '[ '[1,2], '[3,4], '[5,6]]))
--   Eval (Concat ( '[ '[1,2], '[3,4], '[5,6]])) :: [Nat]
--   = '[1, 2, 3, 4, 5, 6]
--   
--   &gt;&gt;&gt; :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]
--   </pre>
data Concat :: t m -> Exp m

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


-- | <h1>Symbols</h1>
--   
--   Type-level strings.
--   
--   Note that the operators from this module conflict with
--   <a>GHC.TypeLits</a>.
--   
--   <a>Symbol</a> also has instances of <tt>(<a>&lt;&gt;</a>)</tt> and
--   <a>MEmpty</a>.
module Fcf.Data.Symbol
data Symbol


-- | Miscellaneous families.
module Fcf.Utils

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

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

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

-- | Type equality.
--   
--   <h3><b>Details</b></h3>
--   
--   The base library also defines a similar <tt>(<a>==</a>)</tt>; it
--   differs from <a>TyEq</a> in the following ways:
--   
--   <ul>
--   <li><a>TyEq</a> is heterogeneous: its arguments may have different
--   kinds;</li>
--   <li><a>TyEq</a> is reflexive: <tt>TyEq a a</tt> always reduces to
--   <a>True</a> even if <tt>a</tt> is a variable.</li>
--   </ul>
data TyEq :: a -> b -> Exp Bool

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

-- | (Limited) equivalent of <tt>\case { .. }</tt> syntax. Supports
--   matching of exact values (<a>--&gt;</a>) and final matches for any
--   value (<a>Any</a>) or for passing value to subcomputation
--   (<a>Else</a>). Examples:
--   
--   <pre>
--   type BoolToNat = <a>Case</a>
--     [ 'True  <a>--&gt;</a> 0
--     , 'False <a>--&gt;</a> 1
--     ]
--   
--   type NatToBool = <a>Case</a>
--     [ 0 <a>--&gt;</a> 'False
--     , <a>Any</a>   'True
--     ]
--   
--   type ZeroOneOrSucc = <a>Case</a>
--     [ 0  <a>--&gt;</a> 0
--     , 1  <a>--&gt;</a> 1
--     , <a>Else</a>   ((<a>+</a>) 1)
--     ]
--   </pre>
data Case :: [Match j k] -> j -> Exp k
data Match j k

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

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

-- | Match any type in <a>Case</a>. Should be used as a final branch.
--   
--   Note: this identifier conflicts with <a>Any</a> (from
--   <a>Fcf.Class.Foldable</a>) <a>Any</a> (from <a>Data.Monoid</a>), and
--   <a>Any</a> (from <a>GHC.Exts</a>).
--   
--   We recommend importing this one qualified.
type Any = ('Any_ :: k -> Match j k)

-- | Pass type being matched in <a>Case</a> to subcomputation. Should be
--   used as a final branch.
type Else = ('Else_ :: (j -> Exp k) -> Match j k)
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 <a>Fcf.Class.Foldable</a> for additional functions.
module Fcf.Data.List

-- | List catenation.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval ('[1, 2] ++ '[3, 4])
--   Eval ('[1, 2] ++ '[3, 4]) :: [Nat]
--   = '[1, 2, 3, 4]
--   </pre>
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.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Cons 1 '[2, 3])
--   Eval (Cons 1 '[2, 3]) :: [Nat]
--   = '[1, 2, 3]
--   
--   &gt;&gt;&gt; :kind! Eval (Cons Int '[Char, Maybe Double])
--   Eval (Cons Int '[Char, Maybe Double]) :: [*]
--   = '[Int, Char, Maybe Double]
--   </pre>
data Cons :: a -> [a] -> Exp [a]

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

-- | Append elements to two lists. Used in the definition of <a>Unzip</a>.
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.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Reverse '[1,2,3,4,5])
--   Eval (Reverse '[1,2,3,4,5]) :: [Nat]
--   = '[5, 4, 3, 2, 1]
--   </pre>
data Reverse :: [a] -> Exp [a]

-- | Intersperse a separator between elements of a list.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Intersperse 0 '[1,2,3,4])
--   Eval (Intersperse 0 '[1,2,3,4]) :: [Nat]
--   = '[1, 0, 2, 0, 3, 0, 4]
--   </pre>
data Intersperse :: a -> [a] -> Exp [a]

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

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

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

-- | Concatenate a collection of elements from a monoid.
--   
--   <h3><b>Example</b></h3>
--   
--   For example, fold a list of lists.
--   
--   <pre>
--   Concat :: [[a]] -&gt; Exp [a]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Concat ( '[ '[1,2], '[3,4], '[5,6]]))
--   Eval (Concat ( '[ '[1,2], '[3,4], '[5,6]])) :: [Nat]
--   = '[1, 2, 3, 4, 5, 6]
--   
--   &gt;&gt;&gt; :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]
--   </pre>
data Concat :: t m -> Exp m

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

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

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

-- | Take a prefix of fixed length.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Take 2 '[1,2,3,4,5])
--   Eval (Take 2 '[1,2,3,4,5]) :: [Nat]
--   = '[1, 2]
--   </pre>
data Take :: Nat -> [a] -> Exp [a]

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

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

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

-- | <a>Span</a>, applied to a predicate <tt>p</tt> and a list <tt>xs</tt>,
--   returns a tuple: the first component is the longest prefix (possibly
--   empty) of <tt>xs</tt> whose elements satisfy <tt>p</tt>; the second
--   component is the remainder of the list.
--   
--   See also <a>TakeWhile</a>, <a>DropWhile</a>, and <a>Break</a>.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Span (Flip (&lt;) 3) '[1,2,3,4,1,2,3,4])
--   Eval (Span (Flip (&lt;) 3) '[1,2,3,4,1,2,3,4]) :: ([Nat], [Nat])
--   = '( '[1, 2], '[3, 4, 1, 2, 3, 4])
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Span (Flip (&lt;) 9) '[1,2,3])
--   Eval (Span (Flip (&lt;) 9) '[1,2,3]) :: ([Nat], [Nat])
--   = '( '[1, 2, 3], '[])
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Span (Flip (&lt;) 0) '[1,2,3])
--   Eval (Span (Flip (&lt;) 0) '[1,2,3]) :: ([Nat], [Nat])
--   = '( '[], '[1, 2, 3])
--   </pre>
data Span :: (a -> Exp Bool) -> [a] -> Exp ([a], [a])

-- | <a>Break</a>, applied to a predicate <tt>p</tt> and a list
--   <tt>xs</tt>, returns a tuple: the first component is the longest
--   prefix (possibly empty) of <tt>xs</tt> whose elements <i>do not
--   satisfy</i> <tt>p</tt>; the second component is the remainder of the
--   list.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Break (Flip (&gt;) 3) '[1,2,3,4,1,2,3,4])
--   Eval (Break (Flip (&gt;) 3) '[1,2,3,4,1,2,3,4]) :: ([Nat], [Nat])
--   = '( '[1, 2, 3], '[4, 1, 2, 3, 4])
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Break (Flip (&lt;) 9) '[1,2,3])
--   Eval (Break (Flip (&lt;) 9) '[1,2,3]) :: ([Nat], [Nat])
--   = '( '[], '[1, 2, 3])
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Break (Flip (&gt;) 9) '[1,2,3])
--   Eval (Break (Flip (&gt;) 9) '[1,2,3]) :: ([Nat], [Nat])
--   = '( '[1, 2, 3], '[])
--   </pre>
data Break :: (a -> Exp Bool) -> [a] -> Exp ([a], [a])

-- | List of suffixes of a list.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Tails '[0,1,2,3])
--   Eval (Tails '[0,1,2,3]) :: [[Nat]]
--   = '[ '[0, 1, 2, 3], '[1, 2, 3], '[2, 3], '[3]]
--   </pre>
data Tails :: [a] -> Exp [[a]]

-- | Return <tt>True</tt> when the first list is a prefix of the second.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :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
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :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
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (IsPrefixOf '[] '[0,1,3,2,4,5])
--   Eval (IsPrefixOf '[] '[0,1,3,2,4,5]) :: Bool
--   = 'True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (IsPrefixOf '[0,1,3,2,4,5] '[])
--   Eval (IsPrefixOf '[0,1,3,2,4,5] '[]) :: Bool
--   = 'False
--   </pre>
data IsPrefixOf :: [a] -> [a] -> Exp Bool

-- | Return <tt>True</tt> when the first list is a suffix of the second.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :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
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :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
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (IsSuffixOf '[] '[0,1,3,2,4,5])
--   Eval (IsSuffixOf '[] '[0,1,3,2,4,5]) :: Bool
--   = 'True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (IsSuffixOf '[0,1,3,2,4,5] '[])
--   Eval (IsSuffixOf '[0,1,3,2,4,5] '[]) :: Bool
--   = 'False
--   </pre>
data IsSuffixOf :: [a] -> [a] -> Exp Bool

-- | Return <tt>True</tt> when the first list is contained within the
--   second.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :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
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :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
--   </pre>
data IsInfixOf :: [a] -> [a] -> Exp Bool

-- | Return <tt>True</tt> if an element is in a list.
--   
--   See also <a>FindIndex</a>.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Elem 1 '[1,2,3])
--   Eval (Elem 1 '[1,2,3]) :: Bool
--   = 'True
--   
--   &gt;&gt;&gt; :kind! Eval (Elem 1 '[2,3])
--   Eval (Elem 1 '[2,3]) :: Bool
--   = 'False
--   </pre>
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 <tt>Just</tt> the first element satisfying a predicate, or
--   evaluate to <tt>Nothing</tt> if no element satisfies the predicate.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Find (TyEq 0) '[1,2,3])
--   Eval (Find (TyEq 0) '[1,2,3]) :: Maybe Nat
--   = 'Nothing
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Find (TyEq 0) '[1,2,3,0])
--   Eval (Find (TyEq 0) '[1,2,3,0]) :: Maybe Nat
--   = 'Just 0
--   </pre>
data Find :: (a -> Exp Bool) -> [a] -> Exp (Maybe a)

-- | Keep all elements that satisfy a predicate, remove all that don't.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Filter ((&gt;) 3) '[1,2,3,0])
--   Eval (Filter ((&gt;) 3) '[1,2,3,0]) :: [Nat]
--   = '[1, 2, 0]
--   </pre>
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.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Partition ((&gt;=) 35) '[ 20, 30, 40, 50])
--   Eval (Partition ((&gt;=) 35) '[ 20, 30, 40, 50]) :: ([Nat], [Nat])
--   = '( '[20, 30], '[40, 50])
--   </pre>
data Partition :: (a -> Exp Bool) -> [a] -> Exp ([a], [a])

-- | Find the index of an element satisfying the predicate.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (FindIndex ((&lt;=) 3) '[1,2,3,1,2,3])
--   Eval (FindIndex ((&lt;=) 3) '[1,2,3,1,2,3]) :: Maybe Nat
--   = 'Just 2
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (FindIndex ((&gt;) 0) '[1,2,3,1,2,3])
--   Eval (FindIndex ((&gt;) 0) '[1,2,3,1,2,3]) :: Maybe Nat
--   = 'Nothing
--   </pre>
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.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (SetIndex 2 7 '[1,2,3])
--   Eval (SetIndex 2 7 '[1,2,3]) :: [Nat]
--   = '[1, 2, 7]
--   </pre>
data SetIndex :: Nat -> a -> [a] -> Exp [a]

-- | Combine elements of two lists pairwise.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (ZipWith (+) '[1,2,3] '[1,1,1])
--   Eval (ZipWith (+) '[1,2,3] '[1,1,1]) :: [Nat]
--   = '[2, 3, 4]
--   </pre>
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 <a>TyEq</a>.
module Fcf.Class.Ord

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

-- | "Smaller than or equal to". Type-level version of
--   <tt>(<a>&lt;=</a>)</tt>.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval ("b" &lt;= "a")
--   Eval ("b" &lt;= "a") :: Bool
--   = 'False
--   </pre>
data (<=) :: a -> a -> Exp Bool

-- | "Greater than or equal to". Type-level version of
--   <tt>(<a>&gt;=</a>)</tt>.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval ("b" &gt;= "a")
--   Eval ("b" &gt;= "a") :: Bool
--   = 'True
--   </pre>
data (>=) :: a -> a -> Exp Bool

-- | "Smaller than". Type-level version of <tt>(<a>&lt;</a>)</tt>.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval ("a" &lt; "b")
--   Eval ("a" &lt; "b") :: Bool
--   = 'True
--   </pre>
data (<) :: a -> a -> Exp Bool

-- | "Greater than". Type-level version of <tt>(<a>&gt;</a>)</tt>.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval ("b" &gt; "a")
--   Eval ("b" &gt; "a") :: Bool
--   = 'True
--   </pre>
data (>) :: a -> a -> Exp Bool

-- | Type equality.
--   
--   <h3><b>Details</b></h3>
--   
--   The base library also defines a similar <tt>(<a>==</a>)</tt>; it
--   differs from <a>TyEq</a> in the following ways:
--   
--   <ul>
--   <li><a>TyEq</a> is heterogeneous: its arguments may have different
--   kinds;</li>
--   <li><a>TyEq</a> is reflexive: <tt>TyEq a a</tt> always reduces to
--   <a>True</a> even if <tt>a</tt> is a variable.</li>
--   </ul>
data TyEq :: a -> b -> Exp Bool


-- | First-class type families
--   
--   For example, here is a regular type family:
--   
--   <pre>
--   type family   FromMaybe (a :: k) (m :: Maybe k) :: k
--   type instance FromMaybe a 'Nothing  = a
--   type instance FromMaybe a ('Just b) = b
--   </pre>
--   
--   With <tt>Fcf</tt>, it translates to a <tt>data</tt> declaration:
--   
--   <pre>
--   data FromMaybe :: k -&gt; Maybe k -&gt; <a>Exp</a> k
--   type instance <a>Eval</a> (FromMaybe a 'Nothing)  = a
--   type instance <a>Eval</a> (FromMaybe a ('Just b)) = b
--   </pre>
--   
--   <ul>
--   <li>Fcfs can be higher-order.</li>
--   <li>The kind constructor <a>Exp</a> is a monad: there's
--   <tt>(<a>=&lt;&lt;</a>)</tt> and <a>Pure</a>.</li>
--   </ul>
--   
--   Essential language extensions for <a>Fcf</a>:
--   
--   <pre>
--   {-# LANGUAGE
--       DataKinds,
--       PolyKinds,
--       TypeFamilies,
--       TypeInType,
--       TypeOperators,
--       UndecidableInstances #-}
--   </pre>
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 <tt>($) f</tt> can
--   usually be replaced with <tt>f</tt>.
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 <a>Bimap</a> 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.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Foldr (+) 0 '[1, 2, 3, 4])
--   Eval (Foldr (+) 0 '[1, 2, 3, 4]) :: Nat
--   = 10
--   </pre>
data Foldr :: (a -> b -> Exp b) -> b -> t a -> Exp b

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

-- | List catenation.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval ('[1, 2] ++ '[3, 4])
--   Eval ('[1, 2] ++ '[3, 4]) :: [Nat]
--   = '[1, 2, 3, 4]
--   </pre>
data (++) :: [a] -> [a] -> Exp [a]

-- | Keep all elements that satisfy a predicate, remove all that don't.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Filter ((&gt;) 3) '[1,2,3,0])
--   Eval (Filter ((&gt;) 3) '[1,2,3,0]) :: [Nat]
--   = '[1, 2, 0]
--   </pre>
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 <tt>Just</tt> the first element satisfying a predicate, or
--   evaluate to <tt>Nothing</tt> if no element satisfies the predicate.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Find (TyEq 0) '[1,2,3])
--   Eval (Find (TyEq 0) '[1,2,3]) :: Maybe Nat
--   = 'Nothing
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Find (TyEq 0) '[1,2,3,0])
--   Eval (Find (TyEq 0) '[1,2,3,0]) :: Maybe Nat
--   = 'Just 0
--   </pre>
data Find :: (a -> Exp Bool) -> [a] -> Exp (Maybe a)

-- | Find the index of an element satisfying the predicate.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (FindIndex ((&lt;=) 3) '[1,2,3,1,2,3])
--   Eval (FindIndex ((&lt;=) 3) '[1,2,3,1,2,3]) :: Maybe Nat
--   = 'Just 2
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (FindIndex ((&gt;) 0) '[1,2,3,1,2,3])
--   Eval (FindIndex ((&gt;) 0) '[1,2,3,1,2,3]) :: Maybe Nat
--   = 'Nothing
--   </pre>
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.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (SetIndex 2 7 '[1,2,3])
--   Eval (SetIndex 2 7 '[1,2,3]) :: [Nat]
--   = '[1, 2, 7]
--   </pre>
data SetIndex :: Nat -> a -> [a] -> Exp [a]

-- | Combine elements of two lists pairwise.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (ZipWith (+) '[1,2,3] '[1,1,1])
--   Eval (ZipWith (+) '[1,2,3] '[1,1,1]) :: [Nat]
--   = '[2, 3, 4]
--   </pre>
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 <a>Unzip</a>.
data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])

-- | N.B.: The order of the two branches is the opposite of "if":
--   <tt>UnBool ifFalse ifTrue bool</tt>.
--   
--   This mirrors the default order of constructors:
--   
--   <pre>
--   data Bool = False | True
--   ----------- False &lt; True
--   </pre>
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 <tt>\case { .. }</tt> syntax. Supports
--   matching of exact values (<a>--&gt;</a>) and final matches for any
--   value (<a>Any</a>) or for passing value to subcomputation
--   (<a>Else</a>). Examples:
--   
--   <pre>
--   type BoolToNat = <a>Case</a>
--     [ 'True  <a>--&gt;</a> 0
--     , 'False <a>--&gt;</a> 1
--     ]
--   
--   type NatToBool = <a>Case</a>
--     [ 0 <a>--&gt;</a> 'False
--     , <a>Any</a>   'True
--     ]
--   
--   type ZeroOneOrSucc = <a>Case</a>
--     [ 0  <a>--&gt;</a> 0
--     , 1  <a>--&gt;</a> 1
--     , <a>Else</a>   ((<a>+</a>) 1)
--     ]
--   </pre>
data Case :: [Match j k] -> j -> Exp k
data Match j k

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

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

-- | Match any type in <a>Case</a>. Should be used as a final branch.
--   
--   Note: this identifier conflicts with <a>Any</a> (from
--   <a>Fcf.Class.Foldable</a>) <a>Any</a> (from <a>Data.Monoid</a>), and
--   <a>Any</a> (from <a>GHC.Exts</a>).
--   
--   We recommend importing this one qualified.
type Any = ('Any_ :: k -> Match j k)

-- | Pass type being matched in <a>Case</a> 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 <a>fmap</a> for type-level functors.
--   
--   Note: this name clashes with <a>Map</a> from <i>containers</i>.
--   <a>FMap</a> is provided as a synonym to avoid this.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; import Fcf.Data.Nat
--   
--   &gt;&gt;&gt; import qualified GHC.TypeLits as TL
--   
--   &gt;&gt;&gt; data AddMul :: Nat -&gt; Nat -&gt; Exp Nat
--   
--   &gt;&gt;&gt; type instance Eval (AddMul x y) = (x TL.+ y) TL.* (x TL.+ y)
--   
--   &gt;&gt;&gt; :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]
--   </pre>
data Map :: (a -> Exp b) -> f a -> Exp (f b)

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

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

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

-- | Type equality.
--   
--   <h3><b>Details</b></h3>
--   
--   The base library also defines a similar <tt>(<a>==</a>)</tt>; it
--   differs from <a>TyEq</a> in the following ways:
--   
--   <ul>
--   <li><a>TyEq</a> is heterogeneous: its arguments may have different
--   kinds;</li>
--   <li><a>TyEq</a> is reflexive: <tt>TyEq a a</tt> always reduces to
--   <a>True</a> even if <tt>a</tt> is a variable.</li>
--   </ul>
data TyEq :: a -> b -> Exp Bool

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