morley-1.7.0: Developer tools for the Michelson Language

Util.Type

Description

General type utilities.

Synopsis

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

#### Instances

Instances details
 KnownList ('[] :: [k]) Source # Instance detailsDefined in Util.Type Methodsklist :: KList '[] Source # KnownList xs => KnownList (x ': xs :: [k]) Source # Instance detailsDefined in Util.Type Methodsklist :: 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 detailsDefined in Util.Type MethodsshowsPrec :: Int -> Some1 f -> ShowS #show :: Some1 f -> String #showList :: [Some1 f] -> ShowS #

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.