Builtins about plutus HOT 13 CLOSED

On static/dynamic builtins: IMO it would be nice if there were eventually only one class of builtin, i.e. our current "static" builtins were just turned into dynamic builtins. Dynamic ones seem strictly more powerful, so removing the weaker version in favour of that seems good. This also solves the naming issues since we only have one thing! (Although they're no longer "builtin", really...)

For people following along: here's how I've been thinking about the "turn PLC terms into Haskell values" problem.

• We want to use our usual evaluator to do this - that's the sensible way to do something to a PLC term.
• But we have no way of representing the result of this computation, since the evaluators just work with PLC terms.
• However, if we have dynamic builtin types, then we naturally have (con a) for any a that's of a dynamic builtin type.
• So we can stuff Haskell values into these constant and use dynamic builtins to manipulate them.
• A simple version of this is using the dynamic builtin strings to fold a PLC term into a string - but if it's of a type compiled from a Haskell type, then we should also be able to fold it into a Haskell value of that Haskell type!
• We would need the ability to create such a fold generically, but this is probably a similar exercise in generic programming to the ones we've already done for lifting etc.

from plutus.

I can add support for sum and product types (without unsafePerformIO nonsense)

Nah, probably still requires unsafePerformIO.

On static/dynamic builtins: IMO it would be nice if there were eventually only one class of builtin, i.e. our current "static" builtins were just turned into dynamic builtins. Dynamic ones seem strictly more powerful, so removing the weaker version in favour of that seems good.

I was previously opposed to that, but now I think you're right. I've just written the following comment in TypeSynthesis.hs:

-- We have a weird corner case here: the type of a 'BuiltinName' can contain 'TypedBuiltinDyn', i.e.
-- a static built-in name is allowed to depend on a dynamic built-in type which are not required
-- to be normalized. For dynamic built-in names we store a map from them to their *normalized types*,
-- with the normalization happening in this module, but what should we do for static built-in names?
-- Right now we just renormalize the type of a static built-in name each time we encounter that name.

If we are going to use dynamic builtins extensively (which is the case, right?), then there is no point in having more corner cases. But if we're going to use dynamic builtin names only for some hacks, then it makes sense to distinguish between hacks and the blessed approach.

We want to use our usual evaluator to do this - that's the sensible way to do something to a PLC term.

One alternative is to analyze the PLC AST directly, but it's a nightmare. The motivation for using evaluators is elaborated in Language.PlutusCore.Constant.Typed as well.

But we have no way of representing the result of this computation, since the evaluators just work with PLC terms.

You once said this:

perhaps the problem is that our evaluators expect to always produce a PLC term? Perhaps we should have a different notion of value for the result of execution that could include the output of dynamic builtins.

It can be indeed the case that extending the result of evaluation is something that we actually need rather than embedding the entire Haskell into Plutus Core. I'll play with that.

from plutus.

Meanwhile, @j-mueller, right now we can convert PLC lists to Haskell lists (and hence lists of lists, lists of lists of lists, etc). I think, I can add support for sum and product types (without unsafePerformIO nonsense). This does not allow to convert an arbitrary PLC to value to a Haskell value, but maybe it's enough to unblock you at least?

Yeah product types and lists should be enough, but I just didn't want to write the contracts on the assumption that we would be able to do this - now that I know this feature is planned I'm not blocked on it, I can mimick it easily for testing purposes.

from plutus.

Yeah product types and lists should be enough

Ok, I'll add them then.

but I just didn't want to write the contracts on the assumption that we would be able to do this - now that I know this feature is planned I'm not blocked on it

Makes perfect sense, but note that even though the feature is planned, it's not clear whether it's possible to implement it in a sensible way. This all is a bit hand-wavy right now.

I can mimick it easily for testing purposes.

Great.

from plutus.

Added support for throwing a PLC error from a builtin name in #642 (not merged yet).

We need to do a few things (better before experimenting with parameterizing Term by additional type variables):

1. Allow parametric polymorphism in TypeScheme
2. Rename KnownDynamicBuiltinType to KnownType and reflect all the types via this type class, including "static" ones. I've recently (in #642) removed TypedBuiltinBool as a special case and realized that we can remove all special cases, even integers and bytestrings, like that. This is needed, because right now we can throw an error from a builtin name that normally returns an Bool, but not from one that returns an Integer, which is a silly limitation. The challenge however is in handling sizes, which I don't know how to approach at the moment.
3. A funny thought: we do not really need to change the AST in order to be able to embed arbitrary Haskell into Plutus Core. We can just carry an environment of Haskell values together with a Plutus Core term which references values in the environment by their indices (say, in the Var constructor, but it's better to have a separate MetaVar constructor for this). At the very least this should allow us to play with the ideas without needing to fix 10000 errors that adding additional parameters to Term would cause.

from plutus.

We can just carry an environment of Haskell values together with a Plutus Core term which references values in the environment by their indices (say, in the Var constructor, but it's better to have a separate MetaVar constructor for this)

Interesting! My only question is how we would type a PLC term with these in it? I guess providing a type-environment at typechecking type and a term-environment at runtime is actually very similar to what we do for the current dynamic builtins.

from plutus.

Interesting! My only question is how we would type a PLC term with these in it? I guess providing a type-environment at typechecking type and a term-environment at runtime is actually very similar to what we do for the current dynamic builtins.

Yes. Except right now we look up only dynamic builtin names and there is a finite amount of them, while with the new approach we can extend environments indefinitely. "Got a Haskell value that you can't embed into PLC? Put it into the current environment and reference it by its index". But this sounds like it may require a GC with reference counting or something.

from plutus.

Plus everything is done with unconstrained indices, which is unpleasant.

from plutus.

Yes. But it's very good for experimenting at least and maybe as a temporary intermediate solution.

from plutus.

This comment's an offshoot from the now-closed "Do we have keywords?" issue: #463

The PLC parser currently has special treatment for builtin names, so they really are built in. This'll have to change once we have extensible builtins: we'll have to look up names in a table or something to make sure they really exist. Fortunately you now have to say builtin every time you mention a built in name, so there's no ambiguity about what's what.

We'll also have to change the spec, but let's cross that bridge when we come to it.

from plutus.

This'll have to change once we have extensible builtins: we'll have to look up names in a table or something to make sure they really exist.

We already have extensible builtins in this sense. Here is an excerpt from the classic pretty-printer:

instance PrettyBy (PrettyConfigClassic configName) (Builtin a) where
    prettyBy _ (BuiltinName    _ n) = pretty n
    prettyBy _ (DynBuiltinName _ n) = pretty n
...
instance (PrettyClassicBy configName (tyname a), PrettyClassicBy configName (name a)) =>
        PrettyBy (PrettyConfigClassic configName) (Term tyname name a) where
    prettyBy config = cata a where
        a (BuiltinF _ bi)      = parens' ("builtin" </> prettyBy config bi)

I don't think we've ever tested how this interacts with the parser. For example in Language.PlutusCore.Generators.AST we have

genBuiltin :: MonadGen m => m (Builtin ())
genBuiltin = BuiltinName () <$> genBuiltinName

i.e. we basically never generate a DynBuiltinName.

we'll have to look up names in a table

I'd start with "if it's marked as a builtin, but it's not a static builtiln, then it's an extensible one". Passing tables around is a good solution, but we're going to change the related interface to builtins, so I'd do the simplest thing and leave the better approach for future.

If you wish, you can add some tests related to extensible builtins and add support for extensible builtlins to the parser.

from plutus.

Right, we haven't added anything about extensible builtins to the parser or spec, they're basically only available if you're constructing an AST directly.

from plutus.

We need to do a few things (better before experimenting with parameterizing Term by additional type variables):

1. Allow parametric polymorphism in TypeScheme

Done in #751.

2. Rename KnownDynamicBuiltinType to KnownType and reflect all the types via this type class, including "static" ones. I've recently (in #642) removed TypedBuiltinBool as a special case and realized that we can remove all special cases, even integers and bytestrings, like that. This is needed, because right now we can throw an error from a builtin name that normally returns an Bool, but not from one that returns an Integer, which is a silly limitation. The challenge however is in handling sizes, which I don't know how to approach at the moment.

Doing that in #983. Now that we don't have sizes, everything is straightforward.

from plutus.