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


-- | 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
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 <=<
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 Uncurry :: (a -> b -> Exp c) -> (a, b) -> Exp c
data UnEither :: (a -> Exp c) -> (b -> Exp c) -> Either a b -> Exp c
data ConstFn :: a -> b -> Exp a
data Fst :: (a, b) -> Exp a
data Snd :: (a, b) -> Exp b

-- | Equivalent to <a>Bimap</a>.
data (***) :: (b -> Exp c) -> (b' -> Exp c') -> (b, b') -> Exp (c, c')
infixr 3 ***
data Foldr :: (a -> b -> Exp b) -> b -> [a] -> Exp b

-- | N.B.: This is equivalent to a <a>Foldr</a> flipped.
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)

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

-- | Find an element associated with a key. <tt> <a>Lookup</a> :: k -&gt;
--   [(k, b)] -&gt; <a>Exp</a> (<a>Maybe</a> b) </tt>
type Lookup (a :: k) (as :: [(k, b)]) = (Map Snd (Eval (Find (TyEq a <=< Fst) as)) :: Exp (Maybe b))

-- | Modify an element at a given index.
--   
--   The list is unchanged if the index is out of bounds.
data SetIndex :: Nat -> a -> [a] -> Exp [a]
type family SetIndexImpl (n :: Nat) (a' :: k) (as :: [k])
data ZipWith :: (a -> b -> Exp c) -> [a] -> [b] -> Exp [c]

-- | <pre>
--   <a>Zip</a> :: [a] -&gt; [b] -&gt; <a>Exp</a> [(a, b)]
--   </pre>
type Zip = ZipWith (Pure2  '(,))
data Unzip :: Exp [(a, b)] -> Exp ([a], [b])
data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])
data UnMaybe :: Exp b -> (a -> Exp b) -> Maybe a -> Exp b
data FromMaybe :: k -> Maybe k -> Exp k
data IsJust :: Maybe a -> Exp Bool
data IsNothing :: Maybe a -> Exp Bool
data IsLeft :: Either a b -> Exp Bool
data IsRight :: Either a b -> Exp Bool

-- | Type-level <a>fmap</a> for type-level functors.
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')

-- | 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
data (+) :: Nat -> Nat -> Exp Nat
data (-) :: Nat -> Nat -> Exp Nat
data (*) :: Nat -> Nat -> Exp Nat
data (^) :: Nat -> Nat -> Exp Nat
data Error :: Symbol -> Exp a
data Collapse :: [Constraint] -> Exp Constraint
data TyEq :: a -> b -> Exp Bool
type family TyEqImpl (a :: k) (b :: k) :: Bool

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

-- | A stuck type that can be used like a type-level <a>undefined</a>.
type family Stuck :: a

-- | Apply and evaluate a unary type function.
type f @@ x = Eval (f x)
class IsBool (b :: Bool)
_If :: IsBool b => (b ~  'True => r) -> (b ~  'False => r) -> r
type family If (b :: Bool) (x :: k) (y :: k) :: k
instance Fcf.IsBool 'GHC.Types.True
instance Fcf.IsBool 'GHC.Types.False
