plutus-core-1.30.0.0: Language library for Plutus Core
Safe HaskellSafe-Inferred
LanguageHaskell2010

Universe.Core

Synopsis

Documentation

data Esc a Source #

"Escapes" a type of an arbitrary kind to fit into Type.

data Some (tag ∷ k → Type) where #

Bundled Patterns

pattern Some ∷ ∀ {k} tag (a ∷ k). () ⇒ tag a → Some tag 

Instances

Instances details
(Closed uni, Everywhere uni PrettyConst) ⇒ PrettyBy ConstConfig (Some (ValueOf uni)) Source # 
Instance details

Defined in PlutusCore.Pretty.PrettyConst

Methods

prettyByConstConfigSome (ValueOf uni) → Doc ann Source #

prettyListByConstConfig → [Some (ValueOf uni)] → Doc ann Source #

Applicative m ⇒ Monoid (Some m) 
Instance details

Defined in Data.Some.Newtype

Methods

memptySome m Source #

mappendSome m → Some m → Some m Source #

mconcat ∷ [Some m] → Some m Source #

Applicative m ⇒ Semigroup (Some m) 
Instance details

Defined in Data.Some.Newtype

Methods

(<>)Some m → Some m → Some m Source #

sconcatNonEmpty (Some m) → Some m Source #

stimesIntegral b ⇒ b → Some m → Some m Source #

GRead f ⇒ Read (Some f) 
Instance details

Defined in Data.Some.Newtype

GShow tag ⇒ Show (Some tag) 
Instance details

Defined in Data.Some.Newtype

Methods

showsPrecIntSome tag → ShowS Source #

showSome tag → String Source #

showList ∷ [Some tag] → ShowS Source #

GNFData tag ⇒ NFData (Some tag) 
Instance details

Defined in Data.Some.Newtype

Methods

rnfSome tag → () Source #

(Closed uni, Everywhere uni Flat) ⇒ Flat (Some (ValueOf uni)) 
Instance details

Defined in PlutusCore.Flat

Methods

encodeSome (ValueOf uni) → Encoding

decode ∷ Get (Some (ValueOf uni))

sizeSome (ValueOf uni) → NumBits → NumBits

GEq tag ⇒ Eq (Some tag) 
Instance details

Defined in Data.Some.Newtype

Methods

(==)Some tag → Some tag → Bool Source #

(/=)Some tag → Some tag → Bool Source #

GCompare tag ⇒ Ord (Some tag) 
Instance details

Defined in Data.Some.Newtype

Methods

compareSome tag → Some tag → Ordering Source #

(<)Some tag → Some tag → Bool Source #

(<=)Some tag → Some tag → Bool Source #

(>)Some tag → Some tag → Bool Source #

(>=)Some tag → Some tag → Bool Source #

maxSome tag → Some tag → Some tag Source #

minSome tag → Some tag → Some tag Source #

(Closed uni, GEq uni, Everywhere uni Eq, Everywhere uni Hashable) ⇒ Hashable (Some (ValueOf uni)) Source # 
Instance details

Defined in Universe.Core

Methods

hashWithSaltIntSome (ValueOf uni) → Int

hashSome (ValueOf uni) → Int

(Closed uni, Everywhere uni ExMemoryUsage) ⇒ ExMemoryUsage (Some (ValueOf uni)) Source # 
Instance details

Defined in PlutusCore.Evaluation.Machine.ExMemoryUsage

Methods

memoryUsageSome (ValueOf uni) → CostRose Source #

(Closed uni, Everywhere uni PrettyConst) ⇒ Pretty (Some (ValueOf uni)) Source # 
Instance details

Defined in PlutusCore.Pretty.PrettyConst

Methods

prettySome (ValueOf uni) → Doc ann #

prettyList ∷ [Some (ValueOf uni)] → Doc ann #

data SomeTypeIn uni Source #

A particular type from a universe.

Constructors

∀ k (a ∷ k). SomeTypeIn !(uni (Esc a)) 

Instances

Instances details
PrettyBy RenderContext (SomeTypeIn DefaultUni) Source # 
Instance details

Defined in PlutusCore.Default.Universe

GShow uni ⇒ Show (SomeTypeIn uni) Source # 
Instance details

Defined in Universe.Core

Methods

showsPrecIntSomeTypeIn uni → ShowS Source #

showSomeTypeIn uni → String Source #

showList ∷ [SomeTypeIn uni] → ShowS Source #

Closed uni ⇒ NFData (SomeTypeIn uni) Source # 
Instance details

Defined in Universe.Core

Methods

rnfSomeTypeIn uni → () Source #

Closed uni ⇒ Flat (SomeTypeIn uni) 
Instance details

Defined in PlutusCore.Flat

Methods

encodeSomeTypeIn uni → Encoding

decode ∷ Get (SomeTypeIn uni)

sizeSomeTypeIn uni → NumBits → NumBits

