Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Avoid evaluating nilCase strictly in matchList, and rename the original matchList to matchList' #5901

Merged
merged 6 commits into from
May 9, 2024

Conversation

zliu41
Copy link
Member

@zliu41 zliu41 commented Apr 13, 2024

This shows indexing a SOP lists is slightly faster than indexing a builtin list.

@zliu41 zliu41 added the No Changelog Required Add this to skip the Changelog Check label Apr 13, 2024
@zliu41 zliu41 requested a review from a team April 13, 2024 00:39
{data}
{Unit -> Unit -> data}
xs
(\(ds : Unit) (eta : Unit) -> error {data})
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ohhhhhh...

So we clearly don't need two Unit arguments, how do we get them? Well, you wrote

    go :: BI.BuiltinList a -> Integer -> a
    go xs i =
      Builtins.matchList
        xs
        (\_ -> traceError builtinListIndexTooLargeError)
        ( \hd tl _ ->
            if i `Builtins.equalsInteger` 0
              then hd
              else go tl (Builtins.subtractInteger i 1)
        )
        ()

which makes sense, you don't want to evaluate the nil case and fail at the very first element.

But why two Units? That's because matchList has a Unit inside of it to make pattern matching on lists lazy:

matchList :: forall a r . BI.BuiltinList a -> r -> (a -> BI.BuiltinList a -> r) -> r
matchList l nilCase consCase = BI.chooseList l (const nilCase) (\_ -> consCase (BI.head l) (BI.tail l)) ()

But it doesn't make the matching actually lazy! matchList always forces nilCase, so putting () inside of matchList doesn't help with laziness as that point nilCase is already forced. So you have to do the () dance again and end up with two unit arguments, which is kinda ridiculous.

I think we should have two matchList functions instead:

matchList :: forall a r . BI.BuiltinList a -> (() -> r) -> (a -> BI.BuiltinList a -> r) -> r
matchList' :: forall a r . BI.BuiltinList a -> r -> (a -> BI.BuiltinList a -> r) -> r

one for lazy matching and one for strict matching.

And while we're here we should probably have some kind of Lazy data type instead of () ->, so that we can compile it to delay and force instead of juggling the slower units.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe this is why we got such a dramatic reduction in MEM in your earlier PR by the way? Although I just took a cursory look and was unable to spot anything.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That doesn't solve the "two unit arguments" problem, does it? You'd still end up with matchList l nilCase consCase = BI.chooseList l (const nilCase) ..., in other words BI.chooseList has to add an additional unit.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, I think it should solve the problem for the most part. You'll end up with

matchList l nilCase consCase = BI.chooseList l nilCase (const <...>) ()

Note the absence of const in the nilCase case. It'll force nilCase to WHNF, but that's a lambda and so you won't actually evaluate the result, just reach the lambda. We don't need that for consCase, since it already evaluates to a lambda, being a function.

This doesn't solve all problems, in particular if consCase is fully eta-reduced, then you'll end up evaluating both branches, but that's the usual caveat of strict languages and the answer is the usual too: don't fully eta-reduce your functions unless you actually want to evaluate the eta-reduced function.

tl;dr you'll keep the unit in the definition of matchList but won't add it to the call site of matchList.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree that matchList is silly and shouldn't be like that. I'm not sure we need two? We just need to delete the pointless units.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You are right - I removed the redundant unit and opened #5908 for further optimization.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I was looking at this and I realised the discussion here is slightly wrong. The delays in matchList are not about the nil case, they're about the cons case. In the cons case we call head and tail; we don't want to do that unless we're definitely choosing that case (they'll fail!). So we have to delay the cons case, and that means we have to delay the nil case too.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I was looking at this and I realised the discussion here is slightly wrong. The delays in matchList are not about the nil case, they're about the cons case.

The nil case is equally important, since it's an arbitrary expression and you may as well have some head in there as well. Except

In the cons case we call head and tail; we don't want to do that unless we're definitely choosing that case (they'll fail!).

in the cons case in matchList (as opposed to chooseList) we have a function, i.e. we don't call head and tail unless the function is actually called.

So it is mostly about the nil case, not the cons case in matchList. In chooseList both are equally important.

@@ -0,0 +1,18 @@
program
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

honestly, this code isn't that bad at all. well done us


compiledBuiltinListIndexing :: CompiledCode (PlutusTx.BuiltinData -> PlutusTx.BuiltinData)
compiledBuiltinListIndexing = $$(compile [||
\d -> BI.unsafeDataAsList d `List.indexBuiltinList` 5 ||])
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why are you taking a Data argument rather than a builtin list directly?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I didn't manage to lift a BuiltinList. Either the required instance is missing or I'm not doing it right.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It exists:

-- See Note [Lift and Typeable instances for builtins]
instance (FromBuiltin arep a, uni `PLC.HasTermLevel` [a]) => Lift uni (BuiltinList arep) where
    lift = liftBuiltin . fromBuiltin

but it doesn't work, because the class structure is bad. The constraints say that BuiltinData must be in the universe, which it's not, hence things don't work.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm confused. They say the type inside the list has to be in there, but here we've got a list of integers, which should be fine?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh, indeed, it's integers, not datas. I don't understand either then.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If it's BuiltinList BuiltinData:

    • No instance for ‘plutus-core-1.25.0.0:Universe.Core.Contains
                         plutus-core-1.25.0.0:PlutusCore.Default.Universe.DefaultUni
                         PlutusTx.BuiltinData’
        arising from a use of ‘liftCodeDef’
    • In the second argument of ‘unsafeApplyCode’, namely
        ‘liftCodeDef builtinListIndexingInput’

If it's BuiltinList BuiltinInteger, then even toBuiltin doesn't work:

    • No instance for ‘PlutusTx.Builtins.Class.ToBuiltin
                         [Integer] (BI.BuiltinList Integer)’
        arising from a use of ‘PlutusTx.toBuiltin’
    • In the expression: PlutusTx.toBuiltin [1 :: Integer .. 10]

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If it's BuiltinList BuiltinInteger, then even toBuiltin doesn't work:

Right, that's because the instance truly doesn't exist. I've created a ticket: #5924

Copy link
Contributor

@michaelpj michaelpj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Surprising but interesting, I guess.

@effectfully effectfully mentioned this pull request Apr 30, 2024
11 tasks
@zliu41 zliu41 removed the No Changelog Required Add this to skip the Changelog Check label May 9, 2024
@zliu41 zliu41 enabled auto-merge (squash) May 9, 2024 18:53
@zliu41 zliu41 changed the title Add budget tests for list indexing operations Avoid evaluating nilCase strictly in matchList, and rename the original matchList to matchList' May 9, 2024
@zliu41 zliu41 merged commit 253004f into master May 9, 2024
8 checks passed
@zliu41 zliu41 deleted the zliu41/index-budget branch May 9, 2024 19:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants