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 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)

# 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.

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.

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.

data Some1 (f :: k -> Type) Source #

A value of type parametrized with *some* type parameter.

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.