Test.TypeSpec.Internal.Apply

Useful abstractions for type level programming using. This reimplements parts of the singletons library, which is just too heavy of a dependency to carry around, when only three small types are used of it.

Documentation

type family (ma :: monad a) >>= (f :: a ~> (monad b :: Type)) :: monad b

Bind to actions.

Instances

type (>>=) b (Either a1) a (Left a1 a b1) f

type (>>=) b (Either a1) a (Left a1 a b1) f = Left a1 b b1

type (>>=) b (Either a) a1 (Right a a1 a2) f

type (>>=) b (Either a) a1 (Right a a1 a2) f = Apply a1 (Either a b) f a2

type (>>) ma mb = ma >>= Const' mb

Execute one action and then the next, ignore the result of the first.

type family (f :: m (a ~> b)) <*> (ma :: m a) :: m b where ...

Execute an action that returns a function than map function over the result of the next action.

Equations

mf <*> mx = mf >>= Apply (Flip (<$>$$)) mx

Tuple construction

data Pair'' :: a ~> (b ~> (a, b))

Instances

type Apply a ((~>) b (a, b)) (Pair'' a b) x

type Apply a ((~>) b (a, b)) (Pair'' a b) x = Pair' b a x

data Pair' :: a -> b ~> (a, b)

Instances

