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

-- | First class type families
--   
--   First class type families, eval-style defunctionalization
--   
--   See Fcf.
@package first-class-families
@version 0.6.0.0

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

-- | Overloaded functions.
module Fcf.Classes

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

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

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

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

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

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

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

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

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

-- | A catch-all guard for Guarded.
type Otherwise = ConstFn  'True

-- | Natural numbers.
--   
--   Note that the operators from this module conflict with
--   GHC.TypeLits and GHC.TypeNats.
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 Foldr 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.  Lookup :: k ->
--   [(k, b)] -> Exp (Maybe b) 
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]

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

-- | Equivalent to 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
data Foldr :: (a -> b -> Exp b) -> b -> [a] -> Exp b

-- | N.B.: This is equivalent to a Foldr 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.  Lookup :: k ->
--   [(k, b)] -> Exp (Maybe b) 
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]

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

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

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

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

-- | A catch-all guard for Guarded.
type Otherwise = ConstFn  'True

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

-- | Type-level bimap.
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.
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
