[Builtins] Add 'Proxy' to the default universe

[effectfully]

This shows how to add Proxy to the default universe, so that we can have only only one built-in MkNil and express the two that we currently have in terms of it.

This is unpolished, 'cause I'm not sure if we want this or not, I just thought it would be easy to implement it, so I did that.

[michaelpj]

This would need Plutus V2, FWIW.

This all makes sense from an engineering perspective, I think my reservation with this stuff is it feels like there's a theoretical hole we haven't quite filled about how polymorphic builtin types can only be instantiated at builtin types, and how we reconcile that with the typesystem that we have...

[effectfully]

This would need Plutus V2, FWIW.

Why? It's just a new built-in type and a new built-in function. We don't need to drop the old MkNilData and MkNilPairData, they can stay, even though this PR renders them obsolete.

I think my reservation with this stuff is it feels like there's a theoretical hole we haven't quite filled about how polymorphic builtin types can only be instantiated at builtin types, and how we reconcile that with the typesystem that we have...

Where do you see a hole?

1. the builtins machinery is very general, it allows us to easily implement things like unsafeCoerce. We could try thinking about reducing the expressiveness of the builtins machinery to the point where every definable builtin fits well into the type system of Plutus by definition, but... why? That will just tie our hands and complicate the already non-trivial machinery. I think it's enough for introduced builtins to have sensible semantics, we don't need to worry about ruling out the possibility of defining bogus builtins
2. this PR precisely allows us to constrain types to be built-ins. proxy a (where proxy is the built-in Proxy type) on the Plutus side is a proof that a is a built-in type. Yes, you can instantiate a at a non-built-in type in Plutus, but that has a perfectly well-defined semantics: it creates an empty type, i.e. an equivalent of Void and turns the builtin into absurd. We've talked about that in the docs

[michaelpj]

We don't need to drop the old MkNilData and MkNilPairData, they can stay, even though this PR renders them obsolete.

Ah, I was assuming we'd drop them. Yes, that's true.

We could try thinking about reducing the expressiveness of the builtins machinery to the point where every definable builtin fits well into the type system of Plutus by definition, but... why?

We need to be able to specify it is why! Kenneth is already having a lot of difficulty specifying the current version, and I think that's without allowing for the possibility of something like unsafeCoerce. So I think we should be careful in letting the implementation drive too much.

this PR precisely allows us to constrain types to be built-ins. proxy a (where proxy is the built-in Proxy type) on the Plutus side is a proof that a is a built-in type.

Hmmm.... And how do you get such a thing? I think the answer is: only by making it as a literal constant. There's something a bit funny here: we could do that today to get rid of the various MkNil builtins: just make constants instead of using builtin functions! I guess this isn't true in all cases, though...

[effectfully]

We need to be able to specify it is why! Kenneth is already having a lot of difficulty specifying the current version, and I think that's without allowing for the possibility of something like unsafeCoerce. So I think we should be careful in letting the implementation drive too much.

These are good intentions, but polymorphic built-in types don't come for free. Without them we could have a builtins machinery that is inline with the rest of the type system of Plutus, but with them things get trickier. It's similar to how we could've avoided the entire extensible built-in types machinery if we were to hardcode an inlined version of Some (ValueOf DefaultUni) and if it didn't have polymorphic built-in types in it. But with them I don't see a way of avoiding dealing with universes. Not sure if I wrote a Note about that. If not, I'll do it at some point.

How would you allow something like a built-in cons : all a. a -> [a] -> [a] while disallowing bogus builtins at the same time? Types are gone at runtime, we have to actually check type tags for equality, boom, bye-bye parametricity in the general case.

I think the answer is: only by making it as a literal constant.

If we're able to compile lists and operations over them, there shouldn't be any trouble compiling Proxy in a similar way, right? Plus you could probably define a special type class in Plutus Tx having instances for Bool, Integer, [a] etc.

[kwxm]

This all seems to make sense, but I wonder if we really need it yet. It's annoying that we're stuck with mkNilData and mkNilPairData forever and we can't just use mkNil instead. I'd be inclined to put this on ice until we actually need it, if we decide we do at some point.

