Data.Type.BitRecords.Assert

Type - level assertion utility leveraging custom TypeErrors

Documentation

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

Apply an Assertion to some value and return that value if the assertion holds, otherwise throw a TypeError.

Equations

Assert cond x = ProcessCheckResult (Check cond x) x

type Assertion a = TyFun a (Maybe ErrorMessage) -> Type

Make an assertion by creating a phantom data type which contains TyFun a (Maybe ErrorMessage) as last parameter. Check is used by Assert the apply the TyFuns which are specialized in this definition to have the return type Maybe ErrorMessage.

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

Apply Assertions to the actual values.

Instances

type Check Nat (NatLE n) x

type Check Nat (NatLE n) x = If (Maybe ErrorMessage) ((<=?) x n) (Nothing ErrorMessage) (Just ErrorMessage ((:$$:) ((:<>:) (Text "Natural too big: ") (ShowType Nat x)) ((:<>:) (Text "Required: <=") (ShowType Nat n))))

type Check Nat (NatGE n) x

type Check Nat (NatGE n) x = If (Maybe ErrorMessage) ((<=?) n x) (Nothing ErrorMessage) (Just ErrorMessage ((:$$:) ((:<>:) (Text "Natural too small: ") (ShowType Nat x)) ((:<>:) (Text "Required: >=") (ShowType Nat n))))

type Check Nat (NatIn from to) n

type Check Nat (NatIn from to) n

type Check k (LengthIn k from to) xs

type Check k (LengthIn k from to) xs = Check Nat (NatIn from to) (CountElementsForLengthIn k xs)

type Check (Maybe ErrorMessage) ((@&&) (Maybe ErrorMessage) a1 a2) x

type Check (Maybe ErrorMessage) ((@&&) (Maybe ErrorMessage) a1 a2) x

type (?::) x cond = Assert cond x infixr 0

Assert that a given type satisfies some condition defined via Check instances. This is only an alias for Assert

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

Assert that two assertions both hold

Instances

type Check (Maybe ErrorMessage) ((@&&) (Maybe ErrorMessage) a1 a2) x

type Check (Maybe ErrorMessage) ((@&&) (Maybe ErrorMessage) a1 a2) x

data NatLE :: Nat -> Assertion Nat

Assert that a Nat is less than or equal to an other Nat.

Instances

type Check Nat (NatLE n) x

type Check Nat (NatLE n) x = If (Maybe ErrorMessage) ((<=?) x n) (Nothing ErrorMessage) (Just ErrorMessage ((:$$:) ((:<>:) (Text "Natural too big: ") (ShowType Nat x)) ((:<>:) (Text "Required: <=") (ShowType Nat n))))

data NatGE :: Nat -> Assertion Nat

Assert that a Nat is greater than or equal to an other Nat.

Instances

type Check Nat (NatGE n) x

type Check Nat (NatGE n) x = If (Maybe ErrorMessage) ((<=?) n x) (Nothing ErrorMessage) (Just ErrorMessage ((:$$:) ((:<>:) (Text "Natural too small: ") (ShowType Nat x)) ((:<>:) (Text "Required: >=") (ShowType Nat n))))

data NatIn :: Nat -> Nat -> Assertion Nat

Assert that a Nat is in a specific range.

Instances

type Check Nat (NatIn from to) n

type Check Nat (NatIn from to) n

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

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 k (LengthIn k from to) xs

type Check k (LengthIn k from to) xs = Check Nat (NatIn from to) (CountElementsForLengthIn k xs)

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

Instances

type CountElementsForLengthIn [k] ([] k)

type CountElementsForLengthIn [k] ([] k) = 0

type CountElementsForLengthIn [a] ((:) a x xs)

type CountElementsForLengthIn [a] ((:) a x xs) = (+) 1 (CountElementsForLengthIn [a] xs)