HORIZON HASKELLDocslts/ghc-9.14.xd82dee82026-10-12Search names, modules, packages, or :: a typeCtrl K

GHC 9.14.1 · lts/ghc-9.14.x · d82dee8 · 2026-10-12

Moduleplutus-core-1.70.0.0

PlutusCore

  • 46 types
  • 9 classes
  • 55 values
valuemapFun
  1. :: fun -> fun'
  2. -> Term tyname name uni fun ann
  3. -> Term tyname name uni fun' ann
#
valuetermMapNames
  1. :: tyname -> tyname'
  2. -> name -> name'
  3. -> Term tyname name uni fun ann
  4. -> Term tyname' name' uni fun ann
#
datadata (:~:) (a :: k) (b :: k) where
#

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.

Constructors

Instances24Category, Groupoid, Semigroupoid, TestCoercion, TestEquality, EqP, …
  • Category (:~:)Defined in ghc-internal-9.1401.0 · GHC.Internal.Control.Category
  • Groupoid (:~:)Defined in semigroupoids-6.0.2 · Data.Groupoid
  • Semigroupoid (:~:)Defined in semigroupoids-6.0.2 · Data.Semigroupoid
  • TestCoercion ((:~:) a)Defined in ghc-internal-9.1401.0 · GHC.Internal.Data.Type.Coercion
  • TestEquality ((:~:) a)Defined in ghc-internal-9.1401.0 · GHC.Internal.Data.Type.Equality
  • EqP ((:~:) a)Defined in some-1.0.6 · Data.EqP
  • GCompare ((:~:) a)Defined in some-1.0.6 · Data.GADT.Internal
  • GEq ((:~:) a)Defined in some-1.0.6 · Data.GADT.Internal
  • GNFData ((:~:) a)Defined in some-1.0.6 · Data.GADT.DeepSeq
  • GRead ((:~:) a)Defined in some-1.0.6 · Data.GADT.Internal
  • GShow ((:~:) a)Defined in some-1.0.6 · Data.GADT.Internal
  • OrdP ((:~:) a)Defined in some-1.0.6 · Data.OrdP
  • NFData2 (:~:)Defined in deepseq-1.5.1.0 · Control.DeepSeq
  • NFData1 ((:~:) a)Defined in deepseq-1.5.1.0 · Control.DeepSeq
  • a ~ b => Bounded (a :~: b)Defined in ghc-internal-9.1401.0 · GHC.Internal.Data.Type.Equality
  • a ~ b => Enum (a :~: b)Defined in ghc-internal-9.1401.0 · GHC.Internal.Data.Type.Equality
  • Eq (a :~: b)Defined in ghc-internal-9.1401.0 · GHC.Internal.Data.Type.Equality
  • (a ~ b, Data a) => Data (a :~: b)Defined in ghc-internal-9.1401.0 · GHC.Internal.Data.Data
  • Ord (a :~: b)Defined in ghc-internal-9.1401.0 · GHC.Internal.Data.Type.Equality
  • a ~ b => Read (a :~: b)Defined in ghc-internal-9.1401.0 · GHC.Internal.Data.Type.Equality
  • Show (a :~: b)Defined in ghc-internal-9.1401.0 · GHC.Internal.Data.Type.Equality
  • NFData (a :~: b)Defined in deepseq-1.5.1.0 · Control.DeepSeq
  • a ~ b => Boring (a :~: b)Defined in boring-0.2.2.1 · Data.Boring

    Homogeneous type equality is Boring too.

  • HasDict (a ~ b) (a :~: b)Defined in constraints-0.14.4 · Data.Constraint
methodshow :: a -> String
#

A specialised variant of showsPrec, using precedence context zero, and returning an ordinary String.

datadata SourcePos
#

The data type SourcePos represents source positions. It contains the name of the source file, a line number, and a column number. Source line and column positions change intensively during parsing, so we need to make them strict to avoid memory leaks.

