Documentation

The class Typeable allows a concrete representation of a type to be calculated.

The type of type schemes of built-in functions. args is a list of types of arguments, res is the resulting type. E.g. Text -> Bool -> Integer is encoded as TypeScheme val [Text, Bool] Integer.

Convert a TypeScheme to the corresponding Kind.

An instance of this class not having any constraints ensures that every type (according to Everywhere) from the universe has 'KnownTypeAst, ReadKnownIn and MakeKnownIn instances.

A BuiltinRuntime represents a possibly partial builtin application, including an empty builtin application (i.e. just the builtin with no arguments).

Applying or type-instantiating a builtin peels off the corresponding constructor from its BuiltinRuntime.

BuiltinCostedResult contains the cost (an ExBudgetStream) and the result (a BuiltinResult (HeadSpine val)) of the builtin application. The cost is stored strictly, since the evaluator is going to look at it and the result is stored lazily, since it's not supposed to be forced before accounting for the cost of the application. If the cost exceeds the available budget, the evaluator discards the result of the builtin application without ever forcing it and terminates with evaluation failure. Allowing the user to compute something that they don't have the budget for would be a major bug.

Evaluators that ignore the entire concept of costing (e.g. the CK machine) may of course force the result of the builtin application unconditionally.

A data wrapper around a function returning the BuiltinRuntime of a built-in function.

In order for lookups to be efficient the BuiltinRuntimes need to be cached, i.e. pulled out of the function statically. See makeBuiltinMeaning for how we achieve that.

Look up the runtime info of a built-in function during evaluation.

The type of errors that can occur during evaluation. There are two kinds of errors:

1. Structural ones -- these are errors that are indicative of the _structure_ of the program being wrong. For example, a free variable was encountered during evaluation, a non-function was applied to an argument or tailList was applied to a non-list.
2. Operational ones -- these are errors that are indicative of the _logic_ of the program being wrong. For example, error was executed, tailList was applied to an empty list or evaluation ran out of gas.

On the chain both of these are just regular failures and we don't distinguish between them there: if a script fails, it fails, it doesn't matter what the reason was. However in the tests it does matter why the failure occurred: a structural error may indicate that the test was written incorrectly while an operational error may be entirely expected.

In other words, structural errors are "runtime type errors" and operational errors are regular runtime errors. Which means that evaluating an (erased) well-typed program should never produce a structural error, only an operational one. This creates a sort of "runtime type system" for UPLC and it would be great to stick to it and enforce in tests etc, but we currently don't.

The error message part of an UnliftingEvaluationError.

When unlifting of a PLC term into a Haskell value fails, this error is thrown.

The type of errors that readKnown and makeKnown can return.

The monad that makeKnown runs in. Equivalent to ExceptT BuiltinError (Writer (DList Text)), except optimized in two ways:

1. everything is strict
2. has the BuiltinSuccess constructor that is used for returning a value with no logs attached, which is the most common case for us, so it helps a lot not to construct and deconstruct a redundant tuple

Moving from ExceptT BuiltinError (Writer (DList Text)) to this data type gave us a speedup of 8% of total evaluation time.

Logs are represented as a DList, because we don't particularly care about the efficiency of logging, since there's no logging on the chain and builtins don't emit much anyway. Otherwise we'd have to use text-builder or text-builder-linear or something of this sort.

Construct a prism focusing on the *EvaluationFailure part of err by taking that *EvaluationFailure and

1. pretty-printing and embedding it into an UnliftingError for the setter part of the prism
2. returning it directly for the opposite direction (there's no other way to convert an UnliftingError to an evaluation failure, since the latter doesn't carry any content)

This is useful for providing AsUnliftingError instances for types such as CkUserError and CekUserError.

Add a log line to the logs.

Prepend logs to a BuiltinResult computation.

The AST of a value with a Plutus type attached to it. The type is for the Plutus type checker to look at. Opaque can appear in the type of the denotation of a builtin.

For unlifting from the Constant constructor when the stored value is of a monomorphic built-in type

The rep parameter specifies how the type looks on the PLC side (i.e. just like with Opaque val rep).

Representation of a type variable: its name and unique and an implicit kind.

Representation of an intrinsically-kinded type variable: a name.

Representation of an intrinsically-kinded type application: a function and an argument.

Representation of of an intrinsically-kinded universal quantifier: a bound name and a body.

For annotating an uninstantiated built-in type, so that it gets handled by the right instance or type family.

LastArg x y is the same thing as y in the signature of the denotation of a built-in functions and this type is only used for referencing x before y, so that the elaboration machinery generates x before y in the all part of the Plutus signature of the builtin. This is a very hacky and indirect way of specifying the ordering of type variables in a Plutus signature, in future we'll do it explicitly by introducing a Forall binder for use in type signatures of denotations of builtins.

