Util.Type

General type utilities.

Documentation

type family (a :: k) == (b :: k) :: Bool where ... infix 4

A type family to compute Boolean equality.

Equations

(f a :: k2) == (g b :: k2) = (f == g) && (a == b)

(a :: k) == (a :: k) = True

(_1 :: k) == (_2 :: k) = False

type family If (cond :: Bool) (tru :: k) (fls :: k) :: k where ...

Type-level If. If True a b ==> a; If False a b ==> b

Equations

If True (tru :: k) (fls :: k) = tru

If False (tru :: k) (fls :: k) = fls

type family (as :: [k]) ++ (bs :: [k]) :: [k] where ...

Append for type-level lists.

Equations

([] :: [k]) ++ (bs :: [k]) = bs

(a ': as :: [k]) ++ (bs :: [k]) = a ': (as ++ bs)

type family IsElem (a :: k) (l :: [k]) :: Bool where ...

Equations

IsElem _ '[] = False

IsElem a (a ': _) = True

IsElem a (_ ': as) = IsElem a as

type family (l :: [k]) / (a :: k) where ...

Remove all occurences of the given element.

Equations

'[] / _ = '[]

(a ': xs) / a = xs / a

(b ': xs) / a = b ': (xs / a)

type family (l1 :: [k]) // (l2 :: [k]) :: [k] where ...

Difference between two lists.

Equations

l // '[] = l

l // (x ': xs) = (l / x) // xs

type family Guard (cond :: Bool) (a :: k) :: Maybe k where ...

Equations

Guard False _ = Nothing

Guard True a = Just a

type FailWhen cond msg = FailUnless (Not cond) msg

Fail with given error if the condition holds.

type family FailUnless (cond :: Bool) (msg :: ErrorMessage) :: Constraint where ...

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)

A natural conclusion from the fact that error have not occured.

failWhenEvi :: forall cond msg. FailWhen cond msg :- (cond ~ False)

type family AllUnique (l :: [k]) :: Bool where ...

Equations

AllUnique '[] = True

AllUnique (x ': xs) = Not (IsElem x xs) && AllUnique xs

type RequireAllUnique desc l = RequireAllUnique' desc l l

class ReifyList (c :: k -> Constraint) (l :: [k]) where

Bring type-level list at term-level using given function to demote its individual elements.

Methods

reifyList :: (forall a. c a => Proxy a -> r) -> [r]

Instances

ReifyList (c :: k -> Constraint) ([] :: [k])

Defined in Util.Type

Methods

reifyList :: (forall (a :: k0). c a => Proxy a -> r) -> [r]

(c x, ReifyList c xs) => ReifyList (c :: a -> Constraint) (x ': xs :: [a])

Defined in Util.Type

Methods

reifyList :: (forall (a0 :: k). c a0 => Proxy a0 -> r) -> [r]

type family PatternMatch (a :: Type) :: Constraint where ...

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

Equations

PatternMatchL '[] = ((), ())

PatternMatchL _ = ()

class KnownList l where

Similar to SingI [], but does not require individual elements to be also instance of SingI.

Methods

klist :: KList l

Instances

KnownList ([] :: [k])

Defined in Util.Type

Methods

klist :: KList []

KnownList xs => KnownList (x ': xs :: [k])

Defined in Util.Type

Methods

klist :: KList (x ': xs)

data KList (l :: [k]) where

SList analogy for KnownList.

Constructors

KNil :: KList '[]

KCons :: KnownList xs => Proxy x -> Proxy xs -> KList (x ': xs)

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)

Split a record into two pieces.

reifyTypeEquality :: forall a b x. (a == b) ~ True => (a ~ b => x) -> x

Reify type equality from boolean equality.