Fcf

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.

First-class type families

type Exp a = a -> Type

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

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

Expression evaluator.

Instances

type Eval (False && b :: Bool -> Type)

Defined in Fcf

type Eval (False && b :: Bool -> Type) = False

type Eval (True && b :: Bool -> Type)

Defined in Fcf

type Eval (True && b :: Bool -> Type) = b

type Eval (a && True :: Bool -> Type)

Defined in Fcf

type Eval (a && True :: Bool -> Type) = a

type Eval (a && False :: Bool -> Type)

Defined in Fcf

type Eval (a && False :: Bool -> Type) = False

type Eval (False || b :: Bool -> Type)

Defined in Fcf

type Eval (False || b :: Bool -> Type) = b

type Eval (True || b :: Bool -> Type)

Defined in Fcf

type Eval (True || b :: Bool -> Type) = True

type Eval (a || False :: Bool -> Type)

Defined in Fcf

type Eval (a || False :: Bool -> Type) = a

type Eval (a || True :: Bool -> Type)

Defined in Fcf

type Eval (a || True :: Bool -> Type) = True

type Eval (Pure x :: a -> Type)

Defined in Fcf

type Eval (Pure x :: a -> Type) = x

type Eval (Join e :: a -> Type)

Defined in Fcf

type Eval (Join e :: a -> Type) = Eval (Eval e)

type Eval (Pure1 f x :: a2 -> Type)

Defined in Fcf

type Eval (Pure1 f x :: a2 -> Type) = f x

type Eval (k =<< e :: a2 -> Type)

Defined in Fcf

type Eval (k =<< e :: a2 -> Type) = Eval (k (Eval e))

type Eval (f <$> e :: a2 -> Type)

Defined in Fcf

type Eval (f <$> e :: a2 -> Type) = f (Eval e)

type Eval (f <*> e :: a2 -> Type)

Defined in Fcf

type Eval (f <*> e :: a2 -> Type) = Eval f (Eval e)

type Eval (UnBool fal tru True :: a -> Type)

Defined in Fcf

type Eval (UnBool fal tru True :: a -> Type) = Eval tru

type Eval (UnBool fal tru False :: a -> Type)

Defined in Fcf

type Eval (UnBool fal tru False :: a -> Type) = Eval fal

type Eval (Uncurry f ((,) x y) :: a2 -> Type)

Defined in Fcf

type Eval (Uncurry f ((,) x y) :: a2 -> Type) = Eval (f x y)

type Eval (UnMaybe y f (Just x) :: a2 -> Type)

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)

Defined in Fcf

type Eval (UnMaybe y f (Nothing :: Maybe a1) :: a2 -> Type) = Eval y

type Eval (Foldr f y (x ': xs) :: a2 -> Type)

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)

Defined in Fcf

type Eval (Foldr f y ([] :: [a1]) :: a2 -> Type) = y

type Eval (UnList y f xs :: a2 -> Type)

Defined in Fcf

type Eval (UnList y f xs :: a2 -> Type) = Eval (Foldr f y xs)

type Eval (Pure2 f x y :: a2 -> Type)

Defined in Fcf

type Eval (Pure2 f x y :: a2 -> Type) = f x y

type Eval ((f <=< g) x :: a3 -> Type)

Defined in Fcf

type Eval ((f <=< g) x :: a3 -> Type) = Eval (f (Eval (g x)))

type Eval (Flip f y x :: a2 -> Type)

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)

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)

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)

Defined in Fcf

type Eval (Pure3 f x y z :: a2 -> Type) = f x y z