GEq uni ⇒ Eq (SomeTypeIn uni) Source # 
Instance details

Defined in Universe.Core

Methods

(==)SomeTypeIn uni → SomeTypeIn uni → Bool Source #

(/=)SomeTypeIn uni → SomeTypeIn uni → Bool Source #

GCompare uni ⇒ Ord (SomeTypeIn uni) Source # 
Instance details

Defined in Universe.Core

Methods

compareSomeTypeIn uni → SomeTypeIn uni → Ordering Source #

(<)SomeTypeIn uni → SomeTypeIn uni → Bool Source #

(<=)SomeTypeIn uni → SomeTypeIn uni → Bool Source #

(>)SomeTypeIn uni → SomeTypeIn uni → Bool Source #

(>=)SomeTypeIn uni → SomeTypeIn uni → Bool Source #

maxSomeTypeIn uni → SomeTypeIn uni → SomeTypeIn uni Source #

minSomeTypeIn uni → SomeTypeIn uni → SomeTypeIn uni Source #

(Closed uni, GEq uni) ⇒ Hashable (SomeTypeIn uni) Source # 
Instance details

Defined in Universe.Core

Methods

hashWithSaltIntSomeTypeIn uni → Int

hashSomeTypeIn uni → Int

ExMemoryUsage (SomeTypeIn uni) Source # 
Instance details

Defined in PlutusCore.Evaluation.Machine.ExMemoryUsage

Pretty (SomeTypeIn DefaultUni) Source # 
Instance details

Defined in PlutusCore.Default.Universe

Pretty (SomeTypeIn uni) ⇒ Pretty (SomeTypeIn (Kinded uni)) Source # 
Instance details

Defined in PlutusCore.Pretty.PrettyConst

Methods

prettySomeTypeIn (Kinded uni) → Doc ann #

prettyList ∷ [SomeTypeIn (Kinded uni)] → Doc ann #

data Kinded uni ta where Source #

Constructors

KindedTypeable k ⇒ !(uni (Esc a)) → Kinded uni (Esc (a ∷ k)) 

Instances

Instances details
GShow uni ⇒ GShow (Kinded uni ∷ TypeType) Source # 
Instance details

Defined in Universe.Core

Methods

gshowsPrec ∷ ∀ (a ∷ k). IntKinded uni a → ShowS #

(Typeable k, Contains uni a) ⇒ Contains (Kinded uni) (a ∷ k) Source #

A Kinded uni contains an a :: k whenever uni contains it and k is Typeable.

Instance details

Defined in Universe.Core

Methods

knownUniKinded uni (Esc a) Source #

Pretty (SomeTypeIn uni) ⇒ Pretty (SomeTypeIn (Kinded uni)) Source # 
Instance details

Defined in PlutusCore.Pretty.PrettyConst

Methods

prettySomeTypeIn (Kinded uni) → Doc ann #

prettyList ∷ [SomeTypeIn (Kinded uni)] → Doc ann #

GShow uni ⇒ Show (Kinded uni ta) Source # 
Instance details

Defined in Universe.Core

Methods

showsPrecIntKinded uni ta → ShowS Source #

showKinded uni ta → String Source #

showList ∷ [Kinded uni ta] → ShowS Source #

data ValueOf uni a Source #

A value of a particular type from a universe.

Constructors

ValueOf !(uni (Esc a)) !a 

Instances

Instances details
(Closed uni, Everywhere uni NFData) ⇒ GNFData (ValueOf uni ∷ TypeType) Source # 
Instance details

Defined in Universe.Core

Methods

grnf ∷ ∀ (a ∷ k). ValueOf uni a → ()

(GCompare uni, Closed uni, Everywhere uni Ord, Everywhere uni Eq) ⇒ GCompare (ValueOf uni ∷ TypeType) Source # 
Instance details

Defined in Universe.Core

Methods

gcompare ∷ ∀ (a ∷ k) (b ∷ k). ValueOf uni a → ValueOf uni b → GOrdering a b

(GEq uni, Closed uni, Everywhere uni Eq) ⇒ GEq (ValueOf uni ∷ TypeType) Source # 
Instance details

Defined in Universe.Core

Methods

geq ∷ ∀ (a ∷ k) (b ∷ k). ValueOf uni a → ValueOf uni b → Maybe (a :~: b) #

(GShow uni, Closed uni, Everywhere uni Show) ⇒ GShow (ValueOf uni ∷ TypeType) Source # 
Instance details

Defined in Universe.Core

Methods

gshowsPrec ∷ ∀ (a ∷ k). IntValueOf uni a → ShowS #

(Closed uni, Everywhere uni PrettyConst) ⇒ PrettyBy ConstConfig (ValueOf uni a) Source # 
Instance details

Defined in PlutusCore.Pretty.PrettyConst

Methods

prettyByConstConfigValueOf uni a → Doc ann Source #

