morley-1.0.0: Developer tools for the Michelson Language

Safe HaskellNone
LanguageHaskell2010

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

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

Reify type equality from boolean equality.