type Eval (Traverse f (x ': xs) :: [b] -> Type)

Defined in Fcf

type Eval (Traverse f (x ': xs) :: [b] -> Type) = Eval (f x) ': Eval (Traverse f xs)

type Eval (Traverse f ([] :: [a]) :: [b] -> Type)

Defined in Fcf

type Eval (Traverse f ([] :: [a]) :: [b] -> Type) = ([] :: [b])

type Eval (BimapEither f g (Right y :: Either a b1) :: Either a' b2 -> Type)

Defined in Fcf

type Eval (BimapEither f g (Right y :: Either a b1) :: Either a' b2 -> Type) = (Right (Eval (g y)) :: Either a' b2)

type Eval (BimapEither f g (Left x :: Either a1 b) :: Either a2 b' -> Type)

Defined in Fcf

type Eval (BimapEither f g (Left x :: Either a1 b) :: Either a2 b' -> Type) = (Left (Eval (f x)) :: Either a2 b')

type Eval (BimapPair f g ((,) x y) :: (k2, k1) -> Type)

Defined in Fcf

type Eval (BimapPair f g ((,) x y) :: (k2, k1) -> Type) = (,) (Eval (f x)) (Eval (g y))

Monadic operations

data Pure :: a -> Exp a

Instances

type Eval (Pure x :: a -> Type)

Defined in Fcf

type Eval (Pure x :: a -> Type) = x

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

Instances

type Eval (Pure1 f x :: a2 -> Type)

Defined in Fcf

type Eval (Pure1 f x :: a2 -> Type) = f x

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

Instances

type Eval (Pure2 f x y :: a2 -> Type)

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

Instances

type Eval (Pure3 f x y z :: a2 -> Type)

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

Instances

type Eval (k =<< e :: a2 -> Type)

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

Instances

type Eval ((f <=< g) x :: a3 -> Type)

Defined in Fcf

type Eval ((f <=< g) x :: a3 -> Type) = Eval (f (Eval (g x)))

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

Instances

type Eval (Join e :: a -> Type)

Defined in Fcf

type Eval (Join e :: a -> Type) = Eval (Eval e)

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

Instances

type Eval (f <$> e :: a2 -> Type)

Defined in Fcf

type Eval (f <$> e :: a2 -> Type) = f (Eval e)

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

Instances

type Eval (f <*> e :: a2 -> Type)

Defined in Fcf

type Eval (f <*> e :: a2 -> Type) = Eval f (Eval e)

More higher-order combinators

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

Instances

type Eval (Flip f y x :: a2 -> Type)

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

Instances

type Eval (Uncurry f ((,) x y) :: a2 -> Type)

Defined in Fcf

type Eval (Uncurry f ((,) x y) :: a2 -> Type) = Eval (f x y)

data BimapPair :: (a -> Exp a') -> (b -> Exp b') -> (a, b) -> Exp (a', b')

Instances

type Eval (BimapPair f g ((,) x y) :: (k2, k1) -> Type)

Defined in Fcf

type Eval (BimapPair f g ((,) x y) :: (k2, k1) -> Type) = (,) (Eval (f x)) (Eval (g y))

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

Instances

type Eval (UnEither f g (Right y :: Either a2 b) :: a1 -> Type)

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)

Defined in Fcf

type Eval (UnEither f g (Left x :: Either a2 b) :: a1 -> Type) = Eval (f x)

data BimapEither :: (a -> Exp a') -> (b -> Exp b') -> Either a b -> Exp (Either a' b')

Instances

type Eval (BimapEither f g (Right y :: Either a b1) :: Either a' b2 -> Type)

Defined in Fcf

type Eval (BimapEither f g (Right y :: Either a b1) :: Either a' b2 -> Type) = (Right (Eval (g y)) :: Either a' b2)

type Eval (BimapEither f g (Left x :: Either a1 b) :: Either a2 b' -> Type)

Defined in Fcf

type Eval (BimapEither f g (Left x :: Either a1 b) :: Either a2 b' -> Type) = (Left (Eval (f x)) :: Either a2 b')

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

Instances

type Eval (UnMaybe y f (Just x) :: a2 -> Type)

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)

Defined in Fcf

type Eval (UnMaybe y f (Nothing :: Maybe a1) :: a2 -> Type) = Eval y

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

Instances

type Eval (Foldr f y (x ': xs) :: a2 -> Type)

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)

Defined in Fcf

type Eval (Foldr f y ([] :: [a1]) :: a2 -> Type) = y

data Traverse :: (a -> Exp b) -> [a] -> Exp [b]

Instances

type Eval (Traverse f (x ': xs) :: [b] -> Type)

Defined in Fcf

type Eval (Traverse f (x ': xs) :: [b] -> Type) = Eval (f x) ': Eval (Traverse f xs)

type Eval (Traverse f ([] :: [a]) :: [b] -> Type)

Defined in Fcf

type Eval (Traverse f ([] :: [a]) :: [b] -> Type) = ([] :: [b])

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

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

Instances

type Eval (UnList y f xs :: a2 -> Type)

Defined in Fcf

type Eval (UnList y f xs :: a2 -> Type) = Eval (Foldr f y xs)

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

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)

Defined in Fcf

type Eval (UnBool fal tru True :: a -> Type) = Eval tru

type Eval (UnBool fal tru False :: a -> Type)

Defined in Fcf

type Eval (UnBool fal tru False :: a -> Type) = Eval fal

Primitives

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

Instances

type Eval (False || b :: Bool -> Type)

Defined in Fcf

type Eval (False || b :: Bool -> Type) = b

type Eval (True || b :: Bool -> Type)

Defined in Fcf

type Eval (True || b :: Bool -> Type) = True

type Eval (a || False :: Bool -> Type)

Defined in Fcf

type Eval (a || False :: Bool -> Type) = a

type Eval (a || True :: Bool -> Type)

Defined in Fcf

type Eval (a || True :: Bool -> Type) = True

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

Instances

type Eval (False && b :: Bool -> Type)

Defined in Fcf

type Eval (False && b :: Bool -> Type) = False

type Eval (True && b :: Bool -> Type)

Defined in Fcf

type Eval (True && b :: Bool -> Type) = b

type Eval (a && True :: Bool -> Type)

Defined in Fcf

type Eval (a && True :: Bool -> Type) = a

type Eval (a && False :: Bool -> Type)

Defined in Fcf

type Eval (a && False :: Bool -> Type) = False

Helpful shorthands

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

Apply and evaluate a unary type function.

Reification

class IsBool (b :: Bool) where

Minimal complete definition

_If

Methods

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

Instances

IsBool False

Defined in Fcf

Methods

_If :: ((False ~ True) -> r) -> ((False ~ False) -> r) -> r

IsBool True

Defined in Fcf

Methods

_If :: ((True ~ True) -> r) -> ((True ~ False) -> r) -> r

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

Instances

type If False (_x :: k) (y :: k)

Defined in Fcf

type If False (_x :: k) (y :: k) = y

type If True (x :: k) (_y :: k)

Defined in Fcf

type If True (x :: k) (_y :: k) = x