Safe Haskell	None
Language	Haskell2010

Util.Type

Description

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
- reifyList :: (forall a. c a => Proxy a -> r) -> [r]
type family PatternMatch (a :: Type) :: Constraint where ...
type family PatternMatchL (l :: [k]) :: Constraint where ...
class KnownList l where
- klist :: KList l
data KList (l :: [k]) where
- 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)
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.

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

Equations

IsElem _ '[] = 'False
IsElem a (a ': _) = 'True
IsElem a (_ ': as) = IsElem a as

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

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

Difference between two lists.

Equations

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

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

Equations

Guard 'False _ = 'Nothing
Guard 'True a = 'Just a

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.

Equations

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.

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

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

Equations

AllUnique '[] = 'True
AllUnique (x ': xs) = Not (IsElem x xs) && AllUnique xs

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.

Methods

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

Instances

Instances details

ReifyList (c :: k -> Constraint) ('[] :: [k]) Source #
Instance details Defined in Util.Type Methods reifyList :: (forall (a :: k0). c a => Proxy a -> r) -> [r] Source #
(c x, ReifyList c xs) => ReifyList (c :: a -> Constraint) (x ': xs :: [a]) Source #
Instance details Defined in Util.Type Methods reifyList :: (forall (a0 :: k). c a0 => Proxy a0 -> r) -> [r] 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.

Equations

PatternMatch Int = ((), ())
PatternMatch _ = ()

type family PatternMatchL (l :: [k]) :: Constraint where ... Source #

Equations

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

class KnownList l where Source #

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

Methods

klist :: KList l Source #

Instances

Instances details

KnownList ('[] :: [k]) Source #
Instance details Defined in Util.Type Methods klist :: KList '[] Source #
KnownList xs => KnownList (x ': xs :: [k]) Source #
Instance details Defined in Util.Type Methods klist :: KList (x ': xs) Source #

data KList (l :: [k]) where Source #

SList analogy for KnownList.

Constructors

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

type RSplit l r = KnownList l Source #

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.

Constructors

forall a. Some1 (f a)

Instances

Instances details

(forall (a :: k). Show (f a)) => Show (Some1 f) Source #
Instance details Defined in Util.Type Methods showsPrec :: Int -> Some1 f -> ShowS # show :: Some1 f -> String # showList :: [Some1 f] -> ShowS #

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.

type ConcatListOfTypesAssociativity a b c = ((a ++ b) ++ c) ~ (a ++ (b ++ c)) Source #

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.