plutus icon indicating copy to clipboard operation
plutus copied to clipboard

Unhardcode Plutus types from signatures of builtins

Open effectfully opened this issue 1 year ago • 0 comments

(formatting was swallowed by Jira, because the shithead MBAs who all seem to be deactivated now insisted that a public project must use a private Jira board, which unexpectedly didn't work out)

Currently one can reference an arbitrary Plutus type in the type of a built-in function. It’s a direct consequence of us creating the typed language first and viewing the untyped one as “merely for evaluation”. This alignment is problematic:

Untangling untyped-plutus-core from plutus-core is difficult due to untyped-plutus-core relying on Plutus types. I’ve come with a truly ingenious way to lift this restriction in via replacing Type with DeferredType in KnownTypeAst where DeferredType is a type family that doesn’t reduce to anything in the untyped world and reduces to Type in the typed one. This way we don't need to reference any Plutus types in the majority of the builtins machinery and so can move it to untyped-plutus-core. Unfortunately concrete built-in functions still have to be defined in the typed language (or down the pipeline) where we know that DeferredType is Type.

Why do we even hardcode Plutus types in there? Maybe some other toolchain doesn’t even support all the sophistication of the Plutus type system, maybe it has a Hindley-Milner type system or something. We don’t need fancy types for builtins, so we shouldn’t hardcode them there either.

Instead of allowing arbitrary Plutus types in the type of a built-in function we can allow only a small subset of them that we actually need as is done in the metatheory. Then KnownTypeAst would return the BuiltinSig (or whatever we name it) instead of Type and convert that BuiltinSig to a Type during Plutus type checking. Easy decoupling for the win.

Ideally, we’d make BuiltinSig a type/data family, so that we could keep the existing tests with fancy types in them, as well as the generality of the language (Plutus isn’t Cardano-specific!), but it’s not too important at the moment and we can always change it in future, since it’s types stuff which doesn’t end up on the blockchain, so we can always change it later. So I think if it’s easy, we should keep the machinery general, and if it’s not, we should remove the generality and the tests.

effectfully avatar May 16 '24 13:05 effectfully