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


-- | Overloaded functions.
module Fcf.Classes

-- | Type-level <a>fmap</a> for type-level functors.
data Map :: (a -> Exp b) -> f a -> Exp (f b)

-- | Type-level <a>bimap</a>.
data Bimap :: (a -> Exp a') -> (b -> Exp b') -> f a b -> Exp (f a' b')


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

-- | Equivalent to <tt>Bimap</tt> 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


-- | 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.
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 = Case
--     [ 'True  --&gt; 0
--     , 'False --&gt; 1
--     ]
--   
--   type NatToBool = Case
--     [ 0 --&gt; 'False
--     , Any   'True
--     ]
--   
--   type ZeroOneOrSucc = Case
--     [ 0  --&gt; 0
--     , 1  --&gt; 1
--     , Else   ((+) 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.
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-level <a>If</a>. <tt>If True a b</tt> ==&gt; <tt>a</tt>; <tt>If
--   False a b</tt> ==&gt; <tt>b</tt>
type family If (cond :: Bool) (tru :: k) (fls :: k) :: k
instance Fcf.Utils.IsBool 'GHC.Types.True
instance Fcf.Utils.IsBool 'GHC.Types.False


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

-- | A conditional choosing the first branch whose guard <tt>a -&gt;
--   <a>Exp</a> <a>Bool</a></tt> accepts a given value <tt>a</tt>.
--   
--   <h3>Example</h3>
--   
--   <pre>
--   type UnitPrefix n = <a>Eval</a> (<a>Guarded</a> n
--     '[ <a>TyEq</a> 0 '<a>:=</a> <tt>Pure</tt> ""
--      , <a>TyEq</a> 1 '<a>:=</a> <tt>Pure</tt> "deci"
--      , <a>TyEq</a> 2 '<a>:=</a> <tt>Pure</tt> "hecto"
--      , <a>TyEq</a> 3 '<a>:=</a> <tt>Pure</tt> "kilo"
--      , <a>TyEq</a> 6 '<a>:=</a> <tt>Pure</tt> "mega"
--      , <a>TyEq</a> 9 '<a>:=</a> <tt>Pure</tt> "giga"
--      , <a>Otherwise</a> '<a>:=</a> <a>Error</a> "Something else"
--      ])
--   </pre>

-- | <i>Deprecated: Use <a>Case</a> instead</i>
data Guarded :: a -> [Guard (a -> Exp Bool) (Exp b)] -> Exp b

-- | A fancy-looking pair type to use with <a>Guarded</a>.
data Guard a b
(:=) :: a -> b -> Guard a b
infixr 0 :=

-- | A catch-all guard for <a>Guarded</a>.
type Otherwise = ConstFn  'True


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

-- | (Kind) This is the kind of type-level natural numbers.
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


-- | Lists.
module Fcf.Data.List
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 Cons :: a -> [a] -> Exp [a]
data (++) :: [a] -> [a] -> Exp [a]
data Filter :: (a -> Exp Bool) -> [a] -> Exp [a]
data Head :: [a] -> Exp (Maybe a)
data Last :: [a] -> Exp (Maybe a)
data Tail :: [a] -> Exp (Maybe [a])
data Init :: [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)
type Elem a as = IsJust =<< FindIndex (TyEq a) as

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


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

-- | Equivalent to <tt>Bimap</tt> 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
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]
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])

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

-- | A conditional choosing the first branch whose guard <tt>a -&gt;
--   <a>Exp</a> <a>Bool</a></tt> accepts a given value <tt>a</tt>.
--   
--   <h3>Example</h3>
--   
--   <pre>
--   type UnitPrefix n = <a>Eval</a> (<a>Guarded</a> n
--     '[ <a>TyEq</a> 0 '<a>:=</a> <tt>Pure</tt> ""
--      , <a>TyEq</a> 1 '<a>:=</a> <tt>Pure</tt> "deci"
--      , <a>TyEq</a> 2 '<a>:=</a> <tt>Pure</tt> "hecto"
--      , <a>TyEq</a> 3 '<a>:=</a> <tt>Pure</tt> "kilo"
--      , <a>TyEq</a> 6 '<a>:=</a> <tt>Pure</tt> "mega"
--      , <a>TyEq</a> 9 '<a>:=</a> <tt>Pure</tt> "giga"
--      , <a>Otherwise</a> '<a>:=</a> <a>Error</a> "Something else"
--      ])
--   </pre>

-- | <i>Deprecated: Use <a>Case</a> instead</i>
data Guarded :: a -> [Guard (a -> Exp Bool) (Exp b)] -> Exp b

-- | A fancy-looking pair type to use with <a>Guarded</a>.
data Guard a b
(:=) :: a -> b -> Guard a b
infixr 0 :=

-- | A catch-all guard for <a>Guarded</a>.
type Otherwise = ConstFn  'True

-- | (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 = Case
--     [ 'True  --&gt; 0
--     , 'False --&gt; 1
--     ]
--   
--   type NatToBool = Case
--     [ 0 --&gt; 'False
--     , Any   'True
--     ]
--   
--   type ZeroOneOrSucc = Case
--     [ 0  --&gt; 0
--     , 1  --&gt; 1
--     , Else   ((+) 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.
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.
data Map :: (a -> Exp b) -> f a -> Exp (f b)

-- | Type-level <a>bimap</a>.
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.
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-level <a>If</a>. <tt>If True a b</tt> ==&gt; <tt>a</tt>; <tt>If
--   False a b</tt> ==&gt; <tt>b</tt>
type family If (cond :: Bool) (tru :: k) (fls :: k) :: k