Instances9Eq, Data, Ord, Read, Show, Generic, …
datadata SrcSpan
#

Constructors

Instances10Eq, Ord, Show, Generic, NFData, Pretty, …
newtypenewtype SrcSpans
#
Instances13Eq, Ord, Show, Generic, Semigroup, Monoid, …
familytype family HasUniques a :: Constraint
#
Instances6HasUniques
datadata Kind ann
#

Constructors

Instances17Functor, CollectScopeInfo, EstablishScoping, Lift, Eq, Show, …
newtypenewtype Normalized a
#

Constructors

Instances13Functor, Applicative, Foldable, Traversable, PrettyBy, Eq, …
datadata Program tyname name (uni :: Type -> Type) fun ann
#

Constructors

Instances15PrettyBy, Functor, CollectScopeInfo, EstablishScoping, Eq, Show, …
datadata Term tyname name (uni :: Type -> Type) fun ann
#

Constructors

Instances24Reference, PrettyBy, Functor, HasAnn, CollectScopeInfo, EstablishScoping, …
datadata Type tyname (uni :: Type -> Type) ann
#

Constructors

Instances20Reference, PrettyBy, Functor, HasAnn, CollectScopeInfo, EstablishScoping, …
familytype family UniOf a :: Type -> Type
#
Instances6UniOf
  • type UniOf (Opaque val rep) = UniOf valDefined in plutus-core-1.70.0.0 · PlutusCore.Builtin.Polymorphism
  • type UniOf (SomeConstant uni rep) = uniDefined in plutus-core-1.70.0.0 · PlutusCore.Builtin.Polymorphism
  • type UniOf (Term tyname name uni fun ann) = uniDefined in plutus-core-1.70.0.0 · PlutusCore.Core.Type
  • type UniOf (CkValue uni fun) = uniDefined in plutus-core-1.70.0.0 · PlutusCore.Evaluation.Machine.Ck
  • type UniOf (Term name uni fun ann) = uniDefined in plutus-core-1.70.0.0 · UntypedPlutusCore.Core.Type
  • type UniOf (CekValue uni fun ann) = uniDefined in plutus-core-1.70.0.0 · UntypedPlutusCore.Evaluation.Machine.Cek.Internal
newtypenewtype DeBruijn
#

Constructors

Instances13Show, Generic, NFData, HasIndex, PrettyBy, Flat, …
datadata FreeVariableError
#

Constructors

Instances9Eq, Ord, Show, Generic, Exception, NFData, …
datadata NamedDeBruijn
#

Constructors

Instances15Read, Show, Generic, NFData, HasIndex, PrettyBy, …
newtypenewtype NamedTyDeBruijn
#

Constructors

Instances13Show, Generic, NFData, Wrapped, HasIndex, PrettyBy, …
newtypenewtype TyDeBruijn
#

Constructors

