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.

Sign up for GitHub

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

Jump to bottom

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

Merged
merged 6 commits into from
May 9, 2024
Merged

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

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
057c38c
Add budget tests for list indexing operations
zliu41 Apr 13, 2024
f823fce
Merge branch 'master' of github.com:IntersectMBO/plutus into zliu41/i…
zliu41 Apr 16, 2024
172d0e4
Address comments
zliu41 Apr 16, 2024
aa1c375
Merge branch 'master' of github.com:IntersectMBO/plutus into zliu41/i…
zliu41 May 8, 2024
3386f7e
fix build
zliu41 May 9, 2024
8f8f4b8
add changelog
zliu41 May 9, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions plutus-tx-plugin/test/Budget/9.6/builtinListIndexing.budget.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
({cpu: 12203376
| mem: 34830})
1 change: 1 addition & 0 deletions plutus-tx-plugin/test/Budget/9.6/builtinListIndexing.eval.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
(con data (I 6))
32 changes: 32 additions & 0 deletions plutus-tx-plugin/test/Budget/9.6/builtinListIndexing.pir.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
let
data Unit | Unit_match where
Unit : Unit
in
letrec
!go : list data -> integer -> data
= \(xs : list data) (i : integer) ->
chooseList
{data}
{Unit -> Unit -> data}
xs
(\(ds : Unit) (eta : Unit) -> error {data})
Copy link
Contributor

@effectfully effectfully Apr 13, 2024 •
edited
Loading

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.

(\(ds : Unit) (ds : Unit) ->
let
!hd : data = headList {data} xs
!tl : list data = tailList {data} xs
in
ifThenElse
{all dead. data}
(equalsInteger 0 i)
(/\dead -> hd)
(/\dead -> go tl (subtractInteger i 1))
{all dead. dead})
Unit
Unit
in
let
data Bool | Bool_match where
True : Bool
False : Bool
in
\(d : data) -> let !xs : list data = unListData d in go xs 5
22 changes: 22 additions & 0 deletions plutus-tx-plugin/test/Budget/9.6/builtinListIndexing.uplc.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
program
1.1.0
((\go d -> go (unListData d) 5)
((\s -> s s)
(\s x ->
(\go i ->
force (force chooseList)
x
(\ds eta -> error)
(\ds ds ->
(\hd ->
(\tl ->
force
(force ifThenElse
(equalsInteger 0 i)
(delay hd)
(delay (go tl (subtractInteger i 1)))))
(force tailList x))
(force headList x))
(constr 0 [])
(constr 0 []))
(s s))))
2 changes: 2 additions & 0 deletions plutus-tx-plugin/test/Budget/9.6/listIndexing.budget.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
({cpu: 10405419
| mem: 33322})
1 change: 1 addition & 0 deletions plutus-tx-plugin/test/Budget/9.6/listIndexing.eval.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
(con data (I 6))
31 changes: 31 additions & 0 deletions plutus-tx-plugin/test/Budget/9.6/listIndexing.pir.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
letrec
data (List :: * -> *) a | List_match where
Nil : List a
Cons : a -> List a -> List a
in
letrec
!go : integer -> List data -> data
= \(ds : integer) (ds : List data) ->
List_match
{data}
ds
{all dead. data}
(/\dead -> error {data})
(\(x : data) (xs : List data) ->
/\dead ->
ifThenElse
{all dead. data}
(equalsInteger 0 ds)
(/\dead -> x)
(/\dead -> go (subtractInteger ds 1) xs)
{all dead. dead})
{all dead. dead}
in
let
data Bool | Bool_match where
True : Bool
False : Bool
data Unit | Unit_match where
Unit : Unit
in
\(xs : List data) -> go 5 xs
18 changes: 18 additions & 0 deletions plutus-tx-plugin/test/Budget/9.6/listIndexing.uplc.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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

1.1.0
((\go xs -> go 5 xs)
((\s -> s s)
(\s x ->
(\go ds ->
force
(case
ds
[ (delay error)
, (\x xs ->
delay
(force
(force ifThenElse
(equalsInteger 0 x)
(delay x)
(delay (go (subtractInteger x 1) xs))))) ]))
(s s))))
33 changes: 33 additions & 0 deletions plutus-tx-plugin/test/Budget/Spec.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ import Budget.WithGHCOptimisations qualified as WithGHCOptTest
import Budget.WithoutGHCOptimisations qualified as WithoutGHCOptTest
import PlutusTx.AsData qualified as AsData
import PlutusTx.Builtins qualified as PlutusTx
import PlutusTx.Builtins.Internal qualified as BI
import PlutusTx.Code
import PlutusTx.IsData qualified as IsData
import PlutusTx.Lift (liftCodeDef, makeLift)
Expand Down Expand Up @@ -201,6 +202,24 @@ tests = testNestedGhc "Budget" [
, goldenPirReadable "null" compiledNull
, goldenEvalCekCatch "null" [compiledNull]

, goldenUPlcReadable "listIndexing" compiledListIndexing
, goldenPirReadable "listIndexing" compiledListIndexing
, goldenEvalCekCatch
"listIndexing"
[compiledListIndexing `unsafeApplyCode` liftCodeDef listIndexingInput]
, goldenBudget
"listIndexing"
(compiledListIndexing `unsafeApplyCode` liftCodeDef listIndexingInput)

, goldenUPlcReadable "builtinListIndexing" compiledBuiltinListIndexing
, goldenPirReadable "builtinListIndexing" compiledBuiltinListIndexing
, goldenEvalCekCatch
"builtinListIndexing"
[compiledBuiltinListIndexing `unsafeApplyCode` liftCodeDef builtinListIndexingInput]
, goldenBudget
"builtinListIndexing"
(compiledBuiltinListIndexing `unsafeApplyCode` liftCodeDef builtinListIndexingInput)

, goldenBudget "toFromData" compiledToFromData
, goldenUPlcReadable "toFromData" compiledToFromData
, goldenPirReadable "toFromData" compiledToFromData
Expand Down Expand Up @@ -461,6 +480,20 @@ compiledNull = $$(compile [||
let ls = [1,2,3,4,5,6,7,8,9,10] :: [Integer]
in PlutusTx.null ls ||])

compiledListIndexing :: CompiledCode ([PlutusTx.BuiltinData] -> PlutusTx.BuiltinData)
compiledListIndexing = $$(compile [||
\xs -> xs List.!! 5 ||])

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


listIndexingInput :: [PlutusTx.BuiltinData]
listIndexingInput = IsData.toBuiltinData <$> [1 :: Integer .. 10]

builtinListIndexingInput :: PlutusTx.BuiltinData
builtinListIndexingInput = IsData.toBuiltinData listIndexingInput

compiledToFromData :: CompiledCode (Either Integer (Maybe (Bool, Integer, Bool)))
compiledToFromData = $$(compile [||
let
Expand Down