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

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 #

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.

class MockableConstraint (c :: Constraint) where Source #

Constaints that can be provided on demand.

Needless to say, this is a pretty unsafe operation. This typeclass makes using it safer in a sense that getting a segfault becomes harder, but still it deceives the type system and should be used only if providing a proper proof would be too difficult.

Methods

provideConstraintUnsafe :: Dict c Source #

Produce a constraint out of thin air.

Instances

Instances details
c a => MockableConstraint (c a) Source #

In majority of the cases we don't want to mock typeclass constraints since coercing instances of typeclasses with methods is utterly unsafe.

Instance details

Defined in Util.Type

KnownPeano a => MockableConstraint (KnownPeano a) Source # 
Instance details

Defined in Util.Peano

(MockableConstraint c1, MockableConstraint c2) => MockableConstraint (c1, c2) Source # 
Instance details

Defined in Util.Type

MockableConstraint (a ~ b) Source # 
Instance details

Defined in Util.Type

(MockableConstraint c1, MockableConstraint c2, MockableConstraint c3) => MockableConstraint (c1, c2, c3) Source # 
Instance details

Defined in Util.Type

Methods

provideConstraintUnsafe :: Dict (c1, c2, c3) Source #

MockableConstraint (RequireLongerOrSameLength l a) Source # 
Instance details

Defined in Util.Peano

MockableConstraint (RequireLongerThan l a) Source # 
Instance details

Defined in Util.Peano

(MockableConstraint c1, MockableConstraint c2, MockableConstraint c3, MockableConstraint c4) => MockableConstraint (c1, c2, c3, c4) Source # 
Instance details

Defined in Util.Type

Methods

provideConstraintUnsafe :: Dict (c1, c2, c3, c4) Source #

(MockableConstraint c1, MockableConstraint c2, MockableConstraint c3, MockableConstraint c4, MockableConstraint c5) => MockableConstraint (c1, c2, c3, c4, c5) Source # 
Instance details

Defined in Util.Type

Methods

provideConstraintUnsafe :: Dict (c1, c2, c3, c4, c5) Source #

onFirst :: Bifunctor p => p a c -> (a -> b) -> p b c Source #

Utility function to help transform the first argument of a binfunctor.