Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Fcf
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 instanceEval
(FromMaybe a 'Nothing) = a type instanceEval
(FromMaybe a ('Just b)) = b
Essential language extensions for Fcf:
{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TypeInType, TypeOperators, UndecidableInstances #-}
Synopsis
- type Exp a = a -> Type
- type family Eval (e :: Exp a) :: a
- 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
- data (<=<) :: (b -> Exp c) -> (a -> Exp b) -> a -> Exp c
- 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
- data (<*>) :: Exp (a -> b) -> Exp a -> Exp b
- data Flip :: (a -> b -> Exp c) -> b -> a -> Exp c
- data ConstFn :: a -> b -> Exp a
- data ($) :: (a -> Exp b) -> a -> Exp b
- data Uncurry :: (a -> b -> Exp c) -> (a, b) -> Exp c
- 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 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
- 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)
- data FindIndex :: (a -> Exp Bool) -> [a] -> Exp (Maybe Nat)
- data Lookup :: k -> [(k, b)] -> Exp (Maybe b)
- data SetIndex :: Nat -> a -> [a] -> Exp [a]
- data ZipWith :: (a -> b -> Exp c) -> [a] -> [b] -> Exp [c]
- data Zip :: [a] -> [b] -> Exp [(a, b)]
- data Unzip :: Exp [(a, b)] -> Exp ([a], [b])
- data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])
- data UnBool :: Exp a -> Exp a -> Bool -> Exp a
- data (||) :: Bool -> Bool -> Exp Bool
- data (&&) :: Bool -> Bool -> Exp Bool
- data Not :: Bool -> Exp Bool
- data Guarded :: a -> [Guard (a -> Exp Bool) (Exp b)] -> Exp b
- data Guard a b = a := b
- type Otherwise = ConstFn 'True
- data Case :: [Match j k] -> j -> Exp 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 (+) :: 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
- 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 Error :: Symbol -> Exp a
- data Constraints :: [Constraint] -> Exp Constraint
- data TyEq :: a -> b -> Exp Bool
- type family Stuck :: a
- class IsBool (b :: Bool) where
- _If :: (b ~ 'True => r) -> (b ~ 'False => r) -> r
- 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 (IsJust ('Nothing :: Maybe a) :: Bool -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (IsJust ('Just _a) :: Bool -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (IsNothing ('Nothing :: Maybe a) :: Bool -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (IsNothing ('Just _a) :: Bool -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval ('False && b :: Bool -> Type) Source # | |
Defined in Fcf.Data.Bool | |
type Eval ('True && b :: Bool -> Type) Source # | |
Defined in Fcf.Data.Bool | |
type Eval (a && 'True :: Bool -> Type) Source # | |
Defined in Fcf.Data.Bool | |
type Eval (a && 'False :: Bool -> Type) Source # | |
Defined in Fcf.Data.Bool | |
type Eval ('False || b :: Bool -> Type) Source # | |
Defined in Fcf.Data.Bool | |
type Eval ('True || b :: Bool -> Type) Source # | |
Defined in Fcf.Data.Bool | |
type Eval (a || 'False :: Bool -> Type) Source # | |
Defined in Fcf.Data.Bool | |
type Eval (a || 'True :: Bool -> Type) Source # | |
Defined in Fcf.Data.Bool | |
type Eval (a > b :: Bool -> Type) Source # | |
type Eval (a < b :: Bool -> Type) Source # | |
type Eval (a >= b :: Bool -> Type) Source # | |
Defined in Fcf.Data.Nat | |
type Eval (a <= b :: Bool -> Type) Source # | |
Defined in Fcf.Data.Nat | |
type Eval (Null (a2 ': as) :: Bool -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Null ('[] :: [a]) :: Bool -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (a ^ b :: Nat -> Type) Source # | |
Defined in Fcf.Data.Nat | |
type Eval (a * b :: Nat -> Type) Source # | |
Defined in Fcf.Data.Nat | |
type Eval (a - b :: Nat -> Type) Source # | |
Defined in Fcf.Data.Nat | |
type Eval (a + b :: Nat -> Type) Source # | |
Defined in Fcf.Data.Nat | |
type Eval (Length (a2 ': as) :: Nat -> Type) Source # | |
type Eval (Length ('[] :: [a]) :: Nat -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Pure x :: a -> Type) Source # | |
Defined in Fcf.Combinators | |
type Eval (Join e :: a -> Type) Source # | |
Defined in Fcf.Combinators | |
type Eval (Error msg :: a -> Type) Source # | |
type Eval (TError msg :: a -> Type) Source # | |
type Eval (IsRight ('Right _a :: Either a b) :: Bool -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (IsRight ('Left _a :: Either a b) :: Bool -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (IsLeft ('Right _a :: Either a b) :: Bool -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (IsLeft ('Left _a :: Either a b) :: Bool -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (Elem a2 as :: Bool -> 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 (FromMaybe _a ('Just b) :: a -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (FromMaybe a2 ('Nothing :: Maybe a1) :: a1 -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (TyEq a b :: Bool -> Type) Source # | |
type Eval (Pure1 f x :: a2 -> Type) Source # | |
Defined in Fcf.Combinators | |
type Eval (k =<< e :: 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 # | |
Defined in Fcf.Combinators | |
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 (Case ms a :: k -> Type) Source # | |
type Eval (UnBool fal tru 'True :: a -> Type) Source # | |
Defined in Fcf.Data.Bool | |
type Eval (UnBool fal tru 'False :: a -> Type) Source # | |
Defined in Fcf.Data.Bool | |
type Eval (Guarded x ((p := y) ': ys) :: a2 -> Type) Source # | |
type Eval (Uncurry f '(x, y) :: a2 -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (UnMaybe y f ('Just x) :: a1 -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (UnMaybe y f ('Nothing :: Maybe a2) :: a1 -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (Foldr f y (x ': xs) :: a2 -> Type) Source # | |
type Eval (Foldr f y ('[] :: [a1]) :: a2 -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (UnList y f xs :: a1 -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Pure2 f x y :: a2 -> Type) Source # | |
Defined in Fcf.Combinators | |
type Eval ((f <=< g) x :: a2 -> Type) Source # | |
Defined in Fcf.Combinators | |
type Eval (LiftM2 f x y :: a3 -> Type) Source # | |
type Eval (Flip f y x :: a2 -> Type) Source # | |
Defined in Fcf.Combinators | |
type Eval (UnEither f g ('Right y :: Either a1 b) :: a2 -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (UnEither f g ('Left x :: Either a1 b) :: a2 -> Type) Source # | |
Defined in Fcf.Data.Common | |
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 (Concat lsts :: [a] -> Type) Source # | |
type Eval (Reverse l :: [a] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Init (a2 ': (b ': as)) :: Maybe [a1] -> Type) Source # | |
type Eval (Init '[a2] :: Maybe [a1] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Init ('[] :: [a]) :: Maybe [a] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Tail (_a ': as) :: Maybe [a] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Tail ('[] :: [a]) :: Maybe [a] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Head (a2 ': _as) :: Maybe a1 -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Head ('[] :: [a]) :: Maybe a -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Last (a2 ': (b ': as)) :: Maybe a1 -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Last '[a2] :: Maybe a1 -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Last ('[] :: [a]) :: Maybe a -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Cons a2 as :: [a1] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval ((x ': xs) ++ ys :: [a] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (('[] :: [a]) ++ ys :: [a] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Filter p (a2 ': as) :: [a1] -> Type) Source # | |
type Eval (Filter _p ('[] :: [a]) :: [a] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Replicate n a2 :: [a1] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Take n as :: [a] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Drop 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 (DropWhile p (x ': xs) :: [a] -> Type) Source # | |
type Eval (DropWhile p ('[] :: [a]) :: [a] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (FindIndex p (a2 ': as) :: Maybe Nat -> Type) Source # | |
type Eval (FindIndex _p ('[] :: [a]) :: Maybe Nat -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Find p (a2 ': as) :: Maybe a1 -> Type) Source # | |
type Eval (Find _p ('[] :: [a]) :: Maybe a -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Zip as bs :: [(a, b)] -> Type) Source # | |
type Eval (Unfoldr f c :: [a] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (ConcatMap f lst :: [a2] -> Type) Source # | |
type Eval (SetIndex n a' as :: [k] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Lookup a as :: Maybe b -> Type) Source # | |
type Eval (Map f (a2 ': as) :: [b] -> Type) Source # | |
type Eval (Map f ('[] :: [a]) :: [b] -> Type) Source # | |
Defined in Fcf.Classes | |
type Eval (Map f ('Just a3) :: Maybe a2 -> Type) Source # | |
Defined in Fcf.Classes | |
type Eval (Map f ('Nothing :: Maybe a) :: Maybe b -> Type) Source # | |
Defined in Fcf.Classes | |
type Eval (ZipWith f (a2 ': as) (b2 ': bs) :: [c] -> Type) Source # | |
type Eval (ZipWith _f _as ('[] :: [b]) :: [c] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (ZipWith _f ('[] :: [a]) _bs :: [c] -> Type) Source # | |
Defined in Fcf.Data.List | |
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 ('Right a3 :: Either a2 a1) :: Either a2 b -> Type) Source # | |
Defined in Fcf.Classes | |
type Eval (Map f ('Left x :: Either a2 a1) :: Either a2 b -> Type) Source # | |
Defined in Fcf.Classes | |
type Eval (Map f '(x, a2) :: (k2, k1) -> Type) Source # | |
Defined in Fcf.Classes | |
type Eval ((f *** f') '(b2, b'2) :: (k1, k2) -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (Bimap f g ('Right y :: Either a b1) :: Either a' b2 -> Type) Source # | |
Defined in Fcf.Classes | |
type Eval (Bimap f g ('Left x :: Either a1 b) :: Either a2 b' -> Type) Source # | |
Defined in Fcf.Classes | |
type Eval (Bimap f g '(x, y) :: (k1, k2) -> Type) Source # | |
Defined in Fcf.Classes | |
type Eval (Map f '(x, y, a2) :: (k2, k3, k1) -> Type) Source # | |
Defined in Fcf.Classes | |
type Eval (Map f '(x, y, z, a2) :: (k2, k3, k4, k1) -> Type) Source # | |
Defined in Fcf.Classes | |
type Eval (Map f '(x, y, z, w, a2) :: (k2, k3, k4, k5, k1) -> Type) Source # | |
Defined in Fcf.Classes |
Functional combinators
data ($) :: (a -> Exp b) -> a -> Exp 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 (***) :: (b -> Exp c) -> (b' -> Exp c') -> (b, b') -> Exp (c, c') infixr 3 Source #
Equivalent to Bimap
for pairs.
Either
data UnEither :: (a -> Exp c) -> (b -> Exp c) -> Either a b -> Exp c Source #
Instances
type Eval (UnEither f g ('Right y :: Either a1 b) :: a2 -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (UnEither f g ('Left x :: Either a1 b) :: a2 -> Type) Source # | |
Defined in Fcf.Data.Common |
data IsLeft :: Either a b -> Exp Bool Source #
Instances
type Eval (IsLeft ('Right _a :: Either a b) :: Bool -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (IsLeft ('Left _a :: Either a b) :: Bool -> Type) Source # | |
Defined in Fcf.Data.Common |
data IsRight :: Either a b -> Exp Bool Source #
Instances
type Eval (IsRight ('Right _a :: Either a b) :: Bool -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (IsRight ('Left _a :: Either a b) :: Bool -> Type) Source # | |
Defined in Fcf.Data.Common |
Maybe
data UnMaybe :: Exp b -> (a -> Exp b) -> Maybe a -> Exp b Source #
Instances
type Eval (UnMaybe y f ('Just x) :: a1 -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (UnMaybe y f ('Nothing :: Maybe a2) :: a1 -> Type) Source # | |
Defined in Fcf.Data.Common |
data FromMaybe :: k -> Maybe k -> Exp k Source #
Instances
type Eval (FromMaybe _a ('Just b) :: a -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (FromMaybe a2 ('Nothing :: Maybe a1) :: a1 -> Type) Source # | |
Defined in Fcf.Data.Common |
data IsNothing :: Maybe a -> Exp Bool Source #
Instances
type Eval (IsNothing ('Nothing :: Maybe a) :: Bool -> Type) Source # | |
Defined in Fcf.Data.Common | |
type Eval (IsNothing ('Just _a) :: Bool -> Type) Source # | |
Defined in Fcf.Data.Common |
Lists
data Foldr :: (a -> b -> Exp b) -> b -> [a] -> Exp b Source #
Foldr for type-level lists.
Example
>>>
:kind! Eval (Foldr (+) 0 '[1, 2, 3, 4])
Eval (Foldr (+) 0 '[1, 2, 3, 4]) :: Nat = 10
Instances
data UnList :: b -> (a -> b -> Exp b) -> [a] -> Exp b Source #
N.B.: This is equivalent to a Foldr
flipped.
data (++) :: [a] -> [a] -> Exp [a] Source #
Type-level list catenation.
Example
>>>
:kind! Eval ('[1, 2] ++ '[3, 4])
Eval ('[1, 2] ++ '[3, 4]) :: [Nat] = '[1, 2, 3, 4]
data Tail :: [a] -> Exp (Maybe [a]) Source #
Instances
type Eval (Tail (_a ': as) :: Maybe [a] -> Type) Source # | |
Defined in Fcf.Data.List | |
type Eval (Tail ('[] :: [a]) :: Maybe [a] -> Type) Source # | |
Defined in Fcf.Data.List |
data Find :: (a -> Exp Bool) -> [a] -> Exp (Maybe a) Source #
data FindIndex :: (a -> Exp Bool) -> [a] -> Exp (Maybe Nat) Source #
Find the index of an element satisfying the predicate.
data SetIndex :: Nat -> a -> [a] -> Exp [a] Source #
Modify an element at a given index.
The list is unchanged if the index is out of bounds.
data ZipWith :: (a -> b -> Exp c) -> [a] -> [b] -> Exp [c] Source #
Bool
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
data (||) :: Bool -> Bool -> Exp Bool infixr 2 Source #
Instances
type Eval ('False || b :: Bool -> Type) Source # | |
Defined in Fcf.Data.Bool | |
type Eval ('True || b :: Bool -> Type) Source # | |
Defined in Fcf.Data.Bool | |
type Eval (a || 'False :: Bool -> Type) Source # | |
Defined in Fcf.Data.Bool | |
type Eval (a || 'True :: Bool -> Type) Source # | |
Defined in Fcf.Data.Bool |
data (&&) :: Bool -> Bool -> Exp Bool infixr 3 Source #
Instances
type Eval ('False && b :: Bool -> Type) Source # | |
Defined in Fcf.Data.Bool | |
type Eval ('True && b :: Bool -> Type) Source # | |
Defined in Fcf.Data.Bool | |
type Eval (a && 'True :: Bool -> Type) Source # | |
Defined in Fcf.Data.Bool | |
type Eval (a && 'False :: Bool -> Type) Source # | |
Defined in Fcf.Data.Bool |
Multi-way if
data Guarded :: a -> [Guard (a -> Exp Bool) (Exp b)] -> Exp b Source #
Deprecated: Use Case
instead
A conditional choosing the first branch whose guard a ->
accepts a given value Exp
Bool
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" ])
Case splitting
data Case :: [Match j k] -> j -> Exp 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.
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 :: (a -> Exp b) -> f a -> Exp (f b) Source #
Type-level fmap
for type-level functors.
Example
>>>
import Fcf.Data.Nat
>>>
import qualified GHC.TypeLits as TL
>>>
data AddMul :: Nat -> Nat -> Exp Nat
>>>
type instance Eval (AddMul x y) = (x TL.+ y) TL.* (x TL.+ y)
>>>
:kind! Eval (Map (AddMul 2) '[0, 1, 2, 3, 4])
Eval (Map (AddMul 2) '[0, 1, 2, 3, 4]) :: [Nat] = '[4, 9, 16, 25, 36]
Instances
type Eval (Map f (a2 ': as) :: [b] -> Type) Source # | |
type Eval (Map f ('[] :: [a]) :: [b] -> Type) Source # | |
Defined in Fcf.Classes | |
type Eval (Map f ('Just a3) :: Maybe a2 -> Type) Source # | |
Defined in Fcf.Classes | |
type Eval (Map f ('Nothing :: Maybe a) :: Maybe b -> Type) Source # | |
Defined in Fcf.Classes | |
type Eval (Map f ('Right a3 :: Either a2 a1) :: Either a2 b -> Type) Source # | |
Defined in Fcf.Classes | |
type Eval (Map f ('Left x :: Either a2 a1) :: Either a2 b -> Type) Source # | |
Defined in Fcf.Classes | |
type Eval (Map f '(x, a2) :: (k2, k1) -> Type) Source # | |
Defined in Fcf.Classes | |
type Eval (Map f '(x, y, a2) :: (k2, k3, k1) -> Type) Source # | |
Defined in Fcf.Classes | |
type Eval (Map f '(x, y, z, a2) :: (k2, k3, k4, k1) -> Type) Source # | |
Defined in Fcf.Classes | |
type Eval (Map f '(x, y, z, w, a2) :: (k2, k3, k4, k5, k1) -> Type) Source # | |
Defined in Fcf.Classes |
data Bimap :: (a -> Exp a') -> (b -> Exp b') -> f a b -> Exp (f a' b') Source #
Type-level bimap
.
Instances
type Eval (Bimap f g ('Right y :: Either a b1) :: Either a' b2 -> Type) Source # | |
Defined in Fcf.Classes | |
type Eval (Bimap f g ('Left x :: Either a1 b) :: Either a2 b' -> Type) Source # | |
Defined in Fcf.Classes | |
type Eval (Bimap f g '(x, y) :: (k1, k2) -> Type) Source # | |
Defined in Fcf.Classes |
Miscellaneous
data Constraints :: [Constraint] -> Exp Constraint 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 |