type Apply k1 (k, k1) (Pair' k1 k x) y

type Apply k1 (k, k1) (Pair' k1 k x) y = (,) k k1 x y

List construction

data Cons'' :: a ~> ([a] ~> [a])

Instances

type Apply a ((~>) [a] [a]) (Cons'' a) x

type Apply a ((~>) [a] [a]) (Cons'' a) x = Cons' a x

data Cons' :: a -> [a] ~> [a]

Instances

type Apply [a] [a] (Cons' a x) xs

type Apply [a] [a] (Cons' a x) xs = (:) a x xs

Convert data types to Partially applicable type functions

data TyCon1 :: (a -> b) -> a ~> b

Instances

type Apply a b (TyCon1 b a f) x

type Apply a b (TyCon1 b a f) x = f x

data TyCon2 :: (a -> b -> c) -> a ~> (b ~> c)

Instances

type Apply a1 ((~>) a b) (TyCon2 b a a1 f) x

type Apply a1 ((~>) a b) (TyCon2 b a a1 f) x = TyCon1 b a (f x)

Execute an action and map a pure function over the result.

data (<$>$$) :: (a ~> b) ~> (m a ~> m b)

Instances

type Apply ((~>) a b) ((~>) (m a) (m b)) ((<$>$$) a m b) f

type Apply ((~>) a b) ((~>) (m a) (m b)) ((<$>$$) a m b) f = (<$>$) m a b f

data (<$>$) :: (a ~> b) -> m a ~> m b

Instances

type Apply (m a) (m b) ((<$>$) m a b f) x

type Apply (m a) (m b) ((<$>$) m a b f) x = (<$>) m a b f x

type family (f :: a ~> b) <$> (ma :: m a) :: m b

Instances

type (<$>) (Either a1) a b f (Left a1 a a2)

type (<$>) (Either a1) a b f (Left a1 a a2) = Left a1 b a2

type (<$>) (Either a) a1 b f (Right a a1 a2)

type (<$>) (Either a) a1 b f (Right a a1 a2) = Right a b (Apply a1 b f a2)

Flip Type Functions

data Flip' :: (a ~> (b ~> c)) ~> (b ~> (a ~> c))

Instances

type Apply ((~>) a ((~>) b c)) ((~>) b ((~>) a c)) (Flip' b a c) f

type Apply ((~>) a ((~>) b c)) ((~>) b ((~>) a c)) (Flip' b a c) f = Flip a b c f

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

Instances

type Apply b ((~>) a c) (Flip a b c f) y

type Apply b ((~>) a c) (Flip a b c f) y = Flip_ a b c f y

data Flip_ :: (a ~> (b ~> c)) -> b -> a ~> c

Instances

type Apply a c (Flip_ a b c f y) x

type Apply a c (Flip_ a b c f y) x = Flip__ a b c f y x

type family Flip__ (f :: a ~> (b ~> c)) (y :: b) (x :: a) :: c where ...

Equations

Flip__ f y x = Apply (Apply f x) y

Type Function composition

data Compose'' :: (b ~> c) ~> ((a ~> b) ~> (a ~> c))

Instances

type Apply ((~>) b c) ((~>) ((~>) a b) ((~>) a c)) (Compose'' b a c) f

type Apply ((~>) b c) ((~>) ((~>) a b) ((~>) a c)) (Compose'' b a c) f = Compose' a b c f

data Compose' :: (b ~> c) -> (a ~> b) ~> (a ~> c)

Instances

type Apply ((~>) a b) ((~>) a c) (Compose' a b c f) g

type Apply ((~>) a b) ((~>) a c) (Compose' a b c f) g = Compose a b c f g

data Compose :: (b ~> c) -> (a ~> b) -> a ~> c

Instances

type Apply a c (Compose a b c f g) x

type Apply a c (Compose a b c f g) x = Compose_ a b c f g x

type family Compose_ (f :: b ~> c) (g :: a ~> b) (x :: a) :: c where ...

Equations

Compose_ f g x = Apply f (Apply g x)

Type-Level const

type family Const (a :: t) (b :: t') :: t where ...

Equations

Const a b = a

data Const' :: a -> b ~> a

Instances

type Apply t' t (Const' t' t a) b

type Apply t' t (Const' t' t a) b = Const t' t a b

data Const'' :: a ~> (b ~> a)

Instances

type Apply a ((~>) b a) (Const'' b a) a1

type Apply a ((~>) b a) (Const'' b a) a1 = Const' b a a1

Defunctionalization

data TyFun :: Type -> Type -> Type

Instances

type Apply a ((~>) [a] [a]) (Cons'' a) x

type Apply a ((~>) [a] [a]) (Cons'' a) x = Cons' a x

type Apply a ((~>) b a) (Const'' b a) a1

type Apply a ((~>) b a) (Const'' b a) a1 = Const' b a a1

type Apply a ((~>) b (a, b)) (Pair'' a b) x

type Apply a ((~>) b (a, b)) (Pair'' a b) x = Pair' b a x

type Apply b ((~>) a c) (Flip a b c f) y

type Apply b ((~>) a c) (Flip a b c f) y = Flip_ a b c f y

type Apply a1 ((~>) a b) (TyCon2 b a a1 f) x

type Apply a1 ((~>) a b) (TyCon2 b a a1 f) x = TyCon1 b a (f x)

type Apply ((~>) b c) ((~>) ((~>) a b) ((~>) a c)) (Compose'' b a c) f

type Apply ((~>) b c) ((~>) ((~>) a b) ((~>) a c)) (Compose'' b a c) f = Compose' a b c f

type Apply ((~>) a ((~>) b c)) ((~>) b ((~>) a c)) (Flip' b a c) f

type Apply ((~>) a ((~>) b c)) ((~>) b ((~>) a c)) (Flip' b a c) f = Flip a b c f

type Apply ((~>) a b) ((~>) (m a) (m b)) ((<$>$$) a m b) f

type Apply ((~>) a b) ((~>) (m a) (m b)) ((<$>$$) a m b) f = (<$>$) m a b f

type Apply ((~>) a b) ((~>) a c) (Compose' a b c f) g

type Apply ((~>) a b) ((~>) a c) (Compose' a b c f) g = Compose a b c f g

type (~>) a b = TyFun a b -> Type infixr 0

type family Apply (f :: a ~> b) (x :: a) :: b

Instances

type Apply t' t (Const' t' t a) b

type Apply t' t (Const' t' t a) b = Const t' t a b

type Apply a b (TyCon1 b a f) x

type Apply a b (TyCon1 b a f) x = f x

type Apply a c (Compose a b c f g) x

type Apply a c (Compose a b c f g) x = Compose_ a b c f g x

type Apply a c (Flip_ a b c f y) x

type Apply a c (Flip_ a b c f y) x = Flip__ a b c f y x

type Apply a ((~>) [a] [a]) (Cons'' a) x

type Apply a ((~>) [a] [a]) (Cons'' a) x = Cons' a x

type Apply a ((~>) b a) (Const'' b a) a1

type Apply a ((~>) b a) (Const'' b a) a1 = Const' b a a1

type Apply a ((~>) b (a, b)) (Pair'' a b) x

type Apply a ((~>) b (a, b)) (Pair'' a b) x = Pair' b a x

type Apply k1 (k, k1) (Pair' k1 k x) y

type Apply k1 (k, k1) (Pair' k1 k x) y = (,) k k1 x y

type Apply b ((~>) a c) (Flip a b c f) y

type Apply b ((~>) a c) (Flip a b c f) y = Flip_ a b c f y

type Apply a1 ((~>) a b) (TyCon2 b a a1 f) x

type Apply a1 ((~>) a b) (TyCon2 b a a1 f) x = TyCon1 b a (f x)

type Apply [a] [a] (Cons' a x) xs

type Apply [a] [a] (Cons' a x) xs = (:) a x xs

type Apply (m a) (m b) ((<$>$) m a b f) x

type Apply (m a) (m b) ((<$>$) m a b f) x = (<$>) m a b f x

type Apply ((~>) b c) ((~>) ((~>) a b) ((~>) a c)) (Compose'' b a c) f

type Apply ((~>) b c) ((~>) ((~>) a b) ((~>) a c)) (Compose'' b a c) f = Compose' a b c f

type Apply ((~>) a ((~>) b c)) ((~>) b ((~>) a c)) (Flip' b a c) f

type Apply ((~>) a ((~>) b c)) ((~>) b ((~>) a c)) (Flip' b a c) f = Flip a b c f

type Apply ((~>) a b) ((~>) (m a) (m b)) ((<$>$$) a m b) f

type Apply ((~>) a b) ((~>) (m a) (m b)) ((<$>$$) a m b) f = (<$>$) m a b f

type Apply ((~>) a b) ((~>) a c) (Compose' a b c f) g

type Apply ((~>) a b) ((~>) a c) (Compose' a b c f) g = Compose a b c f g