prettyListByConstConfig → [ValueOf uni a] → Doc ann Source #

(Closed uni, Everywhere uni PrettyConst) ⇒ PrettyBy ConstConfig (Some (ValueOf uni)) Source # 
Instance details

Defined in PlutusCore.Pretty.PrettyConst

Methods

prettyByConstConfigSome (ValueOf uni) → Doc ann Source #

prettyListByConstConfig → [Some (ValueOf uni)] → Doc ann Source #

(GShow uni, Closed uni, Everywhere uni Show) ⇒ Show (ValueOf uni a) Source # 
Instance details

Defined in Universe.Core

Methods

showsPrecIntValueOf uni a → ShowS Source #

showValueOf uni a → String Source #

showList ∷ [ValueOf uni a] → ShowS Source #

(Closed uni, Everywhere uni NFData) ⇒ NFData (ValueOf uni a) Source # 
Instance details

Defined in Universe.Core

Methods

rnfValueOf uni a → () Source #

(Closed uni, Everywhere uni Flat) ⇒ Flat (Some (ValueOf uni)) 
Instance details

Defined in PlutusCore.Flat

Methods

encodeSome (ValueOf uni) → Encoding

decode ∷ Get (Some (ValueOf uni))

sizeSome (ValueOf uni) → NumBits → NumBits

(GEq uni, Closed uni, Everywhere uni Eq) ⇒ Eq (ValueOf uni a) Source # 
Instance details

Defined in Universe.Core

Methods

(==)ValueOf uni a → ValueOf uni a → Bool Source #

(/=)ValueOf uni a → ValueOf uni a → Bool Source #

(GCompare uni, Closed uni, Everywhere uni Ord, Everywhere uni Eq) ⇒ Ord (ValueOf uni a) Source # 
Instance details

Defined in Universe.Core

Methods

compareValueOf uni a → ValueOf uni a → Ordering Source #

(<)ValueOf uni a → ValueOf uni a → Bool Source #

(<=)ValueOf uni a → ValueOf uni a → Bool Source #

(>)ValueOf uni a → ValueOf uni a → Bool Source #

(>=)ValueOf uni a → ValueOf uni a → Bool Source #

maxValueOf uni a → ValueOf uni a → ValueOf uni a Source #

minValueOf uni a → ValueOf uni a → ValueOf uni a Source #

(Closed uni, GEq uni, Everywhere uni Eq, Everywhere uni Hashable) ⇒ Hashable (ValueOf uni a) Source # 
Instance details

Defined in Universe.Core

Methods

hashWithSaltIntValueOf uni a → Int

hashValueOf uni a → Int

(Closed uni, GEq uni, Everywhere uni Eq, Everywhere uni Hashable) ⇒ Hashable (Some (ValueOf uni)) Source # 
Instance details

Defined in Universe.Core

Methods

hashWithSaltIntSome (ValueOf uni) → Int

hashSome (ValueOf uni) → Int

(Closed uni, Everywhere uni ExMemoryUsage) ⇒ ExMemoryUsage (Some (ValueOf uni)) Source # 
Instance details

Defined in PlutusCore.Evaluation.Machine.ExMemoryUsage

Methods

memoryUsageSome (ValueOf uni) → CostRose Source #

(Closed uni, Everywhere uni PrettyConst) ⇒ Pretty (ValueOf uni a) Source # 
Instance details

Defined in PlutusCore.Pretty.PrettyConst

Methods

prettyValueOf uni a → Doc ann #

prettyList ∷ [ValueOf uni a] → Doc ann #

(Closed uni, Everywhere uni PrettyConst) ⇒ Pretty (Some (ValueOf uni)) Source # 
Instance details

Defined in PlutusCore.Pretty.PrettyConst

Methods

prettySome (ValueOf uni) → Doc ann #

prettyList ∷ [Some (ValueOf uni)] → Doc ann #

class Contains uni a where Source #

A class for enumerating types and fully instantiated type formers that uni contains. For example, a particular ExampleUni may have monomorphic types in it:

instance ExampleUni Contains Integer where ... instance ExampleUni Contains Bool where ...

as well as polymorphic ones:

instance ExampleUni Contains [] where ... instance ExampleUni Contains (,) where ...

as well as their instantiations:

instance ExampleUni Contains a => ExampleUni Contains [a] where ... instance (ExampleUni Contains a, ExampleUni Contains b) => ExampleUni Contains (a, b) where ...

