Documentation

Instantiate type variables in the type of a value using ElaborateFromTo. Example usages:

>>> :t elaborateDebug False
elaborateDebug False :: Bool
>>> :t elaborateDebug fst
elaborateDebug fst
  :: (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
     -> TyVarRep ('TyNameRep "a" 0)

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.

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.