Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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 instanceEval
(FromMaybe a 'Nothing) = a type instanceEval
(FromMaybe a ('Just b)) = b
Essential language extensions for Fcf:
{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}
Synopsis
- type Exp a = a -> Type
- type family Eval (e :: Exp a) :: a
- type (@@) (f :: k1 -> Exp k) (x :: k1) = Eval (f x)
- data Pure (b :: a) (c :: a)
- data Pure1 (c :: a -> b) (d :: a) (e :: b)
- data Pure2 (d :: a -> b -> c) (e :: a) (f :: b) (g :: c)
- data Pure3 (e :: a -> b -> c -> d) (f :: a) (g :: b) (h :: c) (i :: d)
- data ((c :: a -> Exp b) =<< (d :: Exp a)) (e :: b)
- data ((d :: b -> Exp c) <=< (e :: a -> Exp b)) (f :: a) (g :: c)
- type LiftM = (=<<) :: (a -> Exp b) -> Exp a -> b -> Type
- data LiftM2 (d :: a -> b -> Exp c) (e :: Exp a) (f :: Exp b) (g :: c)
- data LiftM3 (e :: a -> b -> c -> Exp d) (f :: Exp a) (g :: Exp b) (h :: Exp c) (i :: d)
- data Join (b :: Exp (Exp a)) (c :: a)
- data ((c :: a -> b) <$> (d :: Exp a)) (e :: b)
- data ((c :: Exp (a -> b)) <*> (d :: Exp a)) (e :: b)
- data Flip (d :: a -> b -> Exp c) (e :: b) (f :: a) (g :: c)
- data ConstFn (c :: a) (d :: b) (e :: a)
- data ((c :: a -> Exp b) $ (d :: a)) (e :: b)
- data Uncurry (d :: a -> b -> Exp c) (e :: (a, b)) (f :: c)
- data Fst (c :: (a, b)) (d :: a)
- data Snd (c :: (a, b)) (d :: b)
- data ((a :: b -> Exp c) *** (d :: b' -> Exp c')) (e :: (b, b')) (f :: (c, c'))
- data UnEither (d :: a -> Exp c) (e :: b -> Exp c) (f :: Either a b) (g :: c)
- data IsLeft (c :: Either a b) (d :: Bool)
- data IsRight (c :: Either a b) (d :: Bool)
- data UnMaybe (c :: Exp b) (d :: a -> Exp b) (e :: Maybe a) (f :: b)
- data FromMaybe (a :: k) (b :: Maybe k) (c :: k)
- data IsNothing (b :: Maybe a) (c :: Bool)
- data IsJust (b :: Maybe a) (c :: Bool)
- data Foldr (c :: a -> b -> Exp b) (d :: b) (e :: t a) (f :: b)
- data UnList (c :: b) (d :: a -> b -> Exp b) (e :: [a]) (f :: b)
- data ((b :: [a]) ++ (c :: [a])) (d :: [a])
- data Filter (b :: a -> Exp Bool) (c :: [a]) (d :: [a])
- data Head (b :: [a]) (c :: Maybe a)
- data Tail (b :: [a]) (c :: Maybe [a])
- data Null (b :: [a]) (c :: Bool)
- data Length (b :: [a]) (c :: Nat)
- data Find (b :: a -> Exp Bool) (c :: [a]) (d :: Maybe a)
- data FindIndex (b :: a -> Exp Bool) (c :: [a]) (d :: Maybe Nat)
- data Lookup (a :: k) (c :: [(k, b)]) (d :: Maybe b)
- data SetIndex (b :: Nat) (c :: a) (d :: [a]) (e :: [a])
- data ZipWith (d :: a -> b -> Exp c) (e :: [a]) (f :: [b]) (g :: [c])
- data Zip (c :: [a]) (d :: [b]) (e :: [(a, b)])
- data Unzip (c :: Exp [(a, b)]) (d :: ([a], [b]))
- data Cons2 (c :: (a, b)) (d :: ([a], [b])) (e :: ([a], [b]))
- data UnBool (b :: Exp a) (c :: Exp a) (d :: Bool) (e :: a)
- data ((a :: Bool) || (b :: Bool)) (c :: Bool)
- data ((a :: Bool) && (b :: Bool)) (c :: Bool)
- data Not (a :: Bool) (b :: Bool)
- data Case (a :: [Match j k]) (b :: j) (c :: k)
- data Match j k
- type (-->) = 'Match_ :: j -> k -> Match j k
- type Is = 'Is_ :: (j -> Exp Bool) -> k -> Match j k
- type Any = 'Any_ :: k -> Match j k
- type Else = 'Else_ :: (j -> Exp k) -> Match j k
- data ((a :: Nat) + (b :: Nat)) (c :: Nat)
- data ((a :: Nat) - (b :: Nat)) (c :: Nat)
- data ((a :: Nat) * (b :: Nat)) (c :: Nat)
- data ((a :: Nat) ^ (b :: Nat)) (c :: Nat)
- data ((a :: Nat) <= (b :: Nat)) (c :: Bool)
- data ((a :: Nat) >= (b :: Nat)) (c :: Bool)
- data ((a :: Nat) < (b :: Nat)) (c :: Bool)
- data ((a :: Nat) > (b :: Nat)) (c :: Bool)
- data Map (c :: a -> Exp b) (d :: f a) (e :: f b)
- data Bimap (c :: a -> Exp a') (d :: b -> Exp b') (e :: f a b) (g :: f a' b')
- data Error (b :: Symbol) (c :: a)
- data Constraints (a :: [Constraint]) b
- data TyEq (c :: a) (d :: b) (e :: Bool)
- type family Stuck :: a
- class IsBool (b :: Bool) where
- type family If (cond :: Bool) (tru :: k) (fls :: k) :: k where ...
First-class type families
type family Eval (e :: Exp a) :: a Source #
Expression evaluator.
Instances
type Eval (Not 'False) Source # | |
Defined in Fcf.Data.Bool | |
type Eval (Not 'True) Source # | |
Defined in Fcf.Data.Bool | |
type Eval (Constraints (a ': as) :: Constraint -> Type) Source # | |
Defined in Fcf.Utils | |
type Eval (Constraints ('[] :: [Constraint])) Source # | |
Defined in Fcf.Utils | |
type Eval (MEmpty_ :: a -> Type) Source # | |
Defined in Fcf.Class.Monoid | |
type Eval (Sum ns :: Nat -> Type) Source # | |
type Eval (Length ('[] :: [a]) :: Nat -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Length (a2 ': as) :: Nat -> Type) Source # | |
type Eval (a * b :: Nat -> Type) Source # | |
type Eval (a + b :: Nat -> Type) Source # | |
type Eval (a - b :: Nat -> Type) Source # | |
type Eval (a ^ b :: Nat -> Type) Source # | |
type Eval (And lst :: Bool -> Type) Source # | |
type Eval (Or lst :: Bool -> Type) Source # | |
type Eval ('False && b :: Bool -> Type) Source # | |
type Eval ('True && b :: Bool -> Type) Source # | |
type Eval (a && 'False :: Bool -> Type) Source # | |
type Eval (a && 'True :: Bool -> Type) Source # | |
type Eval ('False || b :: Bool -> Type) Source # | |
type Eval ('True || b :: Bool -> Type) Source # | |
type Eval (a || 'False :: Bool -> Type) Source # | |
type Eval (a || 'True :: Bool -> Type) Source # | |
type Eval (IsJust ('Just _a) :: Bool -> Type) Source # | |
type Eval (IsJust ('Nothing :: Maybe a) :: Bool -> Type) Source # | |
type Eval (IsNothing ('Just _a) :: Bool -> Type) Source # | |
type Eval (IsNothing ('Nothing :: Maybe a) :: Bool -> Type) Source # | |
type Eval (Null ('[] :: [a]) :: Bool -> Type) Source # | |
type Eval (Null (a2 ': as) :: Bool -> Type) Source # | |
type Eval (a < b :: Bool -> Type) Source # | |
type Eval (a <= b :: Bool -> Type) Source # | |
type Eval (a > b :: Bool -> Type) Source # | |
type Eval (a >= b :: Bool -> Type) Source # | |
type Eval (Join e :: a -> Type) Source # | |
type Eval (Pure x :: a -> Type) Source # | |
Defined in Fcf.Combinators | |
type Eval (Error msg :: a -> Type) Source # | |
type Eval (TError msg :: a -> Type) Source # | |
type Eval (Compare ('Left _a :: Either a b) ('Right _b :: Either a b) :: Ordering -> Type) Source # | |
type Eval (Compare ('Right _a :: Either a b) ('Left _b :: Either a b) :: Ordering -> Type) Source # | |
type Eval (Compare ('Left a2 :: Either a1 b1) ('Left b2 :: Either a1 b1) :: Ordering -> Type) Source # | |
type Eval (Compare ('Right a3 :: Either a2 a1) ('Right b :: Either a2 a1) :: Ordering -> Type) Source # | |
type Eval (Compare 'EQ 'GT) Source # | |
type Eval (Compare 'EQ 'LT) Source # | |
type Eval (Compare 'GT 'EQ) Source # | |
type Eval (Compare 'GT 'LT) Source # | |
type Eval (Compare 'LT 'EQ) Source # | |
type Eval (Compare 'LT 'GT) Source # | |
type Eval (Compare a a :: Ordering -> Type) Source # | |
type Eval (Compare ('Just _a) ('Nothing :: Maybe a) :: Ordering -> Type) Source # | |
type Eval (Compare ('Nothing :: Maybe a) ('Just _b) :: Ordering -> Type) Source # | |
type Eval (Compare ('Nothing :: Maybe a) ('Nothing :: Maybe a) :: Ordering -> Type) Source # | |
type Eval (Compare ('Just a2) ('Just b) :: Ordering -> Type) Source # | |
type Eval (Compare a b :: Ordering -> Type) Source # | |
type Eval (Compare '(a3, a4) '(b1, b2) :: Ordering -> Type) Source # | |
type Eval (Compare '(a4, a5, a6) '(b1, b2, b3) :: Ordering -> Type) Source # | |
type Eval (Compare a b :: Ordering -> Type) Source # | |
type Eval (Compare 'False 'True) Source # | |
type Eval (Compare 'True 'False) Source # | |
type Eval (Compare a a :: Ordering -> Type) Source # | |
type Eval (Compare (_x ': _xs) ('[] :: [a]) :: Ordering -> Type) Source # | |
type Eval (Compare (x ': xs) (y ': ys) :: Ordering -> Type) Source # | |
type Eval (Compare ('[] :: [a]) (_y ': _ys) :: Ordering -> Type) Source # | |
type Eval (Compare ('[] :: [a]) ('[] :: [a]) :: Ordering -> Type) Source # | |
type Eval (Compare a b :: Ordering -> Type) Source # | |
type Eval (a2 < b :: Bool -> Type) Source # | |
Defined in Fcf.Class.Ord | |
type Eval (a2 <= b :: Bool -> Type) Source # | |
Defined in Fcf.Class.Ord | |
type Eval (a2 > b :: Bool -> Type) Source # | |
Defined in Fcf.Class.Ord | |
type Eval (a2 >= b :: Bool -> Type) Source # | |
Defined in Fcf.Class.Ord | |
type Eval (IsLeft ('Left _a :: Either a b) :: Bool -> Type) Source # | |
type Eval (IsLeft ('Right _a :: Either a b) :: Bool -> Type) Source # | |
type Eval (IsRight ('Left _a :: Either a b) :: Bool -> Type) Source # | |
type Eval (IsRight ('Right _a :: Either a b) :: Bool -> Type) Source # | |
type Eval (Elem a2 as :: Bool -> Type) Source # | |
type Eval (IsInfixOf xs ys :: Bool -> Type) Source # | |
type Eval (IsPrefixOf xs ys :: Bool -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (IsSuffixOf xs ys :: Bool -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Concat xs :: a -> Type) Source # | |
type Eval (x .<> y :: a -> Type) Source # | |
Defined in Fcf.Class.Monoid | |
type Eval (FromMaybe _a ('Just b) :: a -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (FromMaybe a2 ('Nothing :: Maybe a1) :: a1 -> Type) Source # | |
type Eval (Fst '(a2, _b) :: a1 -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (Snd '(_a, b) :: a2 -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (All p lst :: Bool -> Type) Source # | |
type Eval (Any p lst :: Bool -> Type) Source # | |
type Eval (TyEq a b :: Bool -> Type) Source # | |
type Eval (UnBool fal tru 'False :: a -> Type) Source # | |
type Eval (UnBool fal tru 'True :: a -> Type) Source # | |
type Eval (ConstFn a2 _b :: a1 -> Type) Source # | |
Defined in Fcf.Combinators | |
type Eval (f $ a3 :: a2 -> Type) Source # | |
Defined in Fcf.Combinators | |
type Eval (f <$> e :: a2 -> Type) Source # | |
Defined in Fcf.Combinators | |
type Eval (f <*> e :: a2 -> Type) Source # | |
type Eval (k =<< e :: a2 -> Type) Source # | |
type Eval (e >>= k :: a2 -> Type) Source # | |
type Eval (Pure1 f x :: a2 -> Type) Source # | |
Defined in Fcf.Combinators | |
type Eval (x & f :: a2 -> Type) Source # | |
Defined in Fcf.Data.Function | |
type Eval (Case ms a :: k -> Type) Source # | |
type Eval (UnMaybe y f ('Just x) :: a1 -> Type) Source # | |
type Eval (UnMaybe y f ('Nothing :: Maybe a2) :: a1 -> Type) Source # | |
type Eval (UnList y f xs :: a1 -> Type) Source # | |
type Eval (FoldMap f ('Left _a :: Either a3 a1) :: a2 -> Type) Source # | |
type Eval (FoldMap f ('Right x :: Either a3 a1) :: a2 -> Type) Source # | |
type Eval (FoldMap f ('Just x) :: a2 -> Type) Source # | |
type Eval (FoldMap f ('Nothing :: Maybe a1) :: a2 -> Type) Source # | |
type Eval (FoldMap f (x ': xs) :: a2 -> Type) Source # | |
type Eval (FoldMap f ('[] :: [a1]) :: a2 -> Type) Source # | |
Defined in Fcf.Class.Foldable | |
type Eval (Uncurry f '(x, y) :: a2 -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (Foldr f y ('Left _a :: Either a3 a1) :: a2 -> Type) Source # | |
type Eval (Foldr f y ('Right x :: Either a3 a1) :: a2 -> Type) Source # | |
type Eval (Foldr f y ('Just x) :: a2 -> Type) Source # | |
type Eval (Foldr f y ('Nothing :: Maybe a1) :: a2 -> Type) Source # | |
type Eval (Foldr f y (x ': xs) :: a2 -> Type) Source # | |
type Eval (Foldr f y ('[] :: [a1]) :: a2 -> Type) Source # | |
Defined in Fcf.Class.Foldable | |
type Eval ((f <=< g) x :: a2 -> Type) Source # | |
type Eval (Flip f y x :: a2 -> Type) Source # | |
Defined in Fcf.Combinators | |
type Eval (Pure2 f x y :: a2 -> Type) Source # | |
Defined in Fcf.Combinators | |
type Eval (UnEither f g ('Left x :: Either a1 b) :: a2 -> Type) Source # | |
type Eval (UnEither f g ('Right y :: Either a1 b) :: a2 -> Type) Source # | |
type Eval (LiftM2 f x y :: a3 -> Type) Source # | |
type Eval (On r f x y :: a2 -> Type) Source # | |
type Eval (Pure3 f x y z :: a2 -> Type) Source # | |
Defined in Fcf.Combinators | |
type Eval (LiftM3 f x y z :: a4 -> Type) Source # | |
type Eval (Bicomap f g r x y :: a4 -> Type) Source # | |
type Eval (Init ('[] :: [a]) :: Maybe [a] -> Type) Source # | |
type Eval (Tail (_a ': as) :: Maybe [a] -> Type) Source # | |
type Eval (Tail ('[] :: [a]) :: Maybe [a] -> Type) Source # | |
type Eval (Init (a2 ': (b ': as)) :: Maybe [a1] -> Type) Source # | |
type Eval (Init '[a2] :: Maybe [a1] -> Type) Source # | |
type Eval (Head ('[] :: [a]) :: Maybe a -> Type) Source # | |
type Eval (Last ('[] :: [a]) :: Maybe a -> Type) Source # | |
type Eval (Head (a2 ': _as) :: Maybe a1 -> Type) Source # | |
type Eval (Last (a2 ': (b ': as)) :: Maybe a1 -> Type) Source # | |
type Eval (Last '[a2] :: Maybe a1 -> Type) Source # | |
type Eval (Tails ('[] :: [a]) :: [[a]] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Tails (a2 ': as) :: [[a1]] -> Type) Source # | |
type Eval (Reverse l :: [a] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (FindIndex _p ('[] :: [a]) :: Maybe Nat -> Type) Source # | |
type Eval (FindIndex p (a2 ': as) :: Maybe Nat -> Type) Source # | |
type Eval (Find _p ('[] :: [a]) :: Maybe a -> Type) Source # | |
type Eval (Find p (a2 ': as) :: Maybe a1 -> Type) Source # | |
type Eval (xs ++ ys :: [a] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Drop n as :: [a] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (DropWhile p (x ': xs) :: [a] -> Type) Source # | |
type Eval (DropWhile p ('[] :: [a]) :: [a] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Filter _p ('[] :: [a]) :: [a] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Intercalate xs xss :: [a] -> Type) Source # | |
Defined in Fcf.Data.List type Eval (Intercalate xs xss :: [a] -> Type) = Eval ((Concat :: [[a]] -> [a] -> Type) =<< Intersperse xs xss) | |
type Eval (Intersperse _1 ('[] :: [a]) :: [a] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Intersperse sep (x ': xs) :: [a] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Take n as :: [a] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (TakeWhile p (x ': xs) :: [a] -> Type) Source # | |
type Eval (TakeWhile p ('[] :: [a]) :: [a] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Cons a2 as :: [a1] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Filter p (a2 ': as) :: [a1] -> Type) Source # | |
type Eval (Replicate n a2 :: [a1] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Snoc lst a :: [k] -> Type) Source # | |
type Eval (Lookup a as :: Maybe b -> Type) Source # | |
type Eval (Zip as bs :: [(a, b)] -> Type) Source # | |
type Eval (Unfoldr f c :: [a] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (SetIndex n a' as :: [k] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Map f ('Just a3) :: Maybe a2 -> Type) Source # | |
type Eval (Map f ('Nothing :: Maybe a) :: Maybe b -> Type) Source # | |
type Eval (ConcatMap f xs :: [b] -> Type) Source # | |
type Eval (Map f ('[] :: [a]) :: [b] -> Type) Source # | |
Defined in Fcf.Class.Functor | |
type Eval (Map f (a2 ': as) :: [b] -> Type) Source # | |
type Eval (ZipWith _f ('[] :: [a]) _bs :: [c] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (ZipWith _f _as ('[] :: [b]) :: [c] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (ZipWith f (a2 ': as) (b2 ': bs) :: [c] -> Type) Source # | |
type Eval (Break p lst :: ([a], [a]) -> Type) Source # | |
type Eval (Partition p lst :: ([a], [a]) -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Span p lst :: ([a], [a]) -> Type) Source # | |
type Eval (Unzip as :: ([a], [b]) -> Type) Source # | |
type Eval (Cons2 '(a3, b) '(as, bs) :: ([a1], [a2]) -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Map f ('Left x :: Either a2 a1) :: Either a2 b -> Type) Source # | |
type Eval (Map f ('Right a3 :: Either a2 a1) :: Either a2 b -> Type) Source # | |
type Eval (Map f '(x, a2) :: (k2, k1) -> Type) Source # | |
Defined in Fcf.Class.Functor | |
type Eval ((f *** f') '(b2, b'2) :: (k1, k2) -> Type) Source # | |
type Eval (Second g x :: f a' b' -> Type) Source # | |
type Eval (First f2 x :: f1 a' b' -> Type) Source # | |
type Eval (Bimap f g ('Right y :: Either a b1) :: Either a' b2 -> Type) Source # | |
type Eval (Bimap f g ('Left x :: Either a1 b) :: Either a2 b' -> Type) Source # | |
type Eval (Bimap f g '(x, y) :: (k1, k2) -> Type) Source # | |
type Eval (Map f '(x, y, a2) :: (k2, k3, k1) -> Type) Source # | |
Defined in Fcf.Class.Functor | |
type Eval (Map f '(x, y, z, a2) :: (k2, k3, k4, k1) -> Type) Source # | |
Defined in Fcf.Class.Functor | |
type Eval (Map f '(x, y, z, w, a2) :: (k2, k3, k4, k5, k1) -> Type) Source # | |
Defined in Fcf.Class.Functor |
type (@@) (f :: k1 -> Exp k) (x :: k1) = Eval (f x) Source #
Apply and evaluate a unary type function.
Functional combinators
data ((c :: a -> Exp b) $ (d :: a)) (e :: b) infixr 0 Source #
Note that this denotes the identity function, so ($) f
can usually be
replaced with f
.
Operations on common types
Pairs
data ((a :: b -> Exp c) *** (d :: b' -> Exp c')) (e :: (b, b')) (f :: (c, c')) infixr 3 Source #
Specialization of Bimap
for pairs.
Either
data UnEither (d :: a -> Exp c) (e :: b -> Exp c) (f :: Either a b) (g :: c) Source #
Maybe
data UnMaybe (c :: Exp b) (d :: a -> Exp b) (e :: Maybe a) (f :: b) Source #
Lists
data Foldr (c :: a -> b -> Exp b) (d :: b) (e :: t a) (f :: b) Source #
Right fold.
Example
>>>
:kind! Eval (Foldr (+) 0 [1, 2, 3, 4])
Eval (Foldr (+) 0 [1, 2, 3, 4]) :: Natural = 10
Instances
type Eval (Foldr f y ('Left _a :: Either a3 a1) :: a2 -> Type) Source # | |
type Eval (Foldr f y ('Right x :: Either a3 a1) :: a2 -> Type) Source # | |
type Eval (Foldr f y ('Just x) :: a2 -> Type) Source # | |
type Eval (Foldr f y ('Nothing :: Maybe a1) :: a2 -> Type) Source # | |
type Eval (Foldr f y (x ': xs) :: a2 -> Type) Source # | |
type Eval (Foldr f y ('[] :: [a1]) :: a2 -> Type) Source # | |
Defined in Fcf.Class.Foldable |
data UnList (c :: b) (d :: a -> b -> Exp b) (e :: [a]) (f :: b) Source #
This is Foldr
with its argument flipped.
data ((b :: [a]) ++ (c :: [a])) (d :: [a]) Source #
List catenation.
Example
>>>
data Example where Ex :: a -> Example -- Hide the type of examples to avoid brittleness in different GHC versions
>>>
:kind! Ex (Eval ([1, 2] ++ [3, 4]) :: [Natural])
Ex (Eval ([1, 2] ++ [3, 4]) :: [Natural]) :: Example = Ex [1, 2, 3, 4]
data Filter (b :: a -> Exp Bool) (c :: [a]) (d :: [a]) Source #
Keep all elements that satisfy a predicate, remove all that don't.
Example
>>>
:kind! Eval (Filter ((>) 3) [1,2,3,0])
Eval (Filter ((>) 3) [1,2,3,0]) :: [Natural] = [1, 2, 0]
data Find (b :: a -> Exp Bool) (c :: [a]) (d :: Maybe a) Source #
Find Just
the first element satisfying a predicate, or evaluate to
Nothing
if no element satisfies the predicate.
Example
>>>
:kind! Eval (Find (TyEq 0) [1,2,3])
Eval (Find (TyEq 0) [1,2,3]) :: Maybe Natural = Nothing
>>>
:kind! Eval (Find (TyEq 0) [1,2,3,0])
Eval (Find (TyEq 0) [1,2,3,0]) :: Maybe Natural = Just 0
data FindIndex (b :: a -> Exp Bool) (c :: [a]) (d :: Maybe Nat) Source #
Find the index of an element satisfying the predicate.
Example
>>>
:kind! Eval (FindIndex ((<=) 3) [1,2,3,1,2,3])
Eval (FindIndex ((<=) 3) [1,2,3,1,2,3]) :: Maybe Natural = Just 2
>>>
:kind! Eval (FindIndex ((>) 0) [1,2,3,1,2,3])
Eval (FindIndex ((>) 0) [1,2,3,1,2,3]) :: Maybe Natural = Nothing
data Lookup (a :: k) (c :: [(k, b)]) (d :: Maybe b) Source #
Find an element associated with a key in an association list.
data SetIndex (b :: Nat) (c :: a) (d :: [a]) (e :: [a]) Source #
Modify an element at a given index.
The list is unchanged if the index is out of bounds.
Example
>>>
:kind! Eval (SetIndex 2 7 [1,2,3])
Eval (SetIndex 2 7 [1,2,3]) :: [Natural] = [1, 2, 7]
data ZipWith (d :: a -> b -> Exp c) (e :: [a]) (f :: [b]) (g :: [c]) Source #
Combine elements of two lists pairwise.
Example
>>>
:kind! Eval (ZipWith (+) [1,2,3] [1,1,1])
Eval (ZipWith (+) [1,2,3] [1,1,1]) :: [Natural] = [2, 3, 4]
data Cons2 (c :: (a, b)) (d :: ([a], [b])) (e :: ([a], [b])) Source #
Append elements to two lists. Used in the definition of Unzip
.
Bool
data UnBool (b :: Exp a) (c :: Exp a) (d :: Bool) (e :: 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
data ((a :: Bool) || (b :: Bool)) (c :: Bool) infixr 2 Source #
data ((a :: Bool) && (b :: Bool)) (c :: Bool) infixr 3 Source #
Case splitting
data Case (a :: [Match j k]) (b :: j) (c :: k) Source #
(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) ]
type Is = 'Is_ :: (j -> Exp Bool) -> k -> Match j k Source #
Match on predicate being successful with type in Case
.
type Any = 'Any_ :: k -> Match j k Source #
Match any type in Case
. Should be used as a final branch.
Note: this identifier conflicts with Any
(from Fcf.Class.Foldable)
Any
(from Data.Monoid), and Any
(from GHC.Exts).
We recommend importing this one qualified.
type Else = 'Else_ :: (j -> Exp k) -> Match j k Source #
Pass type being matched in Case
to subcomputation. Should be used as a
final branch.
Nat
Overloaded operations
data Map (c :: a -> Exp b) (d :: f a) (e :: f b) Source #
Type-level fmap
for type-level functors.
Note: this name clashes with Map
from containers.
FMap
is provided as a synonym to avoid this.
Example
>>>
data Example where Ex :: a -> Example -- Hide the type of examples to avoid brittleness in different GHC versions
>>>
data AddMul :: Nat -> Nat -> Exp Nat
>>>
type instance Eval (AddMul x y) = (x TL.+ y) TL.* (x TL.+ y)
>>>
:kind! Ex (Eval (Map (AddMul 2) '[0, 1, 2, 3, 4]) :: [Nat])
Ex (Eval (Map (AddMul 2) '[0, 1, 2, 3, 4]) :: [Nat]) :: Example = Ex [4, 9, 16, 25, 36]
Instances
type Eval (Map f ('Just a3) :: Maybe a2 -> Type) Source # | |
type Eval (Map f ('Nothing :: Maybe a) :: Maybe b -> Type) Source # | |
type Eval (Map f ('[] :: [a]) :: [b] -> Type) Source # | |
Defined in Fcf.Class.Functor | |
type Eval (Map f (a2 ': as) :: [b] -> Type) Source # | |
type Eval (Map f ('Left x :: Either a2 a1) :: Either a2 b -> Type) Source # | |
type Eval (Map f ('Right a3 :: Either a2 a1) :: Either a2 b -> Type) Source # | |
type Eval (Map f '(x, a2) :: (k2, k1) -> Type) Source # | |
Defined in Fcf.Class.Functor | |
type Eval (Map f '(x, y, a2) :: (k2, k3, k1) -> Type) Source # | |
Defined in Fcf.Class.Functor | |
type Eval (Map f '(x, y, z, a2) :: (k2, k3, k4, k1) -> Type) Source # | |
Defined in Fcf.Class.Functor | |
type Eval (Map f '(x, y, z, w, a2) :: (k2, k3, k4, k5, k1) -> Type) Source # | |
Defined in Fcf.Class.Functor |
data Bimap (c :: a -> Exp a') (d :: b -> Exp b') (e :: f a b) (g :: f a' b') Source #
Type-level bimap
.
Example
>>>
data Example where Ex :: a -> Example -- Hide the type of examples to avoid brittleness in different GHC versions
>>>
:kind! Ex (Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Natural, Natural))
Ex (Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Natural, Natural)) :: Example = Ex '(3, 3)
Miscellaneous
data Constraints (a :: [Constraint]) b Source #
Conjunction of a list of constraints.
Instances
type Eval (Constraints (a ': as) :: Constraint -> Type) Source # | |
Defined in Fcf.Utils | |
type Eval (Constraints ('[] :: [Constraint])) Source # | |
Defined in Fcf.Utils |