Instances12Show, Generic, NFData, Wrapped, Flat, HasIndex, …
datadata DefaultFun
#
AddIntegerSubtractIntegerMultiplyIntegerDivideIntegerQuotientIntegerRemainderIntegerModIntegerEqualsIntegerLessThanIntegerLessThanEqualsIntegerAppendByteStringConsByteStringSliceByteStringLengthOfByteStringIndexByteStringEqualsByteStringLessThanByteStringLessThanEqualsByteStringSha2_256Sha3_256Blake2b_256VerifyEd25519SignatureVerifyEcdsaSecp256k1SignatureVerifySchnorrSecp256k1SignatureAppendStringEqualsStringEncodeUtf8DecodeUtf8IfThenElseChooseUnitTraceFstPairSndPairChooseListMkConsHeadListTailListNullListChooseDataConstrDataMapDataListDataIDataBDataUnConstrDataUnMapDataUnListDataUnIDataUnBDataEqualsDataSerialiseDataMkPairDataMkNilDataMkNilPairDataBls12_381_G1_addBls12_381_G1_negBls12_381_G1_scalarMulBls12_381_G1_equalBls12_381_G1_hashToGroupBls12_381_G1_compressBls12_381_G1_uncompressBls12_381_G2_addBls12_381_G2_negBls12_381_G2_scalarMulBls12_381_G2_equalBls12_381_G2_hashToGroupBls12_381_G2_compressBls12_381_G2_uncompressBls12_381_millerLoopBls12_381_mulMlResultBls12_381_finalVerifyKeccak_256Blake2b_224IntegerToByteStringByteStringToIntegerAndByteStringOrByteStringXorByteStringComplementByteStringReadBitWriteBitsReplicateByteShiftByteStringRotateByteStringCountSetBitsFindFirstSetBitRipemd_160ExpModIntegerDropListLengthOfArrayListToArrayIndexArrayBls12_381_G1_multiScalarMulBls12_381_G2_multiScalarMulInsertCoinLookupCoinUnionValueValueContainsValueDataUnValueDataScaleValueMultiIndexArrayPoliciesAssetCountKeepPoliciesDropPolicies
Instances29Ix, Hashable, Flat, ExMemoryUsage, PrettyBy, ToBuiltinMeaning, …
datadata DefaultUni a where
#

Constructors

Instances240ToKind, Closed, HasUniApply, AnnotateCaseBuiltin, CaseBuiltin, TestTypesFromTheUniverseAreAllKnown, …
datadata Error (uni :: Type -> Type) fun ann
#

Constructors

Instances7PrettyBy, Functor, Eq, Show, Generic, NFData, …
datadata NormCheckError tyname name (uni :: Type -> Type) fun ann
#

Constructors

Instances7PrettyBy, Functor, Eq, Show, Generic, NFData, …
datadata ParserError
#

Constructors

Instances8Eq, Ord, Show, Generic, NFData, Pretty, …
datadata TypeError term (uni :: Type -> Type) fun ann
#
Instances7PrettyBy, Functor, Eq, Show, Generic, NFData, …
datadata UniqueError ann
#

Constructors

Instances8Functor, Eq, Show, Generic, Exception, NFData, …
datadata EvaluationResult a
#

Constructors

Instances21Monad, Functor, MonadFail, Applicative, Foldable, Traversable, …
datadata Name
#

Constructors

Instances21Ord, Show, Generic, NFData, Pretty, HasText, …
newtypenewtype TyName
#

Constructors

Instances23Ord, Show, Generic, NFData, Pretty, Hashable, …
newtypenewtype Unique
#

Constructors

Instances10Enum, Eq, Ord, Show, NFData, Pretty, …
  • Enum UniqueDefined in plutus-core-1.70.0.0 · PlutusCore.Name.Unique
  • Eq UniqueDefined in plutus-core-1.70.0.0 · PlutusCore.Name.Unique
  • Ord UniqueDefined in plutus-core-1.70.0.0 · PlutusCore.Name.Unique
  • Show UniqueDefined in plutus-core-1.70.0.0 · PlutusCore.Name.Unique
  • NFData UniqueDefined in plutus-core-1.70.0.0 · PlutusCore.Name.Unique
  • Pretty UniqueDefined in plutus-core-1.70.0.0 · PlutusCore.Name.Unique
  • Hashable UniqueDefined in plutus-core-1.70.0.0 · PlutusCore.Name.Unique
  • Flat UniqueDefined in plutus-core-1.70.0.0 · PlutusCore.FlatInstances · orphan
  • Lift UniqueDefined in plutus-core-1.70.0.0 · PlutusCore.Name.Unique
  • HasUnique Unique UniqueDefined in plutus-core-1.70.0.0 · PlutusCore.Name.Unique
newtypenewtype UniqueMap unique a
#

Constructors

