| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Util.Type
Description
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 FailWhen cond msg = FailUnless (Not cond) msg
- type family FailUnless (cond :: Bool) (msg :: ErrorMessage) :: Constraint where ...
- failUnlessEvi :: forall cond msg. FailUnless cond msg :- (cond ~ 'True)
- failWhenEvi :: forall cond msg. FailWhen cond msg :- (cond ~ 'False)
- type family AllUnique (l :: [k]) :: Bool where ...
- type RequireAllUnique desc l = RequireAllUnique' desc l l
- 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)
- data Some1 (f :: k -> Type) = forall a. Some1 (f a)
- recordToSomeList :: Rec f l -> [Some1 f]
- reifyTypeEquality :: forall a b x. (a == b) ~ 'True => (a ~ b => x) -> x
- type ConcatListOfTypesAssociativity a b c = ((a ++ b) ++ c) ~ (a ++ (b ++ c))
- listOfTypesConcatAssociativityAxiom :: forall a b c. Dict (ConcatListOfTypesAssociativity a b c)
- class MockableConstraint (c :: Constraint) where
- onFirst :: Bifunctor p => p a c -> (a -> b) -> p b c
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 FailWhen cond msg = FailUnless (Not cond) msg Source #
Fail with given error if the condition holds.
type family FailUnless (cond :: Bool) (msg :: ErrorMessage) :: Constraint where ... Source #
Fail with given error if the condition does not hold.
Equations
| FailUnless 'True _ = () | |
| FailUnless 'False msg = TypeError msg |
failUnlessEvi :: forall cond msg. FailUnless cond msg :- (cond ~ 'True) Source #
A natural conclusion from the fact that error have not occured.
type RequireAllUnique desc l = RequireAllUnique' desc l l Source #
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.
Equations
| PatternMatch Int = ((), ()) | |
| PatternMatch _ = () |
type family PatternMatchL (l :: [k]) :: Constraint where ... Source #
Equations
| 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.
data Some1 (f :: k -> Type) Source #
A value of type parametrized with some type parameter.
Constructors
| forall a. Some1 (f a) |
recordToSomeList :: Rec f l -> [Some1 f] Source #
reifyTypeEquality :: forall a b x. (a == b) ~ 'True => (a ~ b => x) -> x Source #
Reify type equality from boolean equality.
listOfTypesConcatAssociativityAxiom :: forall a b c. Dict (ConcatListOfTypesAssociativity a b c) Source #
GHC can't deduce this itself because in general a type family might be not associative, what brings extra difficulties and redundant constraints, especially if you have complex types. But (++) type family is associative, so let's define this small hack.
class MockableConstraint (c :: Constraint) where Source #
Constaints that can be provided on demand.
Needless to say, this is a pretty unsafe operation. This typeclass makes using it safer in a sense that getting a segfault becomes harder, but still it deceives the type system and should be used only if providing a proper proof would be too difficult.