plutus

plutus copied to clipboard

This issue is for dumping all the plans regarding builtins in a largely unstructured way.

WARNING: this comment is horribly outdated, all the stuff has moved to different places, I'll update the comment some time later.

This comment outlines the general structure of the implementation of builtins. Copied directly from a slack discussion with minor modifications.

The builtins machinery consists of these pieces:

1. a Plutus-unspecific library for packing up types together into universes and doing stuff with them. It does not depend on anything Plutus-related, but it assumes that the user is going to need polymorphic built-in types (otherwise it would be simpler)
2. TypeScheme in plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs -- this specified the signature of a builtin. The signature can be used for getting the Plutus type of the builtin (used during type checking of Plutus programs) and it can be used for evaluation ("does a partially applied builtin expect a type or a term argument or is the builtin fully applied?")
3. KnownTypeAst in plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs -- allows you to convert a Haskell type to the corresponding Plutus one, e.g. Integer ~> con integer, EvaluationResult Bool ~> con bool (note how EvaluationResult has disappeared -- the Error effect is implicit in Plutus!). This allows us to only specify the Haskell type of a builtin and the Plutus one will be inferred automatically and used during type checking of Plutus programs
4. KnownTypeIn in plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs -- allows you to convert a Haskell value to the corresponding Plutus one and the other way around. For example, (1 :: Integer) ~> con integer 1 and EvaluationSuccess (1 :: Integer) ~> con integer 1
5. BuiltinMeaning and BuiltinRuntime in plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs -- the latter is an instantiation of the former at a concrete cost model. BuiltinRuntime consists of the TypeScheme of a built-in function, the built-in function itself and a costing function for it. We use TypeScheme to unlift arguments from terms and feed them to the builtin and also to lift the result back into a term
6. the TypeScheme inference machinery in plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs. This what allows us to only specify the Haskell definition of a builtin and get everything needed for type checking and evaluating it in Plutus. It's important to know that you don't need to understand it to tell how a builtin works: you need to understand what TypeScheme gets inferred for the builtin. This machinery merely automates creation of TypeSchemes for builtins, it does not add any other value on top. What can be inferred, can be written manually (but is quite tedious, which is how the machinery exists)
7. the default set of built-in types and relevant instances (we don't have any other set of built-in types anywhere)
8. the default set of built-in functions (we have another set of built-in types for testing purposes)

There are some helper definitions as well, but these are the main parts.

A lot of from the above has to be changed to become more efficient/expressive/etc. We'll need both major refactoring and small tweaking. This comment is about major refactorings.

• [x] TypeScheme serves both for type checking and evaluation, which means passing around evaluation-irrelevant stuff at runtime, which is silly. So we need to split TypeScheme into two parts. This is the highest priority task, because it affects performance and blocks lots of other things, some of which also affect performance. PRs: #4379, #4516
• [x] the runtime counterpart could encompass the denotation and the costing parts along with the "scheme" one. PR: #4514, #4778
• [x] the current TypeScheme is generally inefficient with all those Proxys and dictionaries inside, that needs to be fixed somehow, but a direct attempt at inlining led to nowhere. Once TypeScheme is split into two parts in a direct way, we'll need to think how to monomorphize functions stored in dictionaries. High priority, because affects performance. PRs: #4317, #4397, #4398, #4421
• [x] we need to reconsider caching the meanings of builtins. We did that once before (and once again) and it gave us horrible results, but that's because currently every built-in functions creates a thunk for every other built-in function before being executed, which is quite insane. Medium priority, because affects performance, but probably not too much (making sure stuff in plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs is compiled efficiently is high priority, because so far not much effort went into this direction, but that does not require any major refactoring, so that will be discussed in the next comment). UPD: there doesn't seem to be anyway around doing caching, it's just way too superior to trying to inline everything, especially given that caching benefits costing (see #4505) and inlining everything builtins-related would destroy that. UPD 2: in the end #4914 fully achieved what we needed
• [x] once type checking and evaluation are properly decoupled, we'll be able to implement a simpler and at the same time more expressive inference machinery. It'll have a simpler API too, here's an example diff (if everything works out like it did in https://github.com/input-output-hk/plutus/pull/4220 which however was a bad way of doing it): Low priority, because doesn't affect performance, just makes signatures of polymorphic built-in functions more readable and so also makes adding new polymorphic built-in functions easier. PR: #4312
• [ ] it's worth considering returning an iterated application from the builtins machinery rather than just term, because that should allow us to implement deep unlifting of value of recursive built-in types (like Data) while keeping recursion on the Haskell side rather than the Plutus side. I'd expect that to be a lot faster. Low priority, because affects performance, but potentially requires non-trivial research. See the branch
• [ ] Ed had this idea that we could use a data family for more compact storage of constants and I implemented that (twice) and it did seem to give an improvement, but a small one. But what if it becomes bigger if other parts of the machiinery get optimized? I looked at the core and it did look better. Low priority, because the already performed experimentation does not suggest we'll be able to get a lot out of this
• [x] currently we unlift values and feed them to builtins one by one and unlifting can fail, which makes it hard to specify how exactly builtins behave and potentially impedes performance. We need to check if that does impede performance and if we can transition to failing only when all arguments are provided (i.e. basically only during lifting). Low priority, because if we're going to change that, it'll require a brand new version of the language, so we'll have plenty of time for that change to come into effect anyway. PRs: #4430, #4510, #4514, #4516, #4879
• [x] make costing lazier to improve expressiveness: #5239

Minor things, all fairly low priority:

• [ ] play with compilation flags, in particular try setting -O2 in various places (setting it globally very unexpectedly makes things worse). PR: #4532
• [x] custom type errors. I had to drop some of them, because stupid errors. We still have quite a few, but there's room for improvement. In particular, detecting a stuck application of ToBinds or some other type family is worth exploring. Also an erroring instance for DefaultUni `Contains` TyVarRep would be very handy. PRs: #4345, #4403, #4557, #4648, #4649
• [x] when builtins are compiled, TypeSchemes are shared (which is how we got that 30% slowdown when we stopped storing meanings of builtins in an array: toBuiltinMeaning creates a ridiculous amount of irrelevant thunks just to use a few of them and throw the others away). Is it fine, can we do better? We'll need to figure out. UPD: we're doing caching and the thunks are created once per the set of builtins due to inlining (clearly visible in generated Core), so it's all fine
• [x] makeKnown and readKnown work in a constrained m. Monomorphizing those may help performance-wise. PRs: #4307, #4308, #4536
• [x] there's a ridiculous problem: the default implementation of readKnown unlifts a value of a built-in type and for that it checks that the expected type tag is equal to the actual one. However instead of taking the expected tag from the global scope, it takes it from the constraint that the default implementation has. And so an obvious optimization does not happen. PR: #4380
• [x] do we want to be able to inline toConstant/fromConstant calls for a particular term for better performance or do we want to move term out of the class head of KnownTypeIn like was done (and then reverted, because that caused a slowdown) in #4172? Is it possible to mix these two things? UPD: we gave up with the latter. PRs: #4419, #4481, #4499, #4533
• [x] when unlifting a value of a built-in type we match on Refl to obtain a proof that the value is of the expected type. Would using unsafeCoerce give us any performance boost? Apparently, not, PR: #4400
• [x] there's an enormous amount of $w$cfromInteger calls. What are those and can we get them inlined? PR: #5062
• [x] I see the following in makeKnown for Integer:

case ww4_s1bxe `cast` <Co:5> of dt_XiSB
  { DefaultUniInteger ipv_s1apx -> (ValueOf dt_XiSB vx_ikbc) `cast` <Co:14>
  })