Take an iterated application of a built-in type and elaborate every function application inside of it to TyAppRep and annotate the head with BuiltinHead.

The idea is that we don't need to process built-in types manually if we simply add some annotations for instance resolution to look for. Think what we'd have to do manually for, say, ToHoles: traverse the spine of the application and collect all the holes into a list, which is troubling, because type applications are left-nested and lists are right-nested, so we'd have to use accumulators or an explicit Reverse type family. And then we also have KnownTypeAst and ToBinds, so handling built-in types in a special way for each of those would be a hassle, especially given the fact that type-level Haskell is not exactly good at computing things. With the ElaborateBuiltin approach we get KnownTypeAst, ToHoles and ToBinds for free.

We make this an open type family, so that elaboration is customizable for each universe.

Take a constraint and use it to constrain every argument of a possibly 0-ary elaborated application of a built-in type.

Take a constraint and use it to constrain every argument of a possibly 0-ary application of a built-in type.

Turn a list of Haskell types args into a functional type ending in res.

>>> :set -XDataKinds
>>> :kind! FoldArgs [(), Bool] Integer
FoldArgs [(), Bool] Integer :: *
= () -> Bool -> Integer 

The meaning of a built-in function consists of its type represented as a TypeScheme, its Haskell denotation and its uninstantiated runtime denotation.

The TypeScheme of a built-in function is used for example for

1. computing the PLC type of the function to be used during type checking
2. getting arity information
3. generating arbitrary values to apply the function to in tests

The denotation is lazy, so that we don't need to worry about a builtin being bottom (happens in tests). The production path is not affected by that, since only runtime denotations are used for evaluation.

Constraints available when defining a built-in function.

A type class for "each function from a set of built-in functions has a BuiltinMeaning".

Feed the TypeScheme of the given built-in function to the continuation.

Get the type of a built-in function.

Chop a function type to get a list of its argument types.

A class that allows us to derive a monotype for a builtin. We could've computed the runtime denotation from the TypeScheme and the denotation of the builtin, but not statically (due to unfolding not working for recursive functions and TypeScheme being recursive, i.e. requiring the conversion function to be recursive), and so it would cause us to retain a lot of evaluation-irrelevant stuff in the constructors of BuiltinRuntime, which has to make evaluation slower (we didn't check) and certainly makes the generated Core much harder to read. Technically speaking, we could get a RuntimeScheme from the TypeScheme and the denotation statically if we changed the definition of TypeScheme and made it a singleton, but then the conversion function would have to become a class anyway and we'd just replicate what we have here, except in a much more complicated way.

A class that allows us to derive a polytype for a builtin.

Ensure a built-in function is not nullary and throw a nice error otherwise.

A function turned into a type class with exactly one fully general instance. We can't package up the constraints of makeBuiltinMeaning (see the instance) into a type or class synonym, because they contain a bunch of variables defined by ~ or determined via functional dependencies and neither class nor type definitions can handle that (see https://gitlab.haskell.org/ghc/ghc/-/issues/7100). Inlining three lines of constraints whenever we need to call makeBuiltinMeaning over a non-concrete type is a bad option and this abstraction is free anyway, hence its existence.

The a type variable goes first, because makeBuiltinMeaning @A is a common pattern.

Convert a BuiltinMeaning to a BuiltinRuntime given a cost model.

Calculate runtime info for all built-in functions given meanings of builtins (as a constraint), the semantics variant of the set of builtins and a cost model.

Representation of a type variable: its name and unique and an implicit kind.

Representation of an intrinsically-kinded type variable: a name.

Representation of an intrinsically-kinded type application: a function and an argument.

Representation of of an intrinsically-kinded universal quantifier: a bound name and a body.

The kind of holes.

A hole in the Rep context.

A hole in the Type context.

Turn a hole in the GHC.Type -> GHC.Type form into one of the Hole form. This only changes the kind of the given argument. This is a way of encoding forall a. a -> Hole at the kind level, which we don't attempt to use, because GHC apparently hates polymorphism at the kind level and chokes upon encountering it.

Specifies that the given type is a built-in one and its values can be embedded into a Term.

Specifies that the given type is a built-in one and can be embedded into a Kind.

The product of HasTypeLevel and HasTermLevel.

Convert a Haskell representation of a possibly 0-ary application of a built-in type to arbitrary types implementing KnownTypeAst.

A constraint for "a is a KnownTypeAst by means of being included in uni".

This class allows one to convert the type-level Haskell representation of a Plutus type into the corresponding Plutus type. Associated type families are needed to help elaboration.

Depending on the universe converting a Haskell type to a Plutus team can give different results (e.g. Int can be a built-in type instead of being encoded via built-in Integer), hence this class takes a uni argument. Plus, elaboration is universe-specific too.