(a universe can have any subset of the mentioned sorts of types, for example it's fine to have instantiated polymorphic types and not have uninstantiated ones and vice versa)

Note that when used as a constraint of a function Contains does not allow you to directly express things like "uni has the Integer, Bool and [] types and type formers", because [] is not fully instantiated. So you can only say "uni has Integer, Bool, [Integer], [Bool], [[Integer]], [[Bool]] etc" and such manual enumeration is annoying, so we'd really like to be able to say that uni has lists of arbitrary built-in types (including lists of lists etc). Contains does not allow that, but Includes does. For example, in the body of the following definition:

foo :: (uni Includes Integer, uni Includes Bool, uni Includes []) => ... foo = ...

you can make use of the fact that uni has lists of arbitrary included types (integers, booleans and lists).

Hence most of the time opt for using the more flexible Includes.

Includes is defined in terms of Contains, so you only need to provide a Contains instance per type from the universe and you'll get Includes for free.

Methods

knownUni ∷ uni (Esc a) Source #

Instances

Instances details
Contains DefaultUni ByteString Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

knownUniDefaultUni (Esc ByteString) Source #

Contains DefaultUni Element Source # 
Instance details

Defined in PlutusCore.Default.Universe

Contains DefaultUni Element Source # 
Instance details

Defined in PlutusCore.Default.Universe

Contains DefaultUni MlResult Source # 
Instance details

Defined in PlutusCore.Default.Universe

Contains DefaultUni Data Source # 
Instance details

Defined in PlutusCore.Default.Universe

Contains DefaultUni Text Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

knownUniDefaultUni (Esc Text) Source #

Contains DefaultUni Integer Source # 
Instance details

Defined in PlutusCore.Default.Universe

Contains DefaultUni () Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

knownUniDefaultUni (Esc ()) Source #

Contains DefaultUni Bool Source # 
Instance details

Defined in PlutusCore.Default.Universe

(Contains DefaultUni f, Contains DefaultUni a) ⇒ Contains DefaultUni (f a ∷ k2) Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

knownUniDefaultUni (Esc (f a)) Source #

(Typeable k, Contains uni a) ⇒ Contains (Kinded uni) (a ∷ k) Source #

A Kinded uni contains an a :: k whenever uni contains it and k is Typeable.

Instance details

Defined in Universe.Core

Methods

knownUniKinded uni (Esc a) Source #

Contains DefaultUni (,) Source # 
Instance details

Defined in PlutusCore.Default.Universe

Contains DefaultUni List Source # 
Instance details

Defined in PlutusCore.Default.Universe

(TypeError NoStandalonePolymorphicDataErrMsg ∷ Constraint) ⇒ Contains uni (TyVarRepTyNameRep kind → kind) Source # 
Instance details

Defined in PlutusCore.Builtin.Polymorphism

Methods

knownUni ∷ uni (Esc TyVarRep) Source #

type Includes uni = Permits (Contains uni) Source #

uni Includes a reads as "a is in the uni". a can be of a higher-kind, see the docs of Contains on why you might want that.

knownUniOf ∷ uni `Contains` a ⇒ proxy a → uni (Esc a) Source #

Same as knownUni, but receives a proxy.

someType ∷ ∀ k (a ∷ k) uni. uni `Contains` a ⇒ SomeTypeIn uni Source #

Wrap a type into SomeTypeIn, provided it's in the universe.

someValueOf ∷ ∀ a uni. uni (Esc a) → a → Some (ValueOf uni) Source #

Wrap a value into Some (ValueOf uni), given its explicit type tag.

someValue ∷ ∀ a uni. uni `Contains` a ⇒ a → Some (ValueOf uni) Source #

Wrap a value into Some (ValueOf uni), provided its type is in the universe.

newtype DecodeUniM a Source #

A monad to decode types from a universe in. We use a monad for decoding, because parsing arguments of polymorphic built-in types can peel off an arbitrary amount of type tags from the input list of tags and so we have state, which is convenient to handle with, well, StateT.

Constructors

DecodeUniM 

Fields

Instances

Instances details
MonadFail DecodeUniM Source # 
Instance details

Defined in Universe.Core

Methods

failStringDecodeUniM a Source #

Alternative DecodeUniM Source # 
Instance details

Defined in Universe.Core

Applicative DecodeUniM Source # 
Instance details

Defined in Universe.Core

Methods

pure ∷ a → DecodeUniM a Source #

(<*>)DecodeUniM (a → b) → DecodeUniM a → DecodeUniM b Source #

liftA2 ∷ (a → b → c) → DecodeUniM a → DecodeUniM b → DecodeUniM c Source #

(*>)DecodeUniM a → DecodeUniM b → DecodeUniM b Source #

(<*)DecodeUniM a → DecodeUniM b → DecodeUniM a Source #

Functor DecodeUniM Source # 
Instance details

Defined in Universe.Core

Methods

fmap ∷ (a → b) → DecodeUniM a → DecodeUniM b Source #

(<$) ∷ a → DecodeUniM b → DecodeUniM a Source #

Monad DecodeUniM Source # 
Instance details

Defined in Universe.Core

Methods

(>>=)DecodeUniM a → (a → DecodeUniM b) → DecodeUniM b Source #

(>>)DecodeUniM a → DecodeUniM b → DecodeUniM b Source #

return ∷ a → DecodeUniM a Source #

MonadPlus DecodeUniM Source # 
Instance details

Defined in Universe.Core

class Closed uni where Source #

A universe is Closed, if it's known how to constrain every type from the universe and every type can be encoded to / decoded from a sequence of integer tags. The universe doesn't have to be finite and providing support for infinite universes is the reason why we encode a type as a sequence of integer tags as opposed to a single integer tag. For example, given

  data U a where
      UList :: !(U a) -> U [a]
      UInt  :: U Int

UList (UList UInt) can be encoded to [0,0,1] where 0 and 1 are the integer tags of the UList and UInt constructors, respectively.

Associated Types

type Everywhere uni (constr ∷ TypeConstraint) ∷ Constraint Source #

A constrant for "constr a holds for any a from uni".

Methods

encodeUni ∷ uni a → [Int] Source #

Encode a type as a sequence of Int tags. The opposite of decodeUni.

withDecodedUni ∷ (∀ k (a ∷ k). Typeable k ⇒ uni (Esc a) → DecodeUniM r) → DecodeUniM r Source #

Decode a type and feed it to the continuation.

bring ∷ uni `Everywhere` constr ⇒ proxy constr → uni (Esc a) → (constr a ⇒ r) → r Source #

Bring a constr a instance in scope, provided a is a type from the universe and constr holds for any type from the universe.

Instances

Instances details
Closed DefaultUni Source # 
Instance details

Defined in PlutusCore.Default.Universe

Associated Types

type Everywhere DefaultUni constr Source #

Methods

encodeUniDefaultUni a → [Int] Source #

withDecodedUni ∷ (∀ k (a ∷ k). Typeable k ⇒ DefaultUni (Esc a) → DecodeUniM r) → DecodeUniM r Source #

bringEverywhere DefaultUni constr ⇒ proxy constr → DefaultUni (Esc a) → (constr a ⇒ r) → r Source #

decodeKindedUniClosed uni ⇒ [Int] → Maybe (SomeTypeIn (Kinded uni)) Source #

Decode a type from a sequence of Int tags. The opposite of encodeUni (modulo invalid input).

peelUniTagDecodeUniM Int Source #

Peel off a tag from the input list of type tags.

type family Permits Source #

constr Permits f elaborates to one of - constr f forall a. constr a => constr (f a) forall a b. (constr a, constr b) => constr (f a b) forall a b c. (constr a, constr b, constr c) => constr (f a b c)

depending on the kind of f. This allows us to say things like

( constr Permits Integer , constr Permits [] , constr Permits (,) )

and thus constraint every type from the universe (including polymorphic ones) to satisfy constr, which is how we provide an implementation of Everywhere for universes with polymorphic types.

Permits is an open type family, so you can provide type instances for fs expecting more type arguments than 3 if you need that.

Note that, say, constr Permits [] elaborates to

forall a. constr a => constr [a]

and for certain type classes that does not make sense (e.g. the Generic instance of [] does not require the type of elements to be Generic), however it's not a problem because we use Permit to constrain the whole universe and so we know that arguments of polymorphic built-in types are builtins themselves are hence do satisfy the constraint and the fact that these constraints on arguments do not get used in the polymorphic case only means that they get ignored.

Instances

Instances details
type Permits Source # 
Instance details

Defined in Universe.Core

type Permits
type Permits Source # 
Instance details

Defined in Universe.Core

type Permits
type Permits Source # 
Instance details

Defined in Universe.Core

type Permits
type Permits Source # 
Instance details

Defined in Universe.Core

type Permits

type family EverywhereAll uni constrs where ... Source #

Equations

EverywhereAll uni '[] = () 
EverywhereAll uni (constr ': constrs) = (uni `Everywhere` constr, uni `EverywhereAll` constrs) 

type (<:) uni1 uni2 = uni1 `Everywhere` Includes uni2 Source #

A constraint for "uni1 is a subuniverse of uni2".

class HasUniApply (uni ∷ TypeType) where Source #

A class for "uni has general type application".

Methods

uniApply ∷ ∀ k l (f ∷ k → l) a. uni (Esc f) → uni (Esc a) → uni (Esc (f a)) Source #

Apply a type constructor to an argument.

matchUniApply Source #

Arguments

∷ uni tb

The type.

→ r

What to return if the type is not an application.

→ (∀ k l (f ∷ k → l) a. tb ~ Esc (f a) ⇒ uni (Esc f) → uni (Esc a) → r)

The continuation taking a function and an argument.

→ r 

Deconstruct a type application into the function and the argument and feed them to the continuation. If the type is not an application, then return the default value.

Instances

Instances details
HasUniApply DefaultUni Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

uniApply ∷ ∀ k l (f ∷ k → l) (a ∷ k). DefaultUni (Esc f) → DefaultUni (Esc a) → DefaultUni (Esc (f a)) Source #

matchUniApplyDefaultUni tb → r → (∀ k l (f ∷ k → l) (a ∷ k). tb ~ Esc (f a) ⇒ DefaultUni (Esc f) → DefaultUni (Esc a) → r) → r Source #

checkStar ∷ ∀ uni a (x ∷ a). Typeable a ⇒ uni (Esc x) → Maybe (a :~: Type) Source #

Check if the kind of the given type from the universe is Type.

withApplicable ∷ ∀ (a ∷ Type) (ab ∷ Type) f x uni m r. (Typeable ab, Typeable a, MonadPlus m) ⇒ uni (Esc (f ∷ ab)) → uni (Esc (x ∷ a)) → (∀ (b ∷ Type). (Typeable b, ab ~ (a → b)) ⇒ m r) → m r Source #

Check if one type from the universe can be applied to another (i.e. check that the expected kind of the argument matches the actual one) and call the continuation in the refined context. Fail with mzero otherwise.

tryUniApply ∷ (MonadPlus m, HasUniApply uni) ⇒ SomeTypeIn (Kinded uni) → SomeTypeIn (Kinded uni) → m (SomeTypeIn (Kinded uni)) Source #

Apply a type constructor to an argument, provided kinds match.

class GShow (t ∷ k → Type) where #

Methods

gshowsPrec ∷ ∀ (a ∷ k). Int → t a → ShowS #

Instances

Instances details
GShow SNat 
Instance details

Defined in Data.GADT.Internal

Methods

gshowsPrec ∷ ∀ (a ∷ k). IntSNat a → ShowS #

GShow SChar 
Instance details

Defined in Data.GADT.Internal

Methods

gshowsPrec ∷ ∀ (a ∷ k). IntSChar a → ShowS #

GShow SSymbol 
Instance details

Defined in Data.GADT.Internal

Methods

gshowsPrec ∷ ∀ (a ∷ k). IntSSymbol a → ShowS #

GShow DefaultUni Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

gshowsPrec ∷ ∀ (a ∷ k). IntDefaultUni a → ShowS #

GShow uni ⇒ GShow (Kinded uni ∷ TypeType) Source # 
Instance details

Defined in Universe.Core

Methods

gshowsPrec ∷ ∀ (a ∷ k). IntKinded uni a → ShowS #

(GShow uni, Closed uni, Everywhere uni Show) ⇒ GShow (ValueOf uni ∷ TypeType) Source # 
Instance details

Defined in Universe.Core

Methods

gshowsPrec ∷ ∀ (a ∷ k). IntValueOf uni a → ShowS #

GShow (TypeRep ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

gshowsPrec ∷ ∀ (a ∷ k0). IntTypeRep a → ShowS #

GShow ((:~:) a ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

gshowsPrec ∷ ∀ (a0 ∷ k0). Int → (a :~: a0) → ShowS #

GShow (GOrdering a ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

gshowsPrec ∷ ∀ (a0 ∷ k0). Int → GOrdering a a0 → ShowS #

(GShow a, GShow b) ⇒ GShow (Product a b ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

gshowsPrec ∷ ∀ (a0 ∷ k0). IntProduct a b a0 → ShowS #

(GShow a, GShow b) ⇒ GShow (Sum a b ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

gshowsPrec ∷ ∀ (a0 ∷ k0). IntSum a b a0 → ShowS #

GShow ((:~~:) a ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

gshowsPrec ∷ ∀ (a0 ∷ k0). Int → (a :~~: a0) → ShowS #

(GShow a, GShow b) ⇒ GShow (a :*: b ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

gshowsPrec ∷ ∀ (a0 ∷ k0). Int → (a :*: b) a0 → ShowS #

(GShow a, GShow b) ⇒ GShow (a :+: b ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

gshowsPrec ∷ ∀ (a0 ∷ k0). Int → (a :+: b) a0 → ShowS #

gshow ∷ ∀ {k} t (a ∷ k). GShow t ⇒ t a → String #

class GEq (f ∷ k → Type) where #

Methods

geq ∷ ∀ (a ∷ k) (b ∷ k). f a → f b → Maybe (a :~: b) #

Instances

Instances details
GEq SNat 
Instance details

Defined in Data.GADT.Internal

Methods

geq ∷ ∀ (a ∷ k) (b ∷ k). SNat a → SNat b → Maybe (a :~: b) #

GEq SChar 
Instance details

Defined in Data.GADT.Internal

Methods

geq ∷ ∀ (a ∷ k) (b ∷ k). SChar a → SChar b → Maybe (a :~: b) #

GEq SSymbol 
Instance details

Defined in Data.GADT.Internal

Methods

geq ∷ ∀ (a ∷ k) (b ∷ k). SSymbol a → SSymbol b → Maybe (a :~: b) #

GEq DefaultUni Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

geq ∷ ∀ (a ∷ k) (b ∷ k). DefaultUni a → DefaultUni b → Maybe (a :~: b) #

(GEq uni, Closed uni, Everywhere uni Eq) ⇒ GEq (ValueOf uni ∷ TypeType) Source # 
Instance details

Defined in Universe.Core

Methods

geq ∷ ∀ (a ∷ k) (b ∷ k). ValueOf uni a → ValueOf uni b → Maybe (a :~: b) #

GEq (TypeRep ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

geq ∷ ∀ (a ∷ k0) (b ∷ k0). TypeRep a → TypeRep b → Maybe (a :~: b) #

GEq ((:~:) a ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

geq ∷ ∀ (a0 ∷ k0) (b ∷ k0). (a :~: a0) → (a :~: b) → Maybe (a0 :~: b) #

(GEq a, GEq b) ⇒ GEq (Product a b ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

geq ∷ ∀ (a0 ∷ k0) (b0 ∷ k0). Product a b a0 → Product a b b0 → Maybe (a0 :~: b0) #

(GEq a, GEq b) ⇒ GEq (Sum a b ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

geq ∷ ∀ (a0 ∷ k0) (b0 ∷ k0). Sum a b a0 → Sum a b b0 → Maybe (a0 :~: b0) #

GEq ((:~~:) a ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

geq ∷ ∀ (a0 ∷ k0) (b ∷ k0). (a :~~: a0) → (a :~~: b) → Maybe (a0 :~: b) #

(GEq a, GEq b) ⇒ GEq (a :*: b ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

geq ∷ ∀ (a0 ∷ k0) (b0 ∷ k0). (a :*: b) a0 → (a :*: b) b0 → Maybe (a0 :~: b0) #

(GEq f, GEq g) ⇒ GEq (f :+: g ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

geq ∷ ∀ (a ∷ k0) (b ∷ k0). (f :+: g) a → (f :+: g) b → Maybe (a :~: b) #

defaultEq ∷ ∀ {k} f (a ∷ k) (b ∷ k). GEq f ⇒ f a → f b → Bool #

data (a ∷ k) :~: (b ∷ k) where infix 4 Source #

Propositional equality. If a :~: b is inhabited by some terminating value, then the type a is the same as the type b. To use this equality in practice, pattern-match on the a :~: b to get out the Refl constructor; in the body of the pattern-match, the compiler knows that a ~ b.

Since: base-4.7.0.0

Constructors

Refl ∷ ∀ {k} (a ∷ k). a :~: a 

Instances

Instances details
Category ((:~:) ∷ k → k → Type)

Since: base-4.7.0.0

Instance details

Defined in Control.Category

Methods

id ∷ ∀ (a ∷ k0). a :~: a Source #

(.) ∷ ∀ (b ∷ k0) (c ∷ k0) (a ∷ k0). (b :~: c) → (a :~: b) → a :~: c Source #

TestEquality ((:~:) a ∷ k → Type)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

testEquality ∷ ∀ (a0 ∷ k0) (b ∷ k0). (a :~: a0) → (a :~: b) → Maybe (a0 :~: b) Source #

GNFData ((:~:) a ∷ k → Type) 
Instance details

Defined in Data.GADT.DeepSeq

Methods

grnf ∷ ∀ (a0 ∷ k0). (a :~: a0) → ()

GCompare ((:~:) a ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

gcompare ∷ ∀ (a0 ∷ k0) (b ∷ k0). (a :~: a0) → (a :~: b) → GOrdering a0 b

GEq ((:~:) a ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

geq ∷ ∀ (a0 ∷ k0) (b ∷ k0). (a :~: a0) → (a :~: b) → Maybe (a0 :~: b) #

GRead ((:~:) a ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

greadsPrecInt → GReadS ((:~:) a)

GShow ((:~:) a ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

gshowsPrec ∷ ∀ (a0 ∷ k0). Int → (a :~: a0) → ShowS #

NFData2 ((:~:)TypeTypeType)

Since: deepseq-1.4.3.0

Instance details

Defined in Control.DeepSeq

Methods

liftRnf2 ∷ (a → ()) → (b → ()) → (a :~: b) → () Source #

NFData1 ((:~:) a)

Since: deepseq-1.4.3.0

Instance details

Defined in Control.DeepSeq

Methods

liftRnf ∷ (a0 → ()) → (a :~: a0) → () Source #

(a ~ b, Data a) ⇒ Data (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Data

Methods

gfoldl ∷ (∀ d b0. Data d ⇒ c (d → b0) → d → c b0) → (∀ g. g → c g) → (a :~: b) → c (a :~: b) Source #

gunfold ∷ (∀ b0 r. Data b0 ⇒ c (b0 → r) → c r) → (∀ r. r → c r) → Constr → c (a :~: b) Source #

toConstr ∷ (a :~: b) → Constr Source #

dataTypeOf ∷ (a :~: b) → DataType Source #

dataCast1Typeable t ⇒ (∀ d. Data d ⇒ c (t d)) → Maybe (c (a :~: b)) Source #

dataCast2Typeable t ⇒ (∀ d e. (Data d, Data e) ⇒ c (t d e)) → Maybe (c (a :~: b)) Source #

gmapT ∷ (∀ b0. Data b0 ⇒ b0 → b0) → (a :~: b) → a :~: b Source #

gmapQl ∷ (r → r' → r) → r → (∀ d. Data d ⇒ d → r') → (a :~: b) → r Source #

gmapQr ∷ ∀ r r'. (r' → r → r) → r → (∀ d. Data d ⇒ d → r') → (a :~: b) → r Source #

gmapQ ∷ (∀ d. Data d ⇒ d → u) → (a :~: b) → [u] Source #

gmapQiInt → (∀ d. Data d ⇒ d → u) → (a :~: b) → u Source #

gmapMMonad m ⇒ (∀ d. Data d ⇒ d → m d) → (a :~: b) → m (a :~: b) Source #

gmapMpMonadPlus m ⇒ (∀ d. Data d ⇒ d → m d) → (a :~: b) → m (a :~: b) Source #

gmapMoMonadPlus m ⇒ (∀ d. Data d ⇒ d → m d) → (a :~: b) → m (a :~: b) Source #

a ~ b ⇒ Bounded (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

minBound ∷ a :~: b Source #

maxBound ∷ a :~: b Source #

a ~ b ⇒ Enum (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

succ ∷ (a :~: b) → a :~: b Source #

pred ∷ (a :~: b) → a :~: b Source #

toEnumInt → a :~: b Source #

fromEnum ∷ (a :~: b) → Int Source #

enumFrom ∷ (a :~: b) → [a :~: b] Source #

enumFromThen ∷ (a :~: b) → (a :~: b) → [a :~: b] Source #

enumFromTo ∷ (a :~: b) → (a :~: b) → [a :~: b] Source #

enumFromThenTo ∷ (a :~: b) → (a :~: b) → (a :~: b) → [a :~: b] Source #

a ~ b ⇒ Read (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Show (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

showsPrecInt → (a :~: b) → ShowS Source #

show ∷ (a :~: b) → String Source #

showList ∷ [a :~: b] → ShowS Source #

NFData (a :~: b)

Since: deepseq-1.4.3.0

Instance details

Defined in Control.DeepSeq

Methods

rnf ∷ (a :~: b) → () Source #

Eq (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

(==) ∷ (a :~: b) → (a :~: b) → Bool Source #

(/=) ∷ (a :~: b) → (a :~: b) → Bool Source #

Ord (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

compare ∷ (a :~: b) → (a :~: b) → Ordering Source #

(<) ∷ (a :~: b) → (a :~: b) → Bool Source #

(<=) ∷ (a :~: b) → (a :~: b) → Bool Source #

(>) ∷ (a :~: b) → (a :~: b) → Bool Source #

(>=) ∷ (a :~: b) → (a :~: b) → Bool Source #

max ∷ (a :~: b) → (a :~: b) → a :~: b Source #

min ∷ (a :~: b) → (a :~: b) → a :~: b Source #

data DSum (tag ∷ k → Type) (f ∷ k → Type) #

Constructors

!(tag a) :=> (f a) 

Instances

Instances details
(GRead tag, Has' Read tag f) ⇒ Read (DSum tag f) 
Instance details

Defined in Data.Dependent.Sum

Methods

readsPrecIntReadS (DSum tag f) Source #

readListReadS [DSum tag f] Source #

readPrecReadPrec (DSum tag f) Source #

readListPrecReadPrec [DSum tag f] Source #

(GShow tag, Has' Show tag f) ⇒ Show (DSum tag f) 
Instance details

Defined in Data.Dependent.Sum

Methods

showsPrecIntDSum tag f → ShowS Source #

showDSum tag f → String Source #

showList ∷ [DSum tag f] → ShowS Source #

(GEq tag, Has' Eq tag f) ⇒ Eq (DSum tag f) 
Instance details

Defined in Data.Dependent.Sum

Methods

(==)DSum tag f → DSum tag f → Bool Source #

(/=)DSum tag f → DSum tag f → Bool Source #

(GCompare tag, Has' Eq tag f, Has' Ord tag f) ⇒ Ord (DSum tag f) 
Instance details

Defined in Data.Dependent.Sum

Methods

compareDSum tag f → DSum tag f → Ordering Source #

(<)DSum tag f → DSum tag f → Bool Source #

(<=)DSum tag f → DSum tag f → Bool Source #

(>)DSum tag f → DSum tag f → Bool Source #

(>=)DSum tag f → DSum tag f → Bool Source #

maxDSum tag f → DSum tag f → DSum tag f Source #

minDSum tag f → DSum tag f → DSum tag f Source #