[Edit: see a later comment where I realise that most of this is rubbish.]
What kind of things do you see us using the Proxy type for in practice? I'm wondering if we can get away without needing it at all. To use mkNil to create an empty list of integers, we first have to instantiate it at type integer, and then we have to apply it to a constant of type proxy(integer) (I even managed to do this successfully after a bit of fiddling with the parser). Could we instead have a polymorphic nullary mkNil builtin that we just instantiate to get an empty list immediately without needing Proxy types and values to be visible in PLC at all? It may be that this approach doesn't give us the flexibility that Proxy does, so I'm wondering what a plausible use case for the full Proxy machinery might be.

I have a vague idea that there might have been some objection to having nullary builtins, although I don't immediately see what the problem would be. Maybe that would torpedo the suggestion above. [Later: I see a comment near the definition of mkNilData saying "nullary builtins don't work", but it doesn't say why. Is that a fundamental restriction? Even if it is, could we define a mkNil of type [forall a, unit] -> list(a)?]

I also haven't thought through how to specify the semantics of all this yet. I think nullary builtins would be OK, but I'm not so sure about Proxy, although that might still fit into the present framework.

[kwxm]

Strictly this would need its own cost model parameters instead of re-using the ones for mkNilData, and that would require us to add new benchmarks for mkNil. However, I'm pretty certain that that would make no difference at all since this is doing almost no work.

[kwxm]

Could we express the meanings of mkNilData and mkNilPairData directly in terms of mkNil? Maybe then we'd just need one benchmark for all three functions.

[effectfully]

Strictly this would need its own cost model parameters instead of re-using the ones for mkNilData, and that would require us to add new benchmarks for mkNil

Yes, I'm just being sloppy here.

Could we express the meanings of mkNilData and mkNilPairData directly in terms of mkNil?

Probably not. They are very similar, but not to the point of the first two being an instance of the last one.

[kwxm]

This would be easy to do, wouldn't it? It'd just be checking whether or not a string was "proxy" (or "Proxy" or whatever).

[effectfully]

Yup, just being sloppy.

[kwxm]

Do you need some code for parsing proxy just below as well? (Also, do we really want what the Parsable instance is doing for the pair and list types, or is that code not supposed to be used?)

[effectfully]

Yep.

(Also, do we really want what the Parsable instance is doing for the pair and list types, or is that code not supposed to be used?)

I don't really know, that's up to @thealmarty.

[thealmarty]

The Parsable instance will be gone in the new parsers. The new parsers won't be dealing with data structures yet. It'll be in another PR. We can think about what we want then.

[kwxm]

I now realise that much of what I wrote earlier was nonsense. My thinking was that many of the things one would once have used Proxy for in Haskell can now be done with type applications (or at least that's the impression I get), and since we have explicit type instantiation in PLC we could just use that instead. But of course we don't have that in UPLC, we just have force, which knows nothing about types! The only place we can mention types in a UPLC program is inside a con, so without major changes the best we can do is to have a polymorphic constant value that carries type information about, and that's exactly what Proxy does. So now I'm persuaded that this seems the only sensible way to proceed if we want to allow things like mkNil which are effectively zero-argument polymorphic builtins.

I was a bit worried that adding this to the specification would need some kind of special case, but now I think that it would fit into the existing framework without having to modify anything. I'd still be inclined to keep it in reserve, to be rolled out if at some point we decide to add some new polymorphic built-in type that needs the functionality.

[michaelpj]

In the builtins-specification that's brewing in my head (it would have to be for V2), I think there's a nice way to incorporate this without including it in the UPLC specification: proxy is just a normal builtin as far as UPLC is concerned, but when we describe the elaboration from TPLC to UPLC we say that we can only do it if certain builtins are present in the target language, namely proxy!

[effectfully]

The only place we can mention types in a UPLC program is inside a con, so without major changes the best we can do is to have a polymorphic constant value that carries type information about, and that's exactly what Proxy does.

Yes, exactly.

I was a bit worried that adding this to the specification would need some kind of special case, but now I think that it would fit into the existing framework without having to modify anything.

I believe so, yes. It's just another polymorphic built-in type, nothing more fancy than the type of lists. It is not handled in any special case.

[effectfully]

Let's close this one for now and reopen when we need it.