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 (NatLE n :: TyFun Nat (Maybe ErrorMessage) -> Type) (x :: Nat)

Defined in Data.Type.BitRecords.Assert

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

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

Defined in Data.Type.BitRecords.Assert

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

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

Defined in Data.Type.BitRecords.Assert

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

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

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)

Defined in Data.Type.BitRecords.Assert

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

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 (a1 @&& a2 :: TyFun (Maybe ErrorMessage) (Maybe ErrorMessage) -> Type) (x :: Maybe ErrorMessage)

Defined in Data.Type.BitRecords.Assert

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

data NatLE :: Nat -> Assertion Nat

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

Instances

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

Defined in Data.Type.BitRecords.Assert

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

data NatGE :: Nat -> Assertion Nat

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

Instances

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

Defined in Data.Type.BitRecords.Assert

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

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

Assert that a Nat is in a specific range.

Instances

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

Defined in Data.Type.BitRecords.Assert

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

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 (LengthIn from to :: TyFun k (Maybe ErrorMessage) -> Type) (xs :: k)

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

Instances

type CountElementsForLengthIn ([] :: [k])

Defined in Data.Type.BitRecords.Assert

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

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

Defined in Data.Type.BitRecords.Assert

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