what is this matching on DefaultUniInteger for? UPD: no longer see it. It was probably used in that last cast.

• [x] there's a TODO in the CEK machine: "We pattern match on @arg@ twice: in 'readKnown' and in 'toExMemory'. Maybe we could fuse the two?". PR: #4778
• [x] make geq reducible statically in one way or another. PRs: #4462, #4463, #5061
• [ ] consider adding Proxy to the universe, so that it's possible to provide builtins like nil (currently impossible) or pair (currently subverts the type checker). PR: #4337
• [x] split KnownTypeIn into two type classes: one for lifting and one for unlifting. This is due to the fact that we have some types values of which can be lifted but not unlifted: EvaluationResult and Emitter. SomeConstantOf was an example of the opposite, but it's gone now. PR: #4420
• [x] we need to consider dropping nullary builtins completely, so that we don't need to check if it's RuntimeSchemeResult yet every time a builtin is forced/applied. Plus it's good to reflect restrictions in the types anyway. PR: #4616 (not beneficial)
• [x] a built-in function is not supposed to fail with an exception, ever, so we need a test that for any set of built-in functions fun (properly constrained of course) checks that Arbitrary arguments don't trigger an exception. PRs: #4555, #4576
• [ ] discharging-related bookkeeping costs us some, we should try dropping discharging at least to see how much it costs us
• [x] instead of relying on the denotation application being implicitly lazy at every step we could make all builtins return a (# #) and only be lazy there. PRs: #4607, #4778
• [x] try let !cost :: (# #) -> ... in CostingFun/Core.hs so that the result of the function can be unboxed. UPD: I've tried it and nothing worked, it wouldn't unbox and it would inline instead
• [x] try to lazily lookup the builtin meanings during deserialization to avoid doing repeated lookups at runtime. Moot given #4914
• [x] looking at Core I feel like EvaluationSuccess should be made strict. PR: #4512
• [x] transformers are way too lazy for our use case, we need something stricter. PR: #4587
• [ ] try dropping extensible builtins completely to see how much they cost us
• [ ] it would be nice to have some builtins-specific benchmarks to make changes in performance more apparent
• [x] stuff that is now redundant should be dropped. PRs: #4317, #4417
• [x] better module structure. PR: #4363
• [ ] code, tests, docs polishing: #4502, #4525, #4527, #4565, #4588, #4589, #4593, #4674, #5208

The comment about major refactorings does not include two big things:

1. documenting builtins
2. collaborating with James to incorporate extensible builtins into the metatheory

It's probably too early to think about the latter right now, given how much the whole builtins machinery is going to change (if everything works out), so I'll focus on the former.

The inline docs in the source code are fairly good, they might use some polishing, but overall they seem pretty comprehensive. What is missing however is a high-level overview of the whole builtins machinery that one can read before diving into the specifics of each of its parts. We do have one such file, Builtins.md, but it was written long ago and it doesn't talk about polymorphic built-in types, builtin meaning inference etc.

Another thing we need is a doc (and presentation) on how to add a new built-in type or function. After all the recent refactorings it's completely trivial to add a new built-in type (regardless of whether it's monomorphic or polymorphic): it's basically just warnings/errors-driven copy-paste, but adding a new built-in function is trickier, because the polymorphic function over a polymorphic built-in type case is so much different to the other cases (improving upon the status quo is one of the major tasks).

PRs:

• #4338
• #4378
• #4454
• #4563
• #4605

Performance improvements in builtins-related PRs (each number is the mean performance change for validation benchmarks):

#4173: -8.23% #4230: -5.09% #4264: -2.42% #4307: -12.01% #4317: -2.01% #4379: -1.78% #4397: -2.75% #4398: -2.02% #4421: -4.87% #4481: -6.7% #4496: -2.59% #4505: -3.2% #4516: -5.88% #4587: -7.91% #4778: -4.56% #4914: -10.35% #5061: -1.16% #5239: -3.12%

Builtins-related weirdness:

1. TyVarRep exploits the very weird corner of the Haskell type system, but it's kinda already the some extension that makes it easier to support what we need
2. the Elaborate module is a big pile of weirdness, but that weirdness is all built upon a single INCOHERENT pragma (there's not even an OVERLAPPABLE one in addition to that) and people do use INCOHERENT pragmas for this kind of guessing of what an uninstantiated type variable stands for. There's was a proposal on making this an language extension, though. Having a dedicated extension certainly would make Elaborate more future-proof. Although it's not that everything will break if Elaborate stops working, we'll just need to manually instantiate all the type variables, which is some annoying boilerplate, but not the end of the world
3. in the KnownTypeAst module ToHoles is a bit weird, but that's because it's needed by the elaboration machinery
4. the functional dependencies of KnownPolytype are pretty weird: args res -> a, a -> res, but that's the usual weirdness of fundeps
5. providing Functor and other throwing instances of higher-kinded classes for Opaque is kinda weird, but last time I handled this in a more principled way, that shocked @michaelpj, so I decided not to bother given that nobody really cares anyway
6. the whole Permits -> Everywhere -> TestTypesFromTheUniverseAreAllKnown pipeline is somewhat weird, but it's a perfectly legitimate use of type families and quantified constraints

Overall, the weirdest things (1 and 2) are avoidable (at the cost of significantly more boilerplate and requiring the user to dive way deeper into how the builtins machinery works in order to define basic builtins), so the only concern is GHC people deciding to break quantified constraints, which would certainly make our lives harder (although we could switch to using the ancient tools that once served our ancestors well).

This issue is for me to track builtins-related work, I don't see what keeping it open conveys, so I'm going to close it for the sake of keeping the number of open tickets at a minimum.