Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Builtins] Make 'toBuiltinRuntime' a class method #4419

Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 2 additions & 0 deletions plutus-core/cost-model/budgeting-bench/Benchmarks/Nops.hs
Original file line number Diff line number Diff line change
Expand Up @@ -86,6 +86,8 @@ nopCostModel =
nopCostParameters :: MachineParameters CekMachineCosts CekValue DefaultUni NopFuns
nopCostParameters = toMachineParameters $ CostModel defaultCekMachineCosts nopCostModel

instance HasConstantIn DefaultUni val => ToBuiltinsRuntime NopFuns val

{- | The meanings of the builtins. Each one takes a number of integer arguments
and returns an integer without doing any other work. We could have used
units instead of integers, but using integers makes it possible to check that
Expand Down
3 changes: 2 additions & 1 deletion plutus-core/plutus-core.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -230,8 +230,9 @@ library
UntypedPlutusCore.Core.Instance.Recursive
UntypedPlutusCore.Core.Plated
UntypedPlutusCore.Evaluation.Machine.Cek.CekMachineCosts
UntypedPlutusCore.Evaluation.Machine.Cek.ExBudgetMode
UntypedPlutusCore.Evaluation.Machine.Cek.Default
UntypedPlutusCore.Evaluation.Machine.Cek.EmitterMode
UntypedPlutusCore.Evaluation.Machine.Cek.ExBudgetMode
UntypedPlutusCore.Mark
UntypedPlutusCore.Rename.Internal
UntypedPlutusCore.Simplify
Expand Down
12 changes: 10 additions & 2 deletions plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs
Original file line number Diff line number Diff line change
Expand Up @@ -127,9 +127,17 @@ instance (ToBuiltinMeaning uni fun1, ToBuiltinMeaning uni fun2) =>
toBuiltinMeaning (Right fun) = case toBuiltinMeaning fun of
BuiltinMeaning sch toF toExF -> BuiltinMeaning sch toF (toExF . snd)

instance
( HasConstantIn DefaultUni val
, ToBuiltinMeaning DefaultUni fun1
, ToBuiltinMeaning DefaultUni fun2
) => ToBuiltinsRuntime (Either fun1 fun2) val

instance HasConstantIn DefaultUni val => ToBuiltinsRuntime ExtensionFun val

defBuiltinsRuntimeExt
:: HasConstantIn DefaultUni term
=> BuiltinsRuntime (Either DefaultFun ExtensionFun) term
:: HasConstantIn DefaultUni val
=> BuiltinsRuntime (Either DefaultFun ExtensionFun) val
defBuiltinsRuntimeExt = toBuiltinsRuntime (defaultBuiltinCostModel, ())

data PlcListRep (a :: GHC.Type)
Expand Down
27 changes: 19 additions & 8 deletions plutus-core/plutus-core/src/PlutusCore/Builtin/KnownType.hs
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@ import PlutusCore.Core
import PlutusCore.Evaluation.Machine.Exception
import PlutusCore.Evaluation.Result

import Control.Lens ((#))
import Control.Lens.TH (makeClassyPrisms)
import Control.Monad.Except
import Data.Coerce
Expand Down Expand Up @@ -171,6 +172,21 @@ instance AsUnliftingError ReadKnownError where
instance AsEvaluationFailure ReadKnownError where
_EvaluationFailure = _EvaluationFailureVia ReadKnownEvaluationFailure

-- | An 'UnliftingError' for case when two type tags don't match.
typeMismatchError
:: GShow uni
=> uni (Esc a)
-> uni (Esc b)
-> UnliftingError
typeMismatchError uniExp uniAct = fromString $ concat
[ "Type mismatch: "
, "expected: " ++ gshow uniExp
, "; actual: " ++ gshow uniAct
]
-- If this function is inlined, it pollutes Core output a lot, so we mark it as non-inlineable,
-- given that we don't care about performance here, since evaluation is about to be terminated.
{-# NOINLINE typeMismatchError #-}

-- See Note [Unlifting values of built-in types].
-- | Convert a constant embedded into a PLC term to the corresponding Haskell value.
readKnownConstant
Expand All @@ -183,14 +199,9 @@ readKnownConstant mayCause val = asConstant mayCause val >>= oneShot \case
-- 'geq' matches on its first argument first, so we make the type tag that will be known
-- statically (because this function will be inlined) go first in order for GHC to optimize some of the matching away.
case uniExp `geq` uniAct of
Just Refl -> pure x
Nothing -> do
let err = fromString $ concat
[ "Type mismatch: "
, "expected: " ++ gshow uniExp
, "; actual: " ++ gshow uniAct
]
throwingWithCause _UnliftingError err mayCause
Just Refl -> Right x
Nothing -> Left $
ErrorWithCause (_UnliftingError # typeMismatchError uniExp uniAct) mayCause
{-# INLINE readKnownConstant #-}

-- See Note [Performance of KnownTypeIn instances].
Expand Down
17 changes: 13 additions & 4 deletions plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
-- GHC doesn't like the definition of 'makeBuiltinMeaning'.
{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}

{-# LANGUAGE AllowAmbiguousTypes #-}
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

do we need this?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I see, it's because we dropped the Proxy args. Does that matter? Perhaps this change should be done separately so we can see if it matters.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does that matter?

Probably not. I did it to see if it could change Core output, but couldn't tell if there was a difference in the end. I left it in the code, because AllowAmbiguousTypes looks better to my taste than those stupid proxies.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, I actually did see it affect things in one of the previous PRs. Even with INLINE pragmas everywhere, stuff still wasn't inlining properly because of that Proxy. I don't think we care about that here though, since the Core output is pretty chaotic anyway: some of TypeScheme are inlined and some are not and we're fine in both the cases, because we really only care about TypeSchemes being outside of the loop that computes BuiltinsRuntime, so that all BuiltinRuntimes are shared and never recomputed.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances #-}
Expand Down Expand Up @@ -113,6 +114,9 @@ Where all lower-case names are Haskell type variables). We'll call functions hav
The end result is that the user only has to specify the type of the denotation of a built-in
function and the 'TypeScheme' of the built-in function will be derived automatically. And in the
monomorphic and simply-polymorphic cases no types need to be specified at all.

Instances have @INLINE@ pragmas attached to methods, not sure if it helps, but it certainly
doesn't hurt.
-}

type family GetArgs a :: [GHC.Type] where
Expand All @@ -126,19 +130,22 @@ class KnownMonotype val args res a | args res -> a, a -> res where
-- | Once we've run out of term-level arguments, we return a 'TypeSchemeResult'.
instance (res ~ res', KnownType val res) => KnownMonotype val '[] res res' where
knownMonotype = TypeSchemeResult
{-# INLINE knownMonotype #-}

-- | Every term-level argument becomes as 'TypeSchemeArrow'.
instance (KnownType val arg, KnownMonotype val args res a) =>
KnownMonotype val (arg ': args) res (arg -> a) where
knownMonotype = TypeSchemeArrow knownMonotype
{-# INLINE knownMonotype #-}

-- | A class that allows us to derive a polytype for a builtin.
class KnownPolytype (binds :: [Some TyNameRep]) val args res a | args res -> a, a -> res where
knownPolytype :: Proxy binds -> TypeScheme val args res
knownPolytype :: TypeScheme val args res

-- | Once we've run out of type-level arguments, we start handling term-level ones.
instance KnownMonotype val args res a => KnownPolytype '[] val args res a where
knownPolytype _ = knownMonotype
knownPolytype = knownMonotype
{-# INLINE knownPolytype #-}

-- Here we unpack an existentially packed @kind@ and constrain it afterwards!
-- So promoted existentials are true sigmas! If we were at the term level, we'd have to pack
Expand All @@ -147,7 +154,8 @@ instance KnownMonotype val args res a => KnownPolytype '[] val args res a where
-- | Every type-level argument becomes a 'TypeSchemeAll'.
instance (KnownSymbol name, KnownNat uniq, KnownKind kind, KnownPolytype binds val args res a) =>
KnownPolytype ('Some ('TyNameRep @kind name uniq) ': binds) val args res a where
knownPolytype _ = TypeSchemeAll @name @uniq @kind Proxy $ knownPolytype (Proxy @binds)
knownPolytype = TypeSchemeAll @name @uniq @kind Proxy $ knownPolytype @binds
{-# INLINE knownPolytype #-}

-- See Note [Automatic derivation of type schemes]
-- | Construct the meaning for a built-in function by automatically deriving its
Expand All @@ -161,4 +169,5 @@ makeBuiltinMeaning
, ElaborateFromTo 0 j val a, KnownPolytype binds val args res a
)
=> a -> (cost -> FoldArgsEx args) -> BuiltinMeaning val cost
makeBuiltinMeaning = BuiltinMeaning (knownPolytype (Proxy @binds) :: TypeScheme val args res)
makeBuiltinMeaning = BuiltinMeaning $ knownPolytype @binds @val @args @res
{-# INLINE makeBuiltinMeaning #-}
47 changes: 33 additions & 14 deletions plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
Original file line number Diff line number Diff line change
@@ -1,15 +1,19 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}

{-# LANGUAGE StrictData #-}
{-# LANGUAGE StrictData #-}

module PlutusCore.Builtin.Runtime where

import PlutusPrelude

import PlutusCore.Builtin.HasConstant
import PlutusCore.Builtin.KnownType
import PlutusCore.Builtin.Meaning
import PlutusCore.Builtin.TypeScheme
import PlutusCore.Core
Expand All @@ -19,7 +23,7 @@ import Control.Lens (ix, (^?))
import Control.Monad.Except
import Data.Array
import Data.Kind qualified as GHC (Type)
import PlutusCore.Builtin.KnownType
import GHC.Exts (inline)

-- | Same as 'TypeScheme' except this one doesn't contain any evaluation-irrelevant types stuff.
data RuntimeScheme val (args :: [GHC.Type]) res where
Expand Down Expand Up @@ -66,7 +70,7 @@ newtype BuiltinsRuntime fun val = BuiltinsRuntime

-- | Convert a 'TypeScheme' to a 'RuntimeScheme'.
typeSchemeToRuntimeScheme :: TypeScheme val args res -> RuntimeScheme val args res
typeSchemeToRuntimeScheme TypeSchemeResult = RuntimeSchemeResult
typeSchemeToRuntimeScheme TypeSchemeResult = RuntimeSchemeResult
typeSchemeToRuntimeScheme (TypeSchemeArrow schB) =
RuntimeSchemeArrow $ typeSchemeToRuntimeScheme schB
typeSchemeToRuntimeScheme (TypeSchemeAll _ schK) =
Expand All @@ -77,13 +81,28 @@ toBuiltinRuntime :: cost -> BuiltinMeaning val cost -> BuiltinRuntime val
toBuiltinRuntime cost (BuiltinMeaning sch f exF) =
BuiltinRuntime (typeSchemeToRuntimeScheme sch) f (exF cost)

-- | Calculate runtime info for all built-in functions given denotations of builtins
-- and a cost model.
toBuiltinsRuntime
:: (cost ~ CostingPart uni fun, HasConstantIn uni val, ToBuiltinMeaning uni fun)
=> cost -> BuiltinsRuntime fun val
toBuiltinsRuntime cost =
BuiltinsRuntime . tabulateArray $ toBuiltinRuntime cost . toBuiltinMeaning
-- | This is a function turned into a class for the sake of specialization and inspection.
-- Every instance of this class MUST use the default implementation of 'toBuiltinsRuntime',
-- i.e. not define 'toBuiltinsRuntime' at all. Having this class allows us to inline away lots of
-- abstractions used by the builtins machinery.
--
-- For performance-critical code both @fun@ and @val@ need to be specified as concrete data types
-- for inlining to happen. In other places it's fine to only specify one of them.
class ToBuiltinsRuntime fun val where
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let me try and write down what I think this is doing.

We want to specialize toBuiltinsRuntime to specific choices of fun and val. It's not enough to inline toBuiltinsRuntime, because then we will only optimize the generic generated code at the call site, rather than generating specialized code (is this true?). Requiring a type class instance for each combination of fun and val creates a definition site which can be individually optimized, and then inlined.

That suggests the following question: does this basically amount to a SPECIALIZE pragma? Note that SPECIALIZE pragmas can be given for imported functions so long as they're INLINABLE.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm also genuinely quite unclear why inlining toBuiltinsRuntime doesn't do the job more simply.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Probably also need to inline toMachineParameters.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's not enough to inline toBuiltinsRuntime, because then we will only optimize the generic generated code at the call site, rather than generating specialized code (is this true?).

Yes, unless the call site has uni and fun specialized. If it doesn't, we'll also need to inline the call site of the call site. And so on until we reach a call site with uni and fun specialized. With the class approach we're just passing around a dictionary with specialized and optimized stuff in it and don't need to worry about chains of call sites, they can do whatever they want.

Note that we're running the CEK machine from different places, so we'd need to track all of them. How would we even do that? inspection-testing? Let's-occasionally-dump-Core-and-check-if-it's-fine-at-every-call-site?

Using a class just seems more reliable than hoping a SPECIALIZE pragma will fire or a chain of calls won't have a missing INLINE somewhere in the middle. And INLINE is sometimes not enough, an explicit call to inline is needed and all of that can change from one GHC version to another. Having a single place where we need to worry about checking if things still get optimized properly is much less of a headache.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well, except this is only for the call to toBuiltinsRuntime. Which isn't called in that many places. From a quick grep, about 2.

Note that we're running the CEK machine from different places, so we'd need to track all of them. How would we even do that?

This is why we have benchmarking, no? We've done all kinds of things that we might accidentally break.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I want to have a little try and see if I can make a version with SPECIALIZE work also, just for comparison.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd really like going in the opposite direction and testing the performance of the builtin machinery via a dedicated benchmark instead of shoving everything into a single huge run and then trying to separate actual changes from noise.

We kind of have that in the cost model benchmarks for the builtins, if you're willing to wait 12 hours or so. I'm not suggesting that seriously because (a) it takes too long, and (b) it tells us far more than we need to know. Maybe we could do something like extracting some small subset for checking the performance of the machinery though? I'm already trying to make some attempt to do that with some extra Nop benchmarks that are supposed to give some measure of the overhead of calling a builtin so that we can just model the cost of running the denotation.

I suppose that an advantage of having some separate benchmarks would be that it'd make it easier to spot regressions in the efficiency of the builtin machinery. That makes me a bit nervous because a lot of it depends on delicate implementation choices and I can imagine things going backwards if something changes in GHC.

Copy link
Contributor Author

@effectfully effectfully Mar 4, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@michaelpj

Yes, although the other way to look at that is that we shouldn't necessarily spend as much time trying to optimize the builtin machinery if the overall effect is small!

What do you consider small? Here's a breakdown of how much speedup we got from builtins-related PRs affecting performance that are already merged. A speedup of 31.22% seems to be quite a decent one. Add to that the monomorphic makeKnown PR giving us another 4.87% and the inlined toBuiltinsRuntime PR giving us another 4.03% (my version, yours is even faster), plus subsequent inlining of makeKnown like we did with readKnown, plus I also have a couple of competing branches for inlining matching on type tags. We're approaching cutting evaluation time in half by just tweaking the builtins machinery. All of that working a few hours per week (I've been also spending time on performance-irrelevant things like refactorings, improving the interface of the builtins machinery and documentation writing). I feel like this is quite a success and I should continue doing it.

@kwxm

I can imagine things going backwards if something changes in GHC.

I'm almost sure it will. Which is one of the reasons why I want the toBuiltinsRuntime-as-a-class alignment. Only one place to look it, no irrelevant things in there and the optimized version is guaranteed to be picked up unlike with INLINE or SPECIALIZE.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A speedup of 31.22% seems to be quite a decent one.

I can't of course just add up those individual changes, I'm cutting some corners here.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Add to that the monomorphic makeKnown PR giving us another 4.87% and the inlined toBuiltinsRuntime PR giving us another 4.03%

My rusty math skills suggest that with these two PRs we'll get a total of 34% speedup, which I think is not bad at all.

-- Somehow getting rid of the @uni ~ UniOf val@ constraint by substituting @UniOf val@ for @uni@
-- completely breaks inlining of 'toBuiltinMeaning'.
-- | Calculate runtime info for all built-in functions given a cost model.
toBuiltinsRuntime :: uni ~ UniOf val => CostingPart uni fun -> BuiltinsRuntime fun val
default toBuiltinsRuntime
:: (HasConstantIn uni val, ToBuiltinMeaning uni fun)
=> CostingPart uni fun -> BuiltinsRuntime fun val
-- Do we want to mark this as @INLINE@? Or @NOINLINE@? The former has the advantage of allowing
-- us to optimize some of the @cost@-related operations away at the cost of potentially blowing
-- up compilation times or even the size of the executable (probably not though). The latter is
-- the opposite. Currently we let GHC decide: it won't inline 'toBuiltinsRuntime' if it's huge.
toBuiltinsRuntime cost =
-- 'toBuiltinMeaning' can be a huge function, hence an explicit 'inline'.
BuiltinsRuntime . tabulateArray $ toBuiltinRuntime cost . inline toBuiltinMeaning

-- | Look up the runtime info of a built-in function during evaluation.
lookupBuiltin
Expand Down
37 changes: 33 additions & 4 deletions plutus-core/plutus-core/src/PlutusCore/Builtin/TypeScheme.hs
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
Expand Down Expand Up @@ -34,20 +35,48 @@ import GHC.TypeLits

infixr 9 `TypeSchemeArrow`

{- Note [KnownType in TypeSchemeArrow]
There's a @KnownType val arg@ constrained packed in the 'TypeSchemeArrow' constructor. We're not
supposed to have it there, it really should be enough to have 'KnownTypeAst', because 'readKnown'
is inlined as an explicit argument. Unfortunately, in the @Generators@ tests we use 'TypeScheme'
for generation of arbitrary arguments of builtins and that requires 'makeKnown', which makes us
have the whole 'KnownType' in 'TypeSchemeArrow', which also retains the unspecialized 'readKnown',
which pollutes Core quite a bit and in particular makes it unclear whether the whole 'HasConstant'
business is inlined away or not.

There are two things that need to be done:

1. 'KnownTypeIn' needs to be split into two classes. Unfortunately, it's not as easy as it may seem:
we did it in https://github.com/input-output-hk/plutus/pull/4420 and it introduced a 2-5%
slowdown
2. the @Generators@ tests need to do something else. Explicitly constraining @args@ outside of
'TypeScheme' sounds like a promising strategy. Maybe we could just delete those tests altogether

However it's also worth considering untangling 'RuntimeScheme' from 'TypeScheme' and generating the
two in parallel, so that we only need to optimize the former. Then we will be able to afford having
any kind of nonsense in 'TypeScheme'. Another reason for that would be the fact that Core output
has 'typeSchemeToRuntimeScheme' all over the place as it can't be inlined due to being a recursive
function, which we can't turn into an inlinable class method, because the indices of 'TypeScheme'
don't reflect its structure due to the 'TypeSchemeAll' constructor not being reflected at the type
level in any way. It's unlikely that having those 'typeSchemeToRuntimeScheme' has any impact on
performance, because they're only evaluated once during initialization, but it certainly has impact
on readability of the Core output.
-}

-- See Note [KnownType in TypeSchemeArrow].
-- | Type schemes of primitive operations.
-- @as@ is a list of types of arguments, @r@ is the resulting type.
-- @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@.
data TypeScheme val (args :: [GHC.Type]) res where
TypeSchemeResult
:: KnownType val res
=> TypeScheme val '[] res
TypeSchemeArrow
:: KnownType val arg
=> TypeScheme val args res -> TypeScheme val (arg ': args) res
=> TypeScheme val args res
-> TypeScheme val (arg ': args) res
TypeSchemeAll
:: (KnownSymbol text, KnownNat uniq, KnownKind kind)
-- Here we require the user to manually provide the unique of a type variable.
-- That's nothing but silly, but I do not see what else we can do with the current design.
=> Proxy '(text, uniq, kind)
-> TypeScheme val args res
-> TypeScheme val args res
Expand Down
10 changes: 6 additions & 4 deletions plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs
Original file line number Diff line number Diff line change
Expand Up @@ -349,14 +349,14 @@ Here's how it's defined:

I.e. @Opaque val rep@ is a wrapper around @val@, which stands for the type of value that an
evaluator uses (the builtins machinery is designed to work with any evaluator and different
evaluators define their type of values differently, for example 'CkValue' if the type of value for
evaluators define their type of values differently, for example 'CkValue' is the type of value for
the CK machine). The idea is simple: in order to apply the denotation of a builtin expecting, say,
an 'Integer' constant we need to actually extract that 'Integer' from the AST of the given value,
but if the denotation is polymorphic over the type of its argument, then we don't need to extract
anything, we can just pass the AST of the value directly to the denotation. I.e. in order for a
polymorphic function to become a monomorphic denotation (denotations are always monomorpic) all type
variables in the type of that function need to be instantiated at the type of value that a given
evaluator uses.
polymorphic function to become a monomorphic denotation (denotations are always monomorphic) all
type variables in the type of that function need to be instantiated at the type of value that a
given evaluator uses.

If we used just @val@ rathen than @Opaque val rep@, we'd specialize

Expand Down Expand Up @@ -790,6 +790,8 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
makeBuiltinMeaning
(\() -> [] @(Data,Data))
(runCostingFunOneArgument . paramMkNilPairData)
-- Keeping the unfolding, so that this function can be inlined in 'toBuiltinsRuntime'.
{-# INLINABLE toBuiltinMeaning #-}

-- It's set deliberately to give us "extra room" in the binary format to add things without running
-- out of space for tags (expanding the space would change the binary format for people who're
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ import PlutusPrelude

import PlutusCore.Builtin
import PlutusCore.Core
import PlutusCore.Default
import PlutusCore.Evaluation.Machine.Exception
import PlutusCore.Evaluation.Result
import PlutusCore.Name
Expand All @@ -43,7 +44,6 @@ import Data.DList (DList)
import Data.DList qualified as DList
import Data.STRef
import Data.Text (Text)
import Universe

infix 4 |>, <|

Expand All @@ -59,6 +59,8 @@ data CkValue uni fun =
| VBuiltin (Term TyName Name uni fun ()) (BuiltinRuntime (CkValue uni fun))
deriving (Show)

instance ToBuiltinsRuntime DefaultFun (CkValue DefaultUni DefaultFun)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't love the fact that now the functions exported from this module claim to work on any uni and fun, but you would need to add these instances to make it work in practice.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Err, it should be a general instance in the CK machine, because we don't care about performance there. I originally did experiments in this module and then forgot to fix it. I'll do that.

The CEK machine is different though, there we do need the specialization. However note that Cek.Internal is not lying: it can handle absolutely any uni and fun, because it asks the caller to provide a BuiltinsRuntime for them and doesn't need anything else. The Cek module does expose general functions while only working on DefaultUni and DefaultFun out of the box though. Maybe we need a module that only exports specialized functions, so that there's no confusion, not sure.

Copy link
Contributor Author

@effectfully effectfully Feb 27, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Err, not so fast, a general instance conflicts with the one for Either...


-- | Take pieces of a possibly partial builtin application and either create a 'CkValue' using
-- 'makeKnown' or a partial builtin application depending on whether the built-in function is
-- fully saturated or not.
Expand Down Expand Up @@ -118,8 +120,9 @@ emitCkM str = do
type instance UniOf (CkValue uni fun) = uni

instance HasConstant (CkValue uni fun) where
asConstant _ (VCon val) = pure val
asConstant mayCause _ = throwNotAConstant mayCause
asConstant mayCause = \case
VCon val -> pure val
_ -> throwNotAConstant mayCause

fromConstant = VCon

Expand Down
Loading