[Builtins] Restructure everything #4363
Conversation
…to effectfully/builtins/restructure-everything
| (Prelude.id :: fi ~ Opaque term (TyAppRep f Integer) => fi -> fi) | ||
| (Prelude.id :: fi ~ Opaque val (TyAppRep f Integer) => fi -> fi) |
There was a problem hiding this comment.
This is how it all started, Opaque is really supposed to be a wrapper around a value, not a general term. I was writing docs and got too disgusted of "we use term for historical reasons" (a couple of years back it did make sense), so I just went ahead and fixed it along with a bunch of other stuff.
There was a problem hiding this comment.
This is purely cosmetic though, right? We could pass terms (or anything else) to buitlins if we wanted to make PLC lazy or something, but in the current setting the things we're passing are always "values" of some sort. This is the thing I was struggling to find a word for in the specification.
There was a problem hiding this comment.
The change does make things clearer though.
There was a problem hiding this comment.
We could pass terms (or anything else) to buitlins if we wanted to make PLC lazy or something, but in the current setting the things we're passing are always "values" of some sort.
Not quite... So a couple years ago this whole machinery was expecting an evaluator to be passed along with a term to unlift from. The evaluator would turn the term into a value and then the user could perform the unlifting. Now that we don't pass any evaluators, there's no way we could turn a term into a value. Meaning if you try to unlift a 1 + 1, you don't know how to evaluate it to 2 to unlift the constant. I.e. if 1 + 1 is attempted to be unlifted, there's no way you could do that within the current machinery, irrespective of whether the language is strict or lazy. So only values can be passed to the unlifting machinery.
But it's fine to lift a constant into a term rather than a value. It's also fine to unlift from a Term as long as that term is in fact a value represented as a Term.
I.e. it's fine to implement KnownTypeIn uni val instances for vals that are general terms rather than values, but then it's your responsibility to ensure that only values represented as terms are passed into the instance, because there's no way the instance could handle a non-value.
| import PlutusCore.Constant | ||
| import PlutusCore.Builtin |
There was a problem hiding this comment.
I've renamed the Constant folder to Builtin, 'cause that makes more sense.
| toSig (acc ++ [Type $ PLC.toTypeAst $ PLC.argOf arr]) schB | ||
| toSig (acc ++ [Type $ PLC.toTypeAst $ PLC.argProxy arr]) schB |
There was a problem hiding this comment.
As per a review comment.
| module PlutusCore.Builtin.Elaborate | ||
| ( ElaborateFromTo | ||
| ) where |
There was a problem hiding this comment.
I think it's nice to have all this weirdness isolated in a dedicated file.
| runSingKind :: SingKind k -> Kind () | ||
| runSingKind SingType = Type () | ||
| runSingKind (SingKindArrow dom cod) = KindArrow () (runSingKind dom) (runSingKind cod) | ||
| demoteKind :: SingKind k -> Kind () | ||
| demoteKind SingType = Type () | ||
| demoteKind (SingKindArrow dom cod) = KindArrow () (demoteKind dom) (demoteKind cod) |
There was a problem hiding this comment.
As per a review comment.
| type KnownBuiltinTypeAst uni a = KnownTypeAst uni (ElaborateBuiltin a) | ||
|
|
||
| type KnownTypeAst :: forall a. (GHC.Type -> GHC.Type) -> a -> GHC.Constraint | ||
| class KnownTypeAst uni x where |
There was a problem hiding this comment.
Just noticed that this class is unusual in missing some haddock!
There was a problem hiding this comment.
I'll fix that separately.
| GetArgs _ = '[] | ||
|
|
||
| -- | A class that allows us to derive a monotype for a builtin. | ||
| class KnownMonotype val args res a | args res -> a, a -> res where |
There was a problem hiding this comment.
Should this and KnownPolytype be in Elaborate, since they deal with the type-scheme-guessing machinery?
There was a problem hiding this comment.
Well, it doesn't do any elaboration, it just directly reflects a Haskell type as a TypeScheme. E.g. it would make sense to have this and no elaboration at all (which is how things were aligned originally). I could create a separate module for this thing too, but it seems small and straightforward enough for it not to need a separate module.
| -- | ||
| -- The @rep@ parameter specifies how the type looks on the PLC side (i.e. just like with | ||
| -- @Opaque val rep@). | ||
| newtype SomeConstant uni (rep :: GHC.Type) = SomeConstant |
There was a problem hiding this comment.
This isn't to do with polymorphism, this is just how we represent constants. Maybe should be somewhere else?
There was a problem hiding this comment.
No, it's literally for polymorphism. Note how similar it is to Opaque. It only makes sense to use SomeConstant when you have an argument whose type has type variables in it (or an even fancier Plutus type). Check out how SomeConstant is used in the Default.Builtins and the Examples.Builtins modules.
There was a problem hiding this comment.
Ugh, I'm getting confused with ValueOf.
Co-authored-by: Michael Peyton Jones <michael.peyton-jones@iohk.io>
Co-authored-by: Michael Peyton Jones <michael.peyton-jones@iohk.io>
This one restructures the whole builtins machinery. It doesn't change any logic whatsoever, just renames a bunch of definitions and moves stuff around.