Safe Haskell | None |
---|---|

Language | Haskell2010 |

Type - level assertion utility leveraging custom `TypeError`

s

## Synopsis

- type family Assert (cond :: Assertion a) (x :: a) :: a where ...
- type Assertion a = TyFun a (Maybe ErrorMessage) -> Type
- type family Check (f :: Assertion a) (x :: a) :: Maybe ErrorMessage
- type (?::) x cond = Assert cond x
- data (@&&) :: Assertion a -> Assertion a -> Assertion a
- data NatLE :: Nat -> Assertion Nat
- data NatGE :: Nat -> Assertion Nat
- data NatIn :: Nat -> Nat -> Assertion Nat
- data LengthIn :: Nat -> Nat -> Assertion a
- type family CountElementsForLengthIn (xs :: k) :: Nat

# Documentation

type family Assert (cond :: Assertion a) (x :: a) :: a where ... Source #

type family Check (f :: Assertion a) (x :: a) :: Maybe ErrorMessage Source #

Apply `Assertion`

s to the actual values.

## Instances

type Check (NatLE n :: TyFun Nat (Maybe ErrorMessage) -> Type) (x :: Nat) Source # | |

type Check (NatGE n :: TyFun Nat (Maybe ErrorMessage) -> Type) (x :: Nat) Source # | |

type Check (NatIn from to :: TyFun Nat (Maybe ErrorMessage) -> Type) (n :: Nat) Source # | |

Defined in Data.Type.BitRecords.Assert | |

type Check (LengthIn from to :: TyFun k (Maybe ErrorMessage) -> Type) (xs :: k) Source # | |

Defined in Data.Type.BitRecords.Assert type Check (LengthIn from to :: TyFun k (Maybe ErrorMessage) -> Type) (xs :: k) = Check (NatIn from to) (CountElementsForLengthIn xs) | |

type Check (a1 @&& a2 :: TyFun (Maybe ErrorMessage) (Maybe ErrorMessage) -> Type) (x :: Maybe ErrorMessage) Source # | |

Defined in Data.Type.BitRecords.Assert type Check (a1 @&& a2 :: TyFun (Maybe ErrorMessage) (Maybe ErrorMessage) -> Type) (x :: Maybe ErrorMessage) |

data (@&&) :: Assertion a -> Assertion a -> Assertion a Source #

Assert that two assertions both hold

## Instances

type Check (a1 @&& a2 :: TyFun (Maybe ErrorMessage) (Maybe ErrorMessage) -> Type) (x :: Maybe ErrorMessage) Source # | |

Defined in Data.Type.BitRecords.Assert type Check (a1 @&& a2 :: TyFun (Maybe ErrorMessage) (Maybe ErrorMessage) -> Type) (x :: Maybe ErrorMessage) |

data LengthIn :: Nat -> Nat -> Assertion a Source #

Assert that a list's length falls into a given range.
This is generalized from actual lists; everything with a `CountElementsForLengthIn`

instance can be asserted.

## Instances

type Check (LengthIn from to :: TyFun k (Maybe ErrorMessage) -> Type) (xs :: k) Source # | |

Defined in Data.Type.BitRecords.Assert type Check (LengthIn from to :: TyFun k (Maybe ErrorMessage) -> Type) (xs :: k) = Check (NatIn from to) (CountElementsForLengthIn xs) |

type family CountElementsForLengthIn (xs :: k) :: Nat Source #

## Instances

type CountElementsForLengthIn ([] :: [k]) Source # | |

Defined in Data.Type.BitRecords.Assert type CountElementsForLengthIn ([] :: [k]) = 0 | |

type CountElementsForLengthIn (x ': xs :: [a]) Source # | |

Defined in Data.Type.BitRecords.Assert |