Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- type family FoldArgs args res where ...
- data BuiltinMeaning val cost = ∀ args res. BuiltinMeaning (TypeScheme val args res) ~(FoldArgs args res) (cost → BuiltinRuntime val)
- type HasMeaningIn uni val = (Typeable val, ExMemoryUsage val, HasConstantIn uni val)
- class (Typeable uni, Typeable fun, Bounded fun, Enum fun, Ix fun, Default (BuiltinSemanticsVariant fun)) ⇒ ToBuiltinMeaning uni fun where
- type CostingPart uni fun
- data BuiltinSemanticsVariant fun
- toBuiltinMeaning ∷ HasMeaningIn uni val ⇒ BuiltinSemanticsVariant fun → fun → BuiltinMeaning val (CostingPart uni fun)
- withTypeSchemeOfBuiltinFunction ∷ ∀ val fun r. (ToBuiltinMeaning (UniOf val) fun, ExMemoryUsage val, Typeable val, HasConstant val) ⇒ BuiltinSemanticsVariant fun → fun → (∀ args res. TypeScheme val args res → r) → r
- typeOfBuiltinFunction ∷ ∀ uni fun. ToBuiltinMeaning uni fun ⇒ BuiltinSemanticsVariant fun → fun → Type TyName uni ()
- type family GetArgs a where ...
- class KnownMonotype val args res where
- knownMonotype ∷ TypeScheme val args res
- toMonoF ∷ ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream) → BuiltinRuntime val
- class KnownMonotype val args res ⇒ KnownPolytype (binds ∷ [Some TyNameRep]) val args res where
- knownPolytype ∷ TypeScheme val args res
- toPolyF ∷ ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream) → BuiltinRuntime val
- type family ThrowOnBothEmpty binds args isBuiltin a where ...
- class MakeBuiltinMeaning a val where
- makeBuiltinMeaning ∷ a → (cost → FoldArgs (GetArgs a) ExBudgetStream) → BuiltinMeaning val cost
- toBuiltinRuntime ∷ cost → BuiltinMeaning val cost → BuiltinRuntime val
- toBuiltinsRuntime ∷ (cost ~ CostingPart uni fun, ToBuiltinMeaning uni fun, HasMeaningIn uni val) ⇒ BuiltinSemanticsVariant fun → cost → BuiltinsRuntime fun val
Documentation
type family FoldArgs args res where ... Source #
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
data BuiltinMeaning val cost Source #
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
- computing the PLC type of the function to be used during type checking
- getting arity information
- 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.
∀ args res. BuiltinMeaning (TypeScheme val args res) ~(FoldArgs args res) (cost → BuiltinRuntime val) |
type HasMeaningIn uni val = (Typeable val, ExMemoryUsage val, HasConstantIn uni val) Source #
Constraints available when defining a built-in function.
class (Typeable uni, Typeable fun, Bounded fun, Enum fun, Ix fun, Default (BuiltinSemanticsVariant fun)) ⇒ ToBuiltinMeaning uni fun where Source #
A type class for "each function from a set of built-in functions has a BuiltinMeaning
".
type CostingPart uni fun Source #
The cost
part of BuiltinMeaning
.
data BuiltinSemanticsVariant fun Source #
See Note [Builtin semantics variants]
toBuiltinMeaning ∷ HasMeaningIn uni val ⇒ BuiltinSemanticsVariant fun → fun → BuiltinMeaning val (CostingPart uni fun) Source #
Get the BuiltinMeaning
of a built-in function.
Instances
withTypeSchemeOfBuiltinFunction ∷ ∀ val fun r. (ToBuiltinMeaning (UniOf val) fun, ExMemoryUsage val, Typeable val, HasConstant val) ⇒ BuiltinSemanticsVariant fun → fun → (∀ args res. TypeScheme val args res → r) → r Source #
Feed the TypeScheme
of the given built-in function to the continuation.
typeOfBuiltinFunction ∷ ∀ uni fun. ToBuiltinMeaning uni fun ⇒ BuiltinSemanticsVariant fun → fun → Type TyName uni () Source #
Get the type of a built-in function.
class KnownMonotype val args res where Source #
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.
knownMonotype ∷ TypeScheme val args res Source #
toMonoF ∷ ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream) → BuiltinRuntime val Source #
Convert the denotation of a builtin to its runtime counterpart .
The argument is in ReadKnownM
, because that's what deferred unlifting amounts to:
passing the action returning the builtin application around until full saturation, which is
when the action actually gets run.
Instances
(Typeable res, KnownTypeAst TyName (UniOf val) res, MakeKnown val res) ⇒ KnownMonotype val ('[] ∷ [Type]) res Source # | Once we've run out of term-level arguments, we return a
|
Defined in PlutusCore.Builtin.Meaning knownMonotype ∷ TypeScheme val '[] res Source # toMonoF ∷ ReadKnownM (FoldArgs '[] res, FoldArgs '[] ExBudgetStream) → BuiltinRuntime val Source # | |
(Typeable arg, KnownTypeAst TyName (UniOf val) arg, MakeKnown val arg, ReadKnown val arg, KnownMonotype val args res) ⇒ KnownMonotype val (arg ': args) res Source # | Every term-level argument becomes a |
Defined in PlutusCore.Builtin.Meaning knownMonotype ∷ TypeScheme val (arg ': args) res Source # toMonoF ∷ ReadKnownM (FoldArgs (arg ': args) res, FoldArgs (arg ': args) ExBudgetStream) → BuiltinRuntime val Source # |
class KnownMonotype val args res ⇒ KnownPolytype (binds ∷ [Some TyNameRep]) val args res where Source #
A class that allows us to derive a polytype for a builtin.
knownPolytype ∷ TypeScheme val args res Source #
toPolyF ∷ ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream) → BuiltinRuntime val Source #
Convert the denotation of a builtin to its runtime counterpart.
The argument is in ReadKnownM
, because that's what we need to do:
passing the action returning the builtin application around until full saturation, which is
when the action actually gets run.
Instances
KnownMonotype val args res ⇒ KnownPolytype ('[] ∷ [Some TyNameRep]) val args res Source # | Once we've run out of type-level arguments, we start handling term-level ones. |
Defined in PlutusCore.Builtin.Meaning knownPolytype ∷ TypeScheme val args res Source # toPolyF ∷ ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream) → BuiltinRuntime val Source # | |
(KnownSymbol name, KnownNat uniq, KnownKind kind, KnownPolytype binds val args res) ⇒ KnownPolytype ('Some ('TyNameRep name uniq ∷ TyNameRep kind) ': binds) val args res Source # | Every type-level argument becomes a |
Defined in PlutusCore.Builtin.Meaning knownPolytype ∷ TypeScheme val args res Source # toPolyF ∷ ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream) → BuiltinRuntime val Source # |
type family ThrowOnBothEmpty binds args isBuiltin a where ... Source #
Ensure a built-in function is not nullary and throw a nice error otherwise.
ThrowOnBothEmpty '[] '[] 'True a = TypeError (('Text "A built-in function must take at least one type or term argument" ':$$: ((('Text "\8216" ':<>: 'ShowType a) ':<>: 'Text "\8217 is a built-in type") ':<>: 'Text " so you can embed any of its values as a constant")) ':$$: 'Text "If you still want a built-in function, add a dummy \8216()\8217 argument") | |
ThrowOnBothEmpty '[] '[] 'False a = TypeError ('Text "A built-in function must take at least one type or term argument" ':$$: 'Text "To fix this error add a dummy \8216()\8217 argument") | |
ThrowOnBothEmpty _ _ _ _ = () |
class MakeBuiltinMeaning a val where Source #
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.
makeBuiltinMeaning ∷ a → (cost → FoldArgs (GetArgs a) ExBudgetStream) → BuiltinMeaning val cost Source #
Construct the meaning for a built-in function by automatically deriving its
TypeScheme
, given
- the denotation of the builtin
- an uninstantiated costing function
Instances
(uni ~ UniOf val, binds ~ ToBinds uni ('[] ∷ [Some TyNameRep]) a, args ~ GetArgs a, a ~ FoldArgs args res, ThrowOnBothEmpty binds args (IsBuiltin uni a) a, ElaborateFromTo uni 0 j val a, KnownPolytype binds val args res) ⇒ MakeBuiltinMeaning a val Source # | |
Defined in PlutusCore.Builtin.Meaning makeBuiltinMeaning ∷ a → (cost → FoldArgs (GetArgs a) ExBudgetStream) → BuiltinMeaning val cost Source # |
toBuiltinRuntime ∷ cost → BuiltinMeaning val cost → BuiltinRuntime val Source #
Convert a BuiltinMeaning
to a BuiltinRuntime
given a cost model.
toBuiltinsRuntime ∷ (cost ~ CostingPart uni fun, ToBuiltinMeaning uni fun, HasMeaningIn uni val) ⇒ BuiltinSemanticsVariant fun → cost → BuiltinsRuntime fun val Source #
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.