Instances6Functor, Foldable, Eq, Show, Semigroup, Monoid
  • Functor (UniqueMap unique)Defined in plutus-core-1.70.0.0 · PlutusCore.Name.UniqueMap
  • Foldable (UniqueMap unique)Defined in plutus-core-1.70.0.0 · PlutusCore.Name.UniqueMap
  • Eq a => Eq (UniqueMap unique a)Defined in plutus-core-1.70.0.0 · PlutusCore.Name.UniqueMap
  • Show a => Show (UniqueMap unique a)Defined in plutus-core-1.70.0.0 · PlutusCore.Name.UniqueMap
  • Semigroup (UniqueMap unique a)Defined in plutus-core-1.70.0.0 · PlutusCore.Name.UniqueMap
  • Monoid (UniqueMap unique a)Defined in plutus-core-1.70.0.0 · PlutusCore.Name.UniqueMap
classclass Monad m => MonadQuote (m :: Type -> Type) where
#

Methods

Instances11MonadQuote, …
newtypenewtype QuoteT (m :: Type -> Type) a
#
Instances12MonadTrans, MFunctor, MonadError, MonadReader, MonadState, MonadWriter, …
classclass Rename a where
#

Methods

Instances6Rename
datadata Version
#

Constructors

Instances9Eq, Ord, Show, Generic, NFData, Pretty, …
classclass HasAnn (f :: Type -> Type) where
#

Methods

Instances3HasAnn
  • HasAnn (Type tyname uni)Defined in plutus-core-1.70.0.0 · PlutusCore.Core.Type
  • HasAnn (Term name uni fun)Defined in plutus-core-1.70.0.0 · UntypedPlutusCore.Core.Type
  • HasAnn (Term tyname name uni fun)Defined in plutus-core-1.70.0.0 · PlutusCore.Core.Type
classclass Contains (uni :: Type -> Type) (a :: k) where
#

Methods

Instances16Contains, …
datadata Esc (a :: k)
#
datadata Kinded (uni :: Type -> Type) ta where
#

Constructors

Instances4GShow, Contains, Pretty, Show
datadata SomeTypeIn (uni :: Type -> Type)
#

Constructors

Instances9PrettyBy, Eq, Ord, Show, NFData, Pretty, …
datadata ValueOf (uni :: Type -> Type) a
#

Constructors

Instances16GCompare, GEq, GNFData, GShow, PrettyBy, Eq, …
classclass GEq (f :: k -> Type) where
#

A class for type-contexts which contain enough information to (at least in some cases) decide the equality of types occurring within them.

This class is sometimes confused with TestEquality from base. TestEquality only checks type equality.

Consider

Example1 expression
data Tag a where TagInt1 :: Tag Int; TagInt2 :: Tag Int

The correct TestEquality Tag instance is

Example1 expression
:{instance TestEquality Tag where    testEquality TagInt1 TagInt1 = Just Refl    testEquality TagInt1 TagInt2 = Just Refl    testEquality TagInt2 TagInt1 = Just Refl    testEquality TagInt2 TagInt2 = Just Refl:}

While we can define

instance GEq Tag where
   geq = testEquality

this will mean we probably want to have

instance Eq Tag where
   _ == _ = True

Note: In the future version of some package (to be released around GHC-9.6 / 9.8) the forall a. Eq (f a) constraint will be added as a constraint to GEq, with a law relating GEq and Eq:

geq x y = Just Refl   ⇒  x == y = True        ∀ (x :: f a) (y :: f b)
x == y                ≡  isJust (geq x y)     ∀ (x, y :: f a)

So, the more useful GEq Tag instance would differentiate between different constructors:

Example1 expression
:{instance GEq Tag where    geq TagInt1 TagInt1 = Just Refl    geq TagInt1 TagInt2 = Nothing    geq TagInt2 TagInt1 = Nothing    geq TagInt2 TagInt2 = Just Refl:}

which is consistent with a derived Eq instance for Tag

Example1 expression
deriving instance Eq (Tag a)

Note that even if a ~ b, the geq (x :: f a) (y :: f b) may be Nothing (when value terms are inequal).

The consistency of GEq and Eq is easy to check by exhaustion:

Example2 expressions
let checkFwdGEq :: (forall a. Eq (f a), GEq f) => f a -> f b -> Bool; checkFwdGEq x y = case geq x y of Just Refl -> x == y; Nothing -> True(checkFwdGEq TagInt1 TagInt1, checkFwdGEq TagInt1 TagInt2, checkFwdGEq TagInt2 TagInt1, checkFwdGEq TagInt2 TagInt2)(True,True,True,True)
Example2 expressions
let checkBwdGEq :: (Eq (f a), GEq f) => f a -> f a -> Bool; checkBwdGEq x y = if x == y then isJust (geq x y) else isNothing (geq x y)(checkBwdGEq TagInt1 TagInt1, checkBwdGEq TagInt1 TagInt2, checkBwdGEq TagInt2 TagInt1, checkBwdGEq TagInt2 TagInt2)(True,True,True,True)

Methods

  • geq :: f a -> f b -> Maybe (a :~: b)

    Produce a witness of type-equality, if one exists.

    A handy idiom for using this would be to pattern-bind in the Maybe monad, eg.:

    extract :: GEq tag => tag a -> DSum tag -> Maybe a
extract t1 (t2 :=> x) = do
    Refl <- geq t1 t2
    return x

    Or in a list comprehension:

    extractMany :: GEq tag => tag a -> [DSum tag] -> [a]
extractMany t1 things = [ x | (t2 :=> x) <- things, Refl <- maybeToList (geq t1 t2)]

    (Making use of the DSum type from Data.Dependent.Sum in both examples)

Instances15GEq, …
  • GEq SBinDefined in bin-0.1.4.1 · Data.Type.Bin
  • GEq SBinPDefined in bin-0.1.4.1 · Data.Type.BinP
  • GEq SNatDefined in fin-0.3.2 · Data.Type.Nat
  • GEq SCharDefined in some-1.0.6 · Data.GADT.Internal
  • GEq SSymbolDefined in some-1.0.6 · Data.GADT.Internal
  • GEq SNatDefined in some-1.0.6 · Data.GADT.Internal
  • GEq DefaultUniDefined in plutus-core-1.70.0.0 · PlutusCore.Default.Universe
  • GEq TypeRepDefined in some-1.0.6 · Data.GADT.Internal
  • (GEq uni, Closed uni, Everywhere uni Eq) => GEq (ValueOf uni)Defined in plutus-core-1.70.0.0 · Universe.Core
  • GEq ((:~:) a)Defined in some-1.0.6 · Data.GADT.Internal
  • GEq ((:~~:) a)Defined in some-1.0.6 · Data.GADT.Internal
  • (GEq a, GEq b) => GEq (Product a b)Defined in some-1.0.6 · Data.GADT.Internal
  • (GEq a, GEq b) => GEq (Sum a b)Defined in some-1.0.6 · Data.GADT.Internal
  • (GEq a, GEq b) => GEq (a :*: b)Defined in some-1.0.6 · Data.GADT.Internal
  • (GEq f, GEq g) => GEq (f :+: g)Defined in some-1.0.6 · Data.GADT.Internal
classclass GShow (t :: k -> Type) where
#

Show-like class for 1-type-parameter GADTs. GShow t => ... is equivalent to something like (forall a. Show (t a)) => .... The easiest way to create instances would probably be to write (or derive) an instance Show (T a), and then simply say:

instance GShow t where gshowsPrec = defaultGshowsPrec

Methods

Instances21GShow, …
  • GShow PosDefined in bin-0.1.4.1 · Data.Bin.Pos
  • GShow PosPDefined in bin-0.1.4.1 · Data.BinP.PosP
  • GShow SBinDefined in bin-0.1.4.1 · Data.Type.Bin
  • GShow SBinPDefined in bin-0.1.4.1 · Data.Type.BinP
  • GShow FinDefined in fin-0.3.2 · Data.Fin
  • GShow SNatDefined in fin-0.3.2 · Data.Type.Nat
  • GShow SCharDefined in some-1.0.6 · Data.GADT.Internal
  • GShow SSymbolDefined in some-1.0.6 · Data.GADT.Internal
  • GShow SNatDefined in some-1.0.6 · Data.GADT.Internal
  • GShow DefaultUniDefined in plutus-core-1.70.0.0 · PlutusCore.Default.Universe
  • SNatI n => GShow (PosP' n)Defined in bin-0.1.4.1 · Data.BinP.PosP
  • GShow TypeRepDefined in some-1.0.6 · Data.GADT.Internal
  • GShow uni => GShow (Kinded uni)Defined in plutus-core-1.70.0.0 · Universe.Core
  • (GShow uni, Closed uni, Everywhere uni Show) => GShow (ValueOf uni)Defined in plutus-core-1.70.0.0 · Universe.Core
  • GShow (GOrdering a)Defined in some-1.0.6 · Data.GADT.Internal
  • GShow ((:~:) a)Defined in some-1.0.6 · Data.GADT.Internal
  • GShow ((:~~:) a)Defined in some-1.0.6 · Data.GADT.Internal
  • (GShow a, GShow b) => GShow (Product a b)Defined in some-1.0.6 · Data.GADT.Internal
    Example1 expression
    gshow (Pair Refl Refl :: Product ((:~:) Int) ((:~:) Int) Int)"Pair Refl Refl"
  • (GShow a, GShow b) => GShow (Sum a b)Defined in some-1.0.6 · Data.GADT.Internal
    Example1 expression
    gshow (InL Refl :: Sum ((:~:) Int) ((:~:) Bool) Int)"InL Refl"
  • (GShow a, GShow b) => GShow (a :*: b)Defined in some-1.0.6 · Data.GADT.Internal
    Example1 expression
    gshow (Pair Refl Refl :: Product ((:~:) Int) ((:~:) Int) Int)"Refl :*: Refl"
  • (GShow a, GShow b) => GShow (a :+: b)Defined in some-1.0.6 · Data.GADT.Internal
    Example1 expression
    gshow (L1 Refl :: ((:~:) Int :+: (:~:) Bool) Int)"L1 Refl"
newtypenewtype Some (tag :: k -> Type)
#

Existential. This is type is useful to hide GADTs' parameters.

Example4 expressions
data Tag :: Type -> Type where TagInt :: Tag Int; TagBool :: Tag Boolinstance GShow Tag where gshowsPrec _ TagInt = showString "TagInt"; gshowsPrec _ TagBool = showString "TagBool"classify s = case s of "TagInt" -> [mkGReadResult TagInt]; "TagBool" -> [mkGReadResult TagBool]; _ -> []instance GRead Tag where greadsPrec _ s = [ (r, rest) | (con, rest) <-  lex s, r <- classify con ]

You can either use PatternSynonyms (available with GHC >= 8.0)

Example2 expressions
let x = Some TagIntxSome TagInt
Example1 expression
case x of { Some TagInt -> "I"; Some TagBool -> "B" } :: String"I"

or you can use functions

Example2 expressions
let y = mkSome TagBoolySome TagBool
Example1 expression
withSome y $ \y' -> case y' of { TagInt -> "I"; TagBool -> "B" } :: String"B"

The implementation of mapSome is safe.

Example2 expressions
let f :: Tag a -> Tag a; f TagInt = TagInt; f TagBool = TagBoolmapSome f ySome TagBool

but you can also use:

Example1 expression
withSome y (mkSome . f)Some TagBool
Example1 expression
read "Some TagBool" :: Some TagSome TagBool
Example1 expression
read "mkSome TagInt" :: Some TagSome TagInt
Instances12PrettyBy, Eq, Ord, Read, Show, Semigroup, …
patternpattern Some :: tag a -> Some tag
#