[Builtins] Split 'KnownTypeIn' into two classes #4420
Conversation
|
/benchmark plutus-benchmark:validation |
|
Comparing benchmark results of 'plutus-benchmark:validation' on '0397f83b8' (base) and '200e29234' (PR)
|
|
I hate you GHC. |
|
Weird. |
|
This still seems like it ought to be good in principle, maybe worth another try on top of the inlining changes? |
That's the intention. |
effectfully
force-pushed
the
effectfully/builtins/split-KnownTypeIn-into-two-classes
branch
from
200e292 to
ddb543f
Compare
|
/benchmark plutus-benchmark:validation |
|
Comparing benchmark results of 'plutus-benchmark:validation' on 'dc9275462' (base) and 'ddb543f8e' (PR)
|
|
Achievement unlocked: GHC defeated. Now need to finish it off. |
|
I mean, the PR, not GHC. |
|
Okay, so we made it not worse than the status quo... but do we expect it to actually benefit us with other changes? It seems like it should, so I'm kind of surprised it's so nothing-y. |
|
I kind of like it anyway, though, it's nice seeing where we need each direction. |
The main reason I've been bothering with this is that I want to get helpful compile-time error messages when someone uses I didn't have much hope for things to become faster, because even though |
Maybe that half a percent speedup that we see in the results above is not noise, but a true half a percent speedup due |
effectfully
force-pushed
the
effectfully/builtins/split-KnownTypeIn-into-two-classes
branch
4 times, most recently
from
1ba266d to
4f49896
Compare
| @@ -27,6 +29,8 @@ liftOrdering LT = GLT | |||
| liftOrdering EQ = error "'liftOrdering': 'Eq'" | |||
| liftOrdering GT = GGT | |||
|
|
|||
| type KnownType val a = (KnownTypeAst (UniOf val) a, MakeKnown val a) | |||
There was a problem hiding this comment.
Naming here doesn't make much sense, but I really don't want to spend a lot of time here refactoring these tests, at the very least not in this PR.
| {-# LANGUAGE UndecidableInstances #-} | ||
| {-# LANGUAGE UndecidableSuperClasses #-} | ||
|
|
||
| module PlutusCore.Builtin.TestKnown |
There was a problem hiding this comment.
Created a separate file just not to keep this scary looking stuff in the important KnownType module and in order not to introduce a dependency on KnownTypeAst in it, as the two concepts are explicitly orthogonal (described in a Note).
There was a problem hiding this comment.
Why not put this rationale in the module comment?
| -- | An instance of this class not having any constraints ensures that every type (according to | ||
| -- 'Everywhere') from the universe has 'KnownTypeAst, 'ReadKnownIn' and 'MakeKnownIn' instances. | ||
| class | ||
| ( uni `Everywhere` ImplementedKnownTypeAst uni |
There was a problem hiding this comment.
We didn't have that ImplementedKnownTypeAst test before, now we do.
|
Code polished, old docs polished, new docs added, ready for review. |
| -} | ||
|
|
||
| -- See Note [Performance of ReadKnownIn and MakeKnownIn instances]. | ||
| class uni ~ UniOf val => MakeKnownIn uni val a where |
There was a problem hiding this comment.
No instances of these typeclasses ever fix val. What would happen if we did this?
class MakeKnownIn uni a where
makeKnown :: forall val . (uni ~ UniOf val) => ...
I think so long as makeKnown gets inlined this is going to be no worse and it lets us get rid of a typeclass parameter.
There was a problem hiding this comment.
Okay, you'd need to add a uni ~ UniOf val constraint in a few places (e.g. kin the definition of MakeKnown), but that seems okay.
There was a problem hiding this comment.
I guess you're not gaining that much, it just seems somewhat interesting to me that really these instances only care about the universe, and you can use the same instance for whatever val you like, so long as it has that universe.
There was a problem hiding this comment.
Nope, I did miss something: the default implementation ultimately relies on HasConstantIn which does need to fix the term type. So you can't do the default instances without this. Leaving my comments just in case they're interesting anyway 🤷
There was a problem hiding this comment.
I've been annoyed by this problem for years by now. Which is how #4172 emerged. It fixed the problem, but made the code slower and we reverted it. I'd been looking at it again today before I read your comments! I'm going to try it again now that we have a good inlining setup.
There was a problem hiding this comment.
No instances of these typeclasses ever fix
val
The Opaque instance does.
There was a problem hiding this comment.
Interesting. We weren't even inlining makeKnown/readKnown at that point, so perhaps it's less surprising that the dictionary-passing overhead didn't get optimized away.
| {-# LANGUAGE UndecidableInstances #-} | ||
| {-# LANGUAGE UndecidableSuperClasses #-} | ||
|
|
||
| module PlutusCore.Builtin.TestKnown |
There was a problem hiding this comment.
Why not put this rationale in the module comment?
|
|
||
| However it's also worth considering untangling 'RuntimeScheme' from 'TypeScheme' and generating the | ||
| two in parallel, so that we only need to optimize the former. Then we will be able to afford having | ||
| any kind of nonsense in 'TypeScheme'. Another reason for that would be the fact that Core output |
There was a problem hiding this comment.
Yeah, this seems reasonable. It doesn't seem crazy that a value representing a type signature for a function should allow you to both lift and unlift the argument types. It's just that we don't need that at runtime, and that's what we have RuntimeScheme for.
There was a problem hiding this comment.
Not sure what you're saying. That what we have right now is already fine, given that MakeKnown only appears for arguments in TypeScheme and not RuntimeScheme?
There was a problem hiding this comment.
Yes, which I think is also what you were saying in the comment: that it seems conceptually fine, so long as it doesn't leak into the implementation of the RuntimeSchemes.
effectfully
force-pushed
the
effectfully/builtins/split-KnownTypeIn-into-two-classes
branch
from
4f49896 to
f891cc6
Compare
effectfully
deleted the
effectfully/builtins/split-KnownTypeIn-into-two-classes
branch
Don't look here yet.