Safe Haskell | None |
---|---|
Language | Haskell2010 |
General type utilities.
Synopsis
- type family (a :: k) == (b :: k) :: Bool where ...
- type family If (cond :: Bool) (tru :: k) (fls :: k) :: k where ...
- type family (as :: [k]) ++ (bs :: [k]) :: [k] where ...
- type family IsElem (a :: k) (l :: [k]) :: Bool where ...
- type family (l :: [k]) / (a :: k) where ...
- type family (l1 :: [k]) // (l2 :: [k]) :: [k] where ...
- type family Guard (cond :: Bool) (a :: k) :: Maybe k where ...
- type family AllUnique (l :: [k]) :: Bool where ...
- type family RequireAllUnique (desc :: Symbol) (l :: [k]) :: Constraint where ...
- class ReifyList (c :: k -> Constraint) (l :: [k]) where
- type family PatternMatch (a :: Type) :: Constraint where ...
- type family PatternMatchL (l :: [k]) :: Constraint where ...
- class KnownList l where
- data KList (l :: [k]) where
- type RSplit l r = KnownList l
- rsplit :: forall k (l :: [k]) (r :: [k]) f. RSplit l r => Rec f (l ++ r) -> (Rec f l, Rec f r)
- reifyTypeEquality :: forall a b x. (a == b) ~ True => (a ~ b => x) -> x
Documentation
type family (a :: k) == (b :: k) :: Bool where ... infix 4 #
A type family to compute Boolean equality.
type family If (cond :: Bool) (tru :: k) (fls :: k) :: k where ... #
Type-level If. If True a b
==> a
; If False a b
==> b
type family RequireAllUnique (desc :: Symbol) (l :: [k]) :: Constraint where ... Source #
RequireAllUnique _ '[] = () | |
RequireAllUnique desc (x ': xs) = If (IsElem x xs) (TypeError (((Text "Duplicated " :<>: Text desc) :<>: Text ":") :$$: ShowType x)) (RequireAllUnique desc xs) |
class ReifyList (c :: k -> Constraint) (l :: [k]) where Source #
Bring type-level list at term-level using given function to demote its individual elements.
Instances
ReifyList (c :: k -> Constraint) ([] :: [k]) Source # | |
(c x, ReifyList c xs) => ReifyList (c :: a -> Constraint) (x ': xs :: [a]) Source # | |
type family PatternMatch (a :: Type) :: Constraint where ... Source #
Make sure given type is evaluated.
This type family fits only for types of Type
kind.
PatternMatch Int = ((), ()) | |
PatternMatch _ = () |
type family PatternMatchL (l :: [k]) :: Constraint where ... Source #
PatternMatchL '[] = ((), ()) | |
PatternMatchL _ = () |
class KnownList l where Source #
Similar to SingI []
, but does not require individual elements to be also
instance of SingI
.
rsplit :: forall k (l :: [k]) (r :: [k]) f. RSplit l r => Rec f (l ++ r) -> (Rec f l, Rec f r) Source #
Split a record into two pieces.
reifyTypeEquality :: forall a b x. (a == b) ~ True => (a ~ b => x) -> x Source #
Reify type equality from boolean equality.