Safe Haskell	Safe
Language	Haskell2010

Fcf

Contents

First-class type families
Helpful shorthands
Reification

Description

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.

Synopsis

type Exp a = a -> Type
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
data (<=<) :: (b -> Exp c) -> (a -> Exp b) -> a -> Exp c
data Join :: Exp (Exp a) -> Exp a
data (<$>) :: (a -> b) -> Exp a -> Exp b
data (<*>) :: Exp (a -> b) -> Exp a -> Exp b
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 UnMaybe :: Exp b -> (a -> Exp b) -> Maybe a -> Exp b
data ConstFn :: a -> b -> Exp a
data Fst :: (a, b) -> Exp a
data Snd :: (a, b) -> Exp b
data (***) :: (b -> Exp c) -> (b' -> Exp c') -> (b, b') -> Exp (c, c')
data Foldr :: (a -> b -> Exp b) -> b -> [a] -> Exp b
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)
type Lookup (a :: k) (as :: [(k, b)]) = (Map Snd (Eval (Find (TyEq a <=< Fst) as)) :: Exp (Maybe b))
data ZipWith :: (a -> b -> Exp c) -> [a] -> [b] -> Exp [c]
type Zip = ZipWith (Pure2 (,))
data Unzip :: Exp [(a, b)] -> Exp ([a], [b])
data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])
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')
data UnBool :: Exp a -> Exp a -> Bool -> Exp a
data (||) :: Bool -> Bool -> Exp Bool
data (&&) :: Bool -> Bool -> Exp Bool
data Error :: Symbol -> Exp a
data Collapse :: [Constraint] -> Exp Constraint
data TyEq :: a -> b -> Exp Bool
type family TyEqImpl (a :: k) (b :: k) :: Bool where ...
data ($) :: (a -> Exp b) -> a -> Exp b
type (@@) f x = Eval (f x)
class IsBool (b :: Bool) where
type family If (b :: Bool) (x :: k) (y :: k) :: k

First-class type families

type Exp a = a -> Type Source #

Kind of type-level expressions indexed by their result type.

type family Eval (e :: Exp a) :: a Source #

Expression evaluator.

Instances

type Eval (Collapse (a ': as) :: Constraint -> Type) Source #
Instance details Defined in Fcf type Eval (Collapse (a ': as) :: Constraint -> Type) = (a, Eval (Collapse as))
type Eval (Collapse ([] :: [Constraint])) Source #
Instance details Defined in Fcf type Eval (Collapse ([] :: [Constraint])) = () ~ ()
type Eval (False && b :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (False && b :: Bool -> Type) = False
type Eval (True && b :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (True && b :: Bool -> Type) = b
type Eval (a && True :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (a && True :: Bool -> Type) = a
type Eval (a && False :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (a && False :: Bool -> Type) = False
type Eval (False \|\| b :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (False \|\| b :: Bool -> Type) = b
type Eval (True \|\| b :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (True \|\| b :: Bool -> Type) = True
type Eval (a \|\| False :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (a \|\| False :: Bool -> Type) = a
type Eval (a \|\| True :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (a \|\| True :: Bool -> Type) = True
type Eval (Null (a2 ': as) :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (Null (a2 ': as) :: Bool -> Type) = False
type Eval (Null ([] :: [a]) :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (Null ([] :: [a]) :: Bool -> Type) = True
type Eval (Length (a2 ': as) :: Nat -> Type) Source #
Instance details Defined in Fcf type Eval (Length (a2 ': as) :: Nat -> Type) = 1 + Eval (Length as)
type Eval (Length ([] :: [a]) :: Nat -> Type) Source #
Instance details Defined in Fcf type Eval (Length ([] :: [a]) :: Nat -> Type) = 0
type Eval (Pure x :: a -> Type) Source #
Instance details Defined in Fcf type Eval (Pure x :: a -> Type) = x
type Eval (Join e :: a -> Type) Source #
Instance details Defined in Fcf type Eval (Join e :: a -> Type) = Eval (Eval e)
type Eval (Error msg :: a -> Type) Source #
Instance details Defined in Fcf type Eval (Error msg :: a -> Type) = (TypeError (Text msg) :: a)
type Eval (Fst ((,) a2 _b) :: a1 -> Type) Source #
Instance details Defined in Fcf type Eval (Fst ((,) a2 _b) :: a1 -> Type) = a2
type Eval (Snd ((,) _a b) :: a1 -> Type) Source #
Instance details Defined in Fcf type Eval (Snd ((,) _a b) :: a1 -> Type) = b
type Eval (TyEq a b :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (TyEq a b :: Bool -> Type) = TyEqImpl a b
type Eval (Pure1 f x :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (Pure1 f x :: a2 -> Type) = f x
type Eval (k =<< e :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (k =<< e :: a2 -> Type) = Eval (k (Eval e))
type Eval (f <$> e :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (f <$> e :: a2 -> Type) = f (Eval e)
type Eval (f <*> e :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (f <*> e :: a2 -> Type) = Eval f (Eval e)
type Eval (ConstFn a2 _b :: a1 -> Type) Source #
Instance details Defined in Fcf type Eval (ConstFn a2 _b :: a1 -> Type) = a2
type Eval (UnBool fal tru True :: a -> Type) Source #
Instance details Defined in Fcf type Eval (UnBool fal tru True :: a -> Type) = Eval tru
type Eval (UnBool fal tru False :: a -> Type) Source #
Instance details Defined in Fcf type Eval (UnBool fal tru False :: a -> Type) = Eval fal
type Eval (f $ a3 :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (f $ a3 :: a2 -> Type) = Eval (f a3)
type Eval (Uncurry f ((,) x y) :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (Uncurry f ((,) x y) :: a2 -> Type) = Eval (f x y)
type Eval (UnMaybe y f (Just x) :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (UnMaybe y f (Just x) :: a2 -> Type) = Eval (f x)
type Eval (UnMaybe y f (Nothing :: Maybe a1) :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (UnMaybe y f (Nothing :: Maybe a1) :: a2 -> Type) = Eval y
type Eval (Foldr f y (x ': xs) :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (Foldr f y (x ': xs) :: a2 -> Type) = Eval (f x (Eval (Foldr f y xs)))
type Eval (Foldr f y ([] :: [a1]) :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (Foldr f y ([] :: [a1]) :: a2 -> Type) = y
type Eval (UnList y f xs :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (UnList y f xs :: a2 -> Type) = Eval (Foldr f y xs)
type Eval (Pure2 f x y :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (Pure2 f x y :: a2 -> Type) = f x y
type Eval ((f <=< g) x :: a3 -> Type) Source #
Instance details Defined in Fcf type Eval ((f <=< g) x :: a3 -> Type) = Eval (f (Eval (g x)))
type Eval (Flip f y x :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (Flip f y x :: a2 -> Type) = Eval (f x y)
type Eval (UnEither f g (Right y :: Either a2 b) :: a1 -> Type) Source #
Instance details Defined in Fcf type Eval (UnEither f g (Right y :: Either a2 b) :: a1 -> Type) = Eval (g y)
type Eval (UnEither f g (Left x :: Either a2 b) :: a1 -> Type) Source #
Instance details Defined in Fcf type Eval (UnEither f g (Left x :: Either a2 b) :: a1 -> Type) = Eval (f x)
type Eval (Pure3 f x y z :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (Pure3 f x y z :: a2 -> Type) = f x y z
type Eval (Tail (_a ': as) :: Maybe [a] -> Type) Source #
Instance details Defined in Fcf type Eval (Tail (_a ': as) :: Maybe [a] -> Type) = Just as
type Eval (Tail ([] :: [a]) :: Maybe [a] -> Type) Source #
Instance details Defined in Fcf type Eval (Tail ([] :: [a]) :: Maybe [a] -> Type) = (Nothing :: Maybe [a])
type Eval (Head (a2 ': _as) :: Maybe a1 -> Type) Source #
Instance details Defined in Fcf type Eval (Head (a2 ': _as) :: Maybe a1 -> Type) = Just a2
type Eval (Head ([] :: [a]) :: Maybe a -> Type) Source #
Instance details Defined in Fcf type Eval (Head ([] :: [a]) :: Maybe a -> Type) = (Nothing :: Maybe a)
type Eval ((x ': xs) ++ ys :: [a] -> Type) Source #
Instance details Defined in Fcf type Eval ((x ': xs) ++ ys :: [a] -> Type) = x ': Eval (xs ++ ys)
type Eval (([] :: [a]) ++ ys :: [a] -> Type) Source #
Instance details Defined in Fcf type Eval (([] :: [a]) ++ ys :: [a] -> Type) = ys
type Eval (Filter _p ([] :: [a]) :: [a] -> Type) Source #
Instance details Defined in Fcf type Eval (Filter _p ([] :: [a]) :: [a] -> Type) = ([] :: [a])
type Eval (Filter p (a2 ': as) :: [a1] -> Type) Source #
Instance details Defined in Fcf type Eval (Filter p (a2 ': as) :: [a1] -> Type) = If (Eval (p a2)) (a2 ': Eval (Filter p as)) (Eval (Filter p as))
type Eval (Find _p ([] :: [a]) :: Maybe a -> Type) Source #
Instance details Defined in Fcf type Eval (Find _p ([] :: [a]) :: Maybe a -> Type) = (Nothing :: Maybe a)
type Eval (Find p (a2 ': as) :: Maybe a1 -> Type) Source #
Instance details Defined in Fcf type Eval (Find p (a2 ': as) :: Maybe a1 -> Type) = If (Eval (p a2)) (Just a2) (Eval (Find p as))
type Eval (Map f (a2 ': as) :: [b] -> Type) Source #
Instance details Defined in Fcf type Eval (Map f (a2 ': as) :: [b] -> Type) = Eval (f a2) ': Eval (Map f as)
type Eval (Map f ([] :: [a]) :: [b] -> Type) Source #
Instance details Defined in Fcf type Eval (Map f ([] :: [a]) :: [b] -> Type) = ([] :: [b])
type Eval (Map f (Just a3) :: Maybe a2 -> Type) Source #
Instance details Defined in Fcf type Eval (Map f (Just a3) :: Maybe a2 -> Type) = Just (Eval (f a3))
type Eval (Map f (Nothing :: Maybe a) :: Maybe b -> Type) Source #
Instance details Defined in Fcf type Eval (Map f (Nothing :: Maybe a) :: Maybe b -> Type) = (Nothing :: Maybe b)
type Eval (ZipWith f (a2 ': as) (b2 ': bs) :: [c] -> Type) Source #
Instance details Defined in Fcf type Eval (ZipWith f (a2 ': as) (b2 ': bs) :: [c] -> Type) = Eval (f a2 b2) ': Eval (ZipWith f as bs)
type Eval (ZipWith _f _as ([] :: [b]) :: [c] -> Type) Source #
Instance details Defined in Fcf type Eval (ZipWith _f _as ([] :: [b]) :: [c] -> Type) = ([] :: [c])
type Eval (ZipWith _f ([] :: [a]) _bs :: [c] -> Type) Source #
Instance details Defined in Fcf type Eval (ZipWith _f ([] :: [a]) _bs :: [c] -> Type) = ([] :: [c])
type Eval (Unzip as :: ([a], [b]) -> Type) Source #
Instance details Defined in Fcf type Eval (Unzip as :: ([a], [b]) -> Type) = Eval (Foldr (Cons2 :: (a, b) -> ([a], [b]) -> ([a], [b]) -> Type) ((,) ([] :: [a]) ([] :: [b])) (Eval as))
type Eval (Cons2 ((,) a3 b) ((,) as bs) :: ([a2], [a1]) -> Type) Source #
Instance details Defined in Fcf type Eval (Cons2 ((,) a3 b) ((,) as bs) :: ([a2], [a1]) -> Type) = (,) (a3 ': as) (b ': bs)
type Eval (Map f (Right a3 :: Either a2 a1) :: Either a2 b -> Type) Source #
Instance details Defined in Fcf type Eval (Map f (Right a3 :: Either a2 a1) :: Either a2 b -> Type) = (Right (Eval (f a3)) :: Either a2 b)
type Eval (Map f (Left x :: Either a2 a1) :: Either a2 b -> Type) Source #
Instance details Defined in Fcf type Eval (Map f (Left x :: Either a2 a1) :: Either a2 b -> Type) = (Left x :: Either a2 b)
type Eval (Map f ((,) x a2) :: (k2, k1) -> Type) Source #
Instance details Defined in Fcf type Eval (Map f ((,) x a2) :: (k2, k1) -> Type) = (,) x (Eval (f a2))
type Eval ((f *** f') ((,) b2 b'2) :: (k2, k1) -> Type) Source #
Instance details Defined in Fcf type Eval ((f *** f') ((,) b2 b'2) :: (k2, k1) -> Type) = (,) (Eval (f b2)) (Eval (f' b'2))
type Eval (Bimap f g (Right y :: Either a b1) :: Either a' b2 -> Type) Source #
Instance details Defined in Fcf type Eval (Bimap f g (Right y :: Either a b1) :: Either a' b2 -> Type) = (Right (Eval (g y)) :: Either a' b2)
type Eval (Bimap f g (Left x :: Either a1 b) :: Either a2 b' -> Type) Source #
Instance details Defined in Fcf type Eval (Bimap f g (Left x :: Either a1 b) :: Either a2 b' -> Type) = (Left (Eval (f x)) :: Either a2 b')
type Eval (Bimap f g ((,) x y) :: (k2, k1) -> Type) Source #
Instance details Defined in Fcf type Eval (Bimap f g ((,) x y) :: (k2, k1) -> Type) = (,) (Eval (f x)) (Eval (g y))
type Eval (Map f ((,,) x y a2) :: (k2, k3, k1) -> Type) Source #
Instance details Defined in Fcf type Eval (Map f ((,,) x y a2) :: (k2, k3, k1) -> Type) = (,,) x y (Eval (f a2))
type Eval (Map f ((,,,) x y z a2) :: (k2, k3, k4, k1) -> Type) Source #
Instance details Defined in Fcf type Eval (Map f ((,,,) x y z a2) :: (k2, k3, k4, k1) -> Type) = (,,,) x y z (Eval (f a2))
type Eval (Map f ((,,,,) x y z w a2) :: (k2, k3, k4, k5, k1) -> Type) Source #
Instance details Defined in Fcf type Eval (Map f ((,,,,) x y z w a2) :: (k2, k3, k4, k5, k1) -> Type) = (,,,,) x y z w (Eval (f a2))

Monadic operations

data Pure :: a -> Exp a Source #

Instances

type Eval (Pure x :: a -> Type) Source #
Instance details Defined in Fcf type Eval (Pure x :: a -> Type) = x

data Pure1 :: (a -> b) -> a -> Exp b Source #

Instances

type Eval (Pure1 f x :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (Pure1 f x :: a2 -> Type) = f x

data Pure2 :: (a -> b -> c) -> a -> b -> Exp c Source #

Instances

type Eval (Pure2 f x y :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (Pure2 f x y :: a2 -> Type) = f x y

data Pure3 :: (a -> b -> c -> d) -> a -> b -> c -> Exp d Source #

Instances

type Eval (Pure3 f x y z :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (Pure3 f x y z :: a2 -> Type) = f x y z

data (=<<) :: (a -> Exp b) -> Exp a -> Exp b infixr 1 Source #

Instances

type Eval (k =<< e :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (k =<< e :: a2 -> Type) = Eval (k (Eval e))

data (<=<) :: (b -> Exp c) -> (a -> Exp b) -> a -> Exp c infixr 1 Source #

Instances

type Eval ((f <=< g) x :: a3 -> Type) Source #
Instance details Defined in Fcf type Eval ((f <=< g) x :: a3 -> Type) = Eval (f (Eval (g x)))

data Join :: Exp (Exp a) -> Exp a Source #

Instances

type Eval (Join e :: a -> Type) Source #
Instance details Defined in Fcf type Eval (Join e :: a -> Type) = Eval (Eval e)

data (<$>) :: (a -> b) -> Exp a -> Exp b infixl 4 Source #

Instances

type Eval (f <$> e :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (f <$> e :: a2 -> Type) = f (Eval e)

data (<*>) :: Exp (a -> b) -> Exp a -> Exp b infixl 4 Source #

Instances

type Eval (f <*> e :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (f <*> e :: a2 -> Type) = Eval f (Eval e)

More combinators

data Flip :: (a -> b -> Exp c) -> b -> a -> Exp c Source #

Instances

type Eval (Flip f y x :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (Flip f y x :: a2 -> Type) = Eval (f x y)

data Uncurry :: (a -> b -> Exp c) -> (a, b) -> Exp c Source #

Instances

type Eval (Uncurry f ((,) x y) :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (Uncurry f ((,) x y) :: a2 -> Type) = Eval (f x y)

data UnEither :: (a -> Exp c) -> (b -> Exp c) -> Either a b -> Exp c Source #

Instances

type Eval (UnEither f g (Right y :: Either a2 b) :: a1 -> Type) Source #
Instance details Defined in Fcf type Eval (UnEither f g (Right y :: Either a2 b) :: a1 -> Type) = Eval (g y)
type Eval (UnEither f g (Left x :: Either a2 b) :: a1 -> Type) Source #
Instance details Defined in Fcf type Eval (UnEither f g (Left x :: Either a2 b) :: a1 -> Type) = Eval (f x)

data UnMaybe :: Exp b -> (a -> Exp b) -> Maybe a -> Exp b Source #

Instances

type Eval (UnMaybe y f (Just x) :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (UnMaybe y f (Just x) :: a2 -> Type) = Eval (f x)
type Eval (UnMaybe y f (Nothing :: Maybe a1) :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (UnMaybe y f (Nothing :: Maybe a1) :: a2 -> Type) = Eval y

data ConstFn :: a -> b -> Exp a Source #

Instances

type Eval (ConstFn a2 _b :: a1 -> Type) Source #
Instance details Defined in Fcf type Eval (ConstFn a2 _b :: a1 -> Type) = a2

Tuples

data Fst :: (a, b) -> Exp a Source #

Instances

type Eval (Fst ((,) a2 _b) :: a1 -> Type) Source #
Instance details Defined in Fcf type Eval (Fst ((,) a2 _b) :: a1 -> Type) = a2

data Snd :: (a, b) -> Exp b Source #

Instances

type Eval (Snd ((,) _a b) :: a1 -> Type) Source #
Instance details Defined in Fcf type Eval (Snd ((,) _a b) :: a1 -> Type) = b

data (***) :: (b -> Exp c) -> (b' -> Exp c') -> (b, b') -> Exp (c, c') infixr 3 Source #

Equivalent to Bimap.

Instances

type Eval ((f *** f') ((,) b2 b'2) :: (k2, k1) -> Type) Source #
Instance details Defined in Fcf type Eval ((f *** f') ((,) b2 b'2) :: (k2, k1) -> Type) = (,) (Eval (f b2)) (Eval (f' b'2))

Lists

data Foldr :: (a -> b -> Exp b) -> b -> [a] -> Exp b Source #

Instances

type Eval (Foldr f y (x ': xs) :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (Foldr f y (x ': xs) :: a2 -> Type) = Eval (f x (Eval (Foldr f y xs)))
type Eval (Foldr f y ([] :: [a1]) :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (Foldr f y ([] :: [a1]) :: a2 -> Type) = y

data UnList :: b -> (a -> b -> Exp b) -> [a] -> Exp b Source #

N.B.: This is equivalent to a Foldr flipped.

Instances

type Eval (UnList y f xs :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (UnList y f xs :: a2 -> Type) = Eval (Foldr f y xs)

data (++) :: [a] -> [a] -> Exp [a] Source #

Instances

type Eval ((x ': xs) ++ ys :: [a] -> Type) Source #
Instance details Defined in Fcf type Eval ((x ': xs) ++ ys :: [a] -> Type) = x ': Eval (xs ++ ys)
type Eval (([] :: [a]) ++ ys :: [a] -> Type) Source #
Instance details Defined in Fcf type Eval (([] :: [a]) ++ ys :: [a] -> Type) = ys

data Filter :: (a -> Exp Bool) -> [a] -> Exp [a] Source #

Instances

type Eval (Filter _p ([] :: [a]) :: [a] -> Type) Source #
Instance details Defined in Fcf type Eval (Filter _p ([] :: [a]) :: [a] -> Type) = ([] :: [a])
type Eval (Filter p (a2 ': as) :: [a1] -> Type) Source #
Instance details Defined in Fcf type Eval (Filter p (a2 ': as) :: [a1] -> Type) = If (Eval (p a2)) (a2 ': Eval (Filter p as)) (Eval (Filter p as))

data Head :: [a] -> Exp (Maybe a) Source #

Instances

type Eval (Head (a2 ': _as) :: Maybe a1 -> Type) Source #
Instance details Defined in Fcf type Eval (Head (a2 ': _as) :: Maybe a1 -> Type) = Just a2
type Eval (Head ([] :: [a]) :: Maybe a -> Type) Source #
Instance details Defined in Fcf type Eval (Head ([] :: [a]) :: Maybe a -> Type) = (Nothing :: Maybe a)

data Tail :: [a] -> Exp (Maybe [a]) Source #

Instances

type Eval (Tail (_a ': as) :: Maybe [a] -> Type) Source #
Instance details Defined in Fcf type Eval (Tail (_a ': as) :: Maybe [a] -> Type) = Just as
type Eval (Tail ([] :: [a]) :: Maybe [a] -> Type) Source #
Instance details Defined in Fcf type Eval (Tail ([] :: [a]) :: Maybe [a] -> Type) = (Nothing :: Maybe [a])

data Null :: [a] -> Exp Bool Source #

Instances

type Eval (Null (a2 ': as) :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (Null (a2 ': as) :: Bool -> Type) = False
type Eval (Null ([] :: [a]) :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (Null ([] :: [a]) :: Bool -> Type) = True

data Length :: [a] -> Exp Nat Source #

Instances

type Eval (Length (a2 ': as) :: Nat -> Type) Source #
Instance details Defined in Fcf type Eval (Length (a2 ': as) :: Nat -> Type) = 1 + Eval (Length as)
type Eval (Length ([] :: [a]) :: Nat -> Type) Source #
Instance details Defined in Fcf type Eval (Length ([] :: [a]) :: Nat -> Type) = 0

data Find :: (a -> Exp Bool) -> [a] -> Exp (Maybe a) Source #

Instances

type Eval (Find _p ([] :: [a]) :: Maybe a -> Type) Source #
Instance details Defined in Fcf type Eval (Find _p ([] :: [a]) :: Maybe a -> Type) = (Nothing :: Maybe a)
type Eval (Find p (a2 ': as) :: Maybe a1 -> Type) Source #
Instance details Defined in Fcf type Eval (Find p (a2 ': as) :: Maybe a1 -> Type) = If (Eval (p a2)) (Just a2) (Eval (Find p as))

type Lookup (a :: k) (as :: [(k, b)]) = (Map Snd (Eval (Find (TyEq a <=< Fst) as)) :: Exp (Maybe b)) Source #

Lookup :: k -> [(k, b)] -> Exp (Maybe b)

data ZipWith :: (a -> b -> Exp c) -> [a] -> [b] -> Exp [c] Source #

Instances

type Eval (ZipWith f (a2 ': as) (b2 ': bs) :: [c] -> Type) Source #
Instance details Defined in Fcf type Eval (ZipWith f (a2 ': as) (b2 ': bs) :: [c] -> Type) = Eval (f a2 b2) ': Eval (ZipWith f as bs)
type Eval (ZipWith _f _as ([] :: [b]) :: [c] -> Type) Source #
Instance details Defined in Fcf type Eval (ZipWith _f _as ([] :: [b]) :: [c] -> Type) = ([] :: [c])
type Eval (ZipWith _f ([] :: [a]) _bs :: [c] -> Type) Source #
Instance details Defined in Fcf type Eval (ZipWith _f ([] :: [a]) _bs :: [c] -> Type) = ([] :: [c])

type Zip = ZipWith (Pure2 (,)) Source #

Zip :: [a] -> [b] -> Exp [(a, b)]

data Unzip :: Exp [(a, b)] -> Exp ([a], [b]) Source #

Instances

type Eval (Unzip as :: ([a], [b]) -> Type) Source #
Instance details Defined in Fcf type Eval (Unzip as :: ([a], [b]) -> Type) = Eval (Foldr (Cons2 :: (a, b) -> ([a], [b]) -> ([a], [b]) -> Type) ((,) ([] :: [a]) ([] :: [b])) (Eval as))

data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b]) Source #

Instances

type Eval (Cons2 ((,) a3 b) ((,) as bs) :: ([a2], [a1]) -> Type) Source #
Instance details Defined in Fcf type Eval (Cons2 ((,) a3 b) ((,) as bs) :: ([a2], [a1]) -> Type) = (,) (a3 ': as) (b ': bs)

Overloaded functions

data Map :: (a -> Exp b) -> f a -> Exp (f b) Source #

Type-level fmap for type-level functors.

Instances

type Eval (Map f (a2 ': as) :: [b] -> Type) Source #
Instance details Defined in Fcf type Eval (Map f (a2 ': as) :: [b] -> Type) = Eval (f a2) ': Eval (Map f as)
type Eval (Map f ([] :: [a]) :: [b] -> Type) Source #
Instance details Defined in Fcf type Eval (Map f ([] :: [a]) :: [b] -> Type) = ([] :: [b])
type Eval (Map f (Just a3) :: Maybe a2 -> Type) Source #
Instance details Defined in Fcf type Eval (Map f (Just a3) :: Maybe a2 -> Type) = Just (Eval (f a3))
type Eval (Map f (Nothing :: Maybe a) :: Maybe b -> Type) Source #
Instance details Defined in Fcf type Eval (Map f (Nothing :: Maybe a) :: Maybe b -> Type) = (Nothing :: Maybe b)
type Eval (Map f (Right a3 :: Either a2 a1) :: Either a2 b -> Type) Source #
Instance details Defined in Fcf type Eval (Map f (Right a3 :: Either a2 a1) :: Either a2 b -> Type) = (Right (Eval (f a3)) :: Either a2 b)
type Eval (Map f (Left x :: Either a2 a1) :: Either a2 b -> Type) Source #
Instance details Defined in Fcf type Eval (Map f (Left x :: Either a2 a1) :: Either a2 b -> Type) = (Left x :: Either a2 b)
type Eval (Map f ((,) x a2) :: (k2, k1) -> Type) Source #
Instance details Defined in Fcf type Eval (Map f ((,) x a2) :: (k2, k1) -> Type) = (,) x (Eval (f a2))
type Eval (Map f ((,,) x y a2) :: (k2, k3, k1) -> Type) Source #
Instance details Defined in Fcf type Eval (Map f ((,,) x y a2) :: (k2, k3, k1) -> Type) = (,,) x y (Eval (f a2))
type Eval (Map f ((,,,) x y z a2) :: (k2, k3, k4, k1) -> Type) Source #
Instance details Defined in Fcf type Eval (Map f ((,,,) x y z a2) :: (k2, k3, k4, k1) -> Type) = (,,,) x y z (Eval (f a2))
type Eval (Map f ((,,,,) x y z w a2) :: (k2, k3, k4, k5, k1) -> Type) Source #
Instance details Defined in Fcf type Eval (Map f ((,,,,) x y z w a2) :: (k2, k3, k4, k5, k1) -> Type) = (,,,,) x y z w (Eval (f a2))

data Bimap :: (a -> Exp a') -> (b -> Exp b') -> f a b -> Exp (f a' b') Source #

Instances

type Eval (Bimap f g (Right y :: Either a b1) :: Either a' b2 -> Type) Source #
Instance details Defined in Fcf type Eval (Bimap f g (Right y :: Either a b1) :: Either a' b2 -> Type) = (Right (Eval (g y)) :: Either a' b2)
type Eval (Bimap f g (Left x :: Either a1 b) :: Either a2 b' -> Type) Source #
Instance details Defined in Fcf type Eval (Bimap f g (Left x :: Either a1 b) :: Either a2 b' -> Type) = (Left (Eval (f x)) :: Either a2 b')
type Eval (Bimap f g ((,) x y) :: (k2, k1) -> Type) Source #
Instance details Defined in Fcf type Eval (Bimap f g ((,) x y) :: (k2, k1) -> Type) = (,) (Eval (f x)) (Eval (g y))

data UnBool :: Exp a -> Exp a -> Bool -> Exp a Source #

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

Instances

type Eval (UnBool fal tru True :: a -> Type) Source #
Instance details Defined in Fcf type Eval (UnBool fal tru True :: a -> Type) = Eval tru
type Eval (UnBool fal tru False :: a -> Type) Source #
Instance details Defined in Fcf type Eval (UnBool fal tru False :: a -> Type) = Eval fal

Primitives

data (||) :: Bool -> Bool -> Exp Bool infixr 2 Source #

Instances

type Eval (False \|\| b :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (False \|\| b :: Bool -> Type) = b
type Eval (True \|\| b :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (True \|\| b :: Bool -> Type) = True
type Eval (a \|\| False :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (a \|\| False :: Bool -> Type) = a
type Eval (a \|\| True :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (a \|\| True :: Bool -> Type) = True

data (&&) :: Bool -> Bool -> Exp Bool infixr 3 Source #

Instances

type Eval (False && b :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (False && b :: Bool -> Type) = False
type Eval (True && b :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (True && b :: Bool -> Type) = b
type Eval (a && True :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (a && True :: Bool -> Type) = a
type Eval (a && False :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (a && False :: Bool -> Type) = False

Other

data Error :: Symbol -> Exp a Source #

Instances

type Eval (Error msg :: a -> Type) Source #
Instance details Defined in Fcf type Eval (Error msg :: a -> Type) = (TypeError (Text msg) :: a)

data Collapse :: [Constraint] -> Exp Constraint Source #

Instances

type Eval (Collapse (a ': as) :: Constraint -> Type) Source #
Instance details Defined in Fcf type Eval (Collapse (a ': as) :: Constraint -> Type) = (a, Eval (Collapse as))
type Eval (Collapse ([] :: [Constraint])) Source #
Instance details Defined in Fcf type Eval (Collapse ([] :: [Constraint])) = () ~ ()

data TyEq :: a -> b -> Exp Bool Source #

Instances

type Eval (TyEq a b :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (TyEq a b :: Bool -> Type) = TyEqImpl a b

type family TyEqImpl (a :: k) (b :: k) :: Bool where ... Source #

Equations

TyEqImpl a a = True
TyEqImpl a b = False

data ($) :: (a -> Exp b) -> a -> Exp b infixr 0 Source #

Instances

type Eval (f $ a3 :: a2 -> Type) Source #
Instance details Defined in Fcf type Eval (f $ a3 :: a2 -> Type) = Eval (f a3)

Helpful shorthands

type (@@) f x = Eval (f x) Source #

Apply and evaluate a unary type function.

Reification

class IsBool (b :: Bool) where Source #

Minimal complete definition

_If

Methods

_If :: (b ~ True => r) -> (b ~ False => r) -> r Source #

Instances

IsBool False Source #
Instance details Defined in Fcf Methods _If :: ((False ~ True) -> r) -> ((False ~ False) -> r) -> r Source #
IsBool True Source #
Instance details Defined in Fcf Methods _If :: ((True ~ True) -> r) -> ((True ~ False) -> r) -> r Source #

type family If (b :: Bool) (x :: k) (y :: k) :: k Source #

Instances

type If False (_x :: k) (y :: k) Source #
Instance details Defined in Fcf type If False (_x :: k) (y :: k) = y
type If True (x :: k) (_y :: k) Source #
Instance details Defined in Fcf type If True (x :: k) (_y :: k) = x

type Eval (False \|\| b :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (False \|\| b :: Bool -> Type) = b
type Eval (True \|\| b :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (True \|\| b :: Bool -> Type) = True
type Eval (a \|\| False :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (a \|\| False :: Bool -> Type) = a
type Eval (a \|\| True :: Bool -> Type) Source #
Instance details Defined in Fcf type Eval (a \|\| True :: Bool -> Type) = True