From 16be7da33eacb1991ae0164b9fd65e12c7e4771e Mon Sep 17 00:00:00 2001 From: effectfully Date: Tue, 7 May 2024 00:23:26 +0200 Subject: [PATCH] [PIR] Don't generate 'fixBy' if you don't need to (#5954) Removes unnecessary generation of `fixBy` when we only need `fix`. --- .../stdlib/PlutusCore/StdLib/Data/Function.hs | 48 ++- .../src/PlutusIR/Compiler/Recursion.hs | 11 +- .../Compiler/Recursion/factorial.golden | 18 +- .../StrictLetRec/strictLetRec.golden | 391 +++++------------- .../PlutusCore/Generators/QuickCheck/GenTm.hs | 2 +- 5 files changed, 171 insertions(+), 299 deletions(-) diff --git a/plutus-core/plutus-core/stdlib/PlutusCore/StdLib/Data/Function.hs b/plutus-core/plutus-core/stdlib/PlutusCore/StdLib/Data/Function.hs index 268332c7519..4bce9452545 100644 --- a/plutus-core/plutus-core/stdlib/PlutusCore/StdLib/Data/Function.hs +++ b/plutus-core/plutus-core/stdlib/PlutusCore/StdLib/Data/Function.hs @@ -79,6 +79,51 @@ applyFun = runQuote $ do . lamAbs () x (TyVar () a) $ apply () (var () f) (var () x) +{- Note [Recursion combinators] +We create singly recursive and mutually recursive functions using different combinators. + +For singly recursive functions we use the Z combinator (a strict cousin of the Y combinator) that in +UPLC looks like this: + + \f -> (\s -> s s) (\s -> f (\x -> s s x)) + +We have benchmarked its Haskell version at + https://github.com/IntersectMBO/plutus/tree/9538fc9829426b2ecb0628d352e2d7af96ec8204/doc/notes/fomega/z-combinator-benchmarks +and observed that in Haskell there's no detectable difference in performance of functions defined +using explicit recursion versus the Z combinator. However Haskell is a compiled language and Plutus +is interpreted, so it's very likely that natively supporting recursion in Plutus instead of +compiling recursive functions to combinators would significantly boost performance. + +We've tried using + + \f -> (\s -> s s) (\s x -> f (s s) x) + +instead of + + \f -> (\s -> s s) (\s -> f (\x -> s s x)) + +and while it worked OK at the PLC level, it wasn't a suitable primitive for compilation of recursive +functions, because it would add laziness in unexpected places, see + https://github.com/IntersectMBO/plutus/issues/5961 +so we had to change it. + +We use + + \f -> (\s -> s s) (\s x -> f (s s) x) + +instead of the more standard + + \f -> (\s x -> f (s s) x) (\s x -> f (s s) x) + +because in practice @f@ gets inlined and we wouldn't be able to do so if it occurred twice in the +term. Plus the former also allows us to save on the size of the term. + +For mutually recursive functions we use the 'fixBy' combinator, which is, to the best of our +knowledge, our own invention. It was first described at + https://github.com/IntersectMBO/plutus/blob/067e74f0606fddc5e183dd45209b461e293a6224/doc/notes/fomega/mutual-term-level-recursion/FixN.agda +and fully specified in our "Unraveling recursion: compiling an IR with recursion to System F" paper. +-} + -- | @Self@ as a PLC type. -- -- > fix \(self :: * -> *) (a :: *) -> self a -> a @@ -144,7 +189,6 @@ fixAndType = runQuote $ do $ TyFun () (TyFun () funAB funAB) funAB pure (fixTerm, fixType) - -- | A type that looks like a transformation. -- -- > trans F G Q : F Q -> G Q @@ -337,6 +381,7 @@ fixNAndType n fixByTerm = runQuote $ do ] pure (fixNTerm, fixNType) +-- See Note [Recursion combinators]. -- | Get the fixed-point of a single recursive function. getSingleFixOf :: (TermLike term TyName Name uni fun) @@ -346,6 +391,7 @@ getSingleFixOf ann fix1 fun@FunctionDef{_functionDefType=(FunctionType _ dom cod abstractedBody = mkIterLamAbs [functionDefVarDecl fun] $ _functionDefTerm fun in apply ann instantiatedFix abstractedBody +-- See Note [Recursion combinators]. -- | Get the fixed-point of a list of mutually recursive functions. -- -- > MutualFixOf _ fixN [ FunctionDef _ fN1 (FunctionType _ a1 b1) f1 diff --git a/plutus-core/plutus-ir/src/PlutusIR/Compiler/Recursion.hs b/plutus-core/plutus-ir/src/PlutusIR/Compiler/Recursion.hs index 4787ceec8cc..a3fc4481208 100644 --- a/plutus-core/plutus-ir/src/PlutusIR/Compiler/Recursion.hs +++ b/plutus-core/plutus-ir/src/PlutusIR/Compiler/Recursion.hs @@ -98,15 +98,16 @@ mkFixpoint bs = do name <- liftQuote $ toProgramName fixByKey let (fixByTerm, fixByType) = Function.fixByAndType pure (PLC.Def (PLC.VarDecl noProvenance name (noProvenance <$ fixByType)) (noProvenance <$ fixByTerm, Strict), mempty) - fixBy <- lookupOrDefineTerm p0 fixByKey mkFixByDef let mkFixNDef = do name <- liftQuote $ toProgramName fixNKey - let ((fixNTerm, fixNType), fixNDeps) = - if arity == 1 - then (Function.fixAndType, mempty) + ((fixNTerm, fixNType), fixNDeps) <- + if arity == 1 + then pure (Function.fixAndType, mempty) -- fixN depends on fixBy - else (Function.fixNAndType arity (void fixBy), Set.singleton fixByKey) + else do + fixBy <- lookupOrDefineTerm p0 fixByKey mkFixByDef + pure (Function.fixNAndType arity (void fixBy), Set.singleton fixByKey) pure (PLC.Def (PLC.VarDecl noProvenance name (noProvenance <$ fixNType)) (noProvenance <$ fixNTerm, Strict), fixNDeps) fixN <- lookupOrDefineTerm p0 fixNKey mkFixNDef diff --git a/plutus-core/plutus-ir/test/PlutusIR/Compiler/Recursion/factorial.golden b/plutus-core/plutus-ir/test/PlutusIR/Compiler/Recursion/factorial.golden index 2210a3ba2e3..0cd169bc9ba 100644 --- a/plutus-core/plutus-ir/test/PlutusIR/Compiler/Recursion/factorial.golden +++ b/plutus-core/plutus-ir/test/PlutusIR/Compiler/Recursion/factorial.golden @@ -2,27 +2,27 @@ 1.1.0 [ [ - (lam s_1651 [ s_1651 s_1651 ]) + (lam s_1609 [ s_1609 s_1609 ]) (lam - s_1652 + s_1610 (lam - i_1653 + i_1611 [ [ [ [ (force (builtin ifThenElse)) - [ [ (builtin equalsInteger) (con integer 0) ] i_1653 ] + [ [ (builtin equalsInteger) (con integer 0) ] i_1611 ] ] - (lam u_1654 (con integer 1)) + (lam u_1612 (con integer 1)) ] (lam - u_1655 + u_1613 [ - [ (builtin multiplyInteger) i_1653 ] + [ (builtin multiplyInteger) i_1611 ] [ - (lam x_1656 [ [ s_1652 s_1652 ] x_1656 ]) - [ [ (builtin subtractInteger) i_1653 ] (con integer 1) ] + (lam x_1614 [ [ s_1610 s_1610 ] x_1614 ]) + [ [ (builtin subtractInteger) i_1611 ] (con integer 1) ] ] ] ) diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/StrictLetRec/strictLetRec.golden b/plutus-core/plutus-ir/test/PlutusIR/Transform/StrictLetRec/strictLetRec.golden index 51f3ce0d059..d90d9f8a085 100644 --- a/plutus-core/plutus-ir/test/PlutusIR/Transform/StrictLetRec/strictLetRec.golden +++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/StrictLetRec/strictLetRec.golden @@ -3,222 +3,23 @@ (termbind (strict) (vardecl - fixBy - (all - F - (fun (type) (type)) - (fun - (fun (all Q (type) (fun [ F Q ] Q)) (all Q (type) (fun [ F Q ] Q))) - (fun - (all Q (type) (fun [ F Q ] [ F Q ])) (all Q (type) (fun [ F Q ] Q)) - ) - ) - ) + fix1 + (all a (type) (all b (type) (fun (fun (fun a b) (fun a b)) (fun a b)))) ) (abs - F - (fun (type) (type)) - (lam - by - (fun (all Q (type) (fun [ F Q ] Q)) (all Q (type) (fun [ F Q ] Q))) - [ - { + a + (type) + (abs + b + (type) + (lam + f + (fun (fun a b) (fun a b)) + [ { (abs a (type) - (abs - b - (type) - (lam - f - (fun (fun a b) (fun a b)) - [ - { - (abs - a - (type) - (lam - s - [ - (lam - a - (type) - (ifix - (lam - self - (fun (type) (type)) - (lam a (type) (fun [ self a ] a)) - ) - a - ) - ) - a - ] - [ (unwrap s) s ] - ) - ) - (fun a b) - } - (iwrap - (lam - self - (fun (type) (type)) - (lam a (type) (fun [ self a ] a)) - ) - (fun a b) - (lam - s - [ - (lam - a - (type) - (ifix - (lam - self - (fun (type) (type)) - (lam a (type) (fun [ self a ] a)) - ) - a - ) - ) - (fun a b) - ] - [ - f - (lam - x - a - [ - [ - { - (abs - a - (type) - (lam - s - [ - (lam - a - (type) - (ifix - (lam - self - (fun (type) (type)) - (lam - a (type) (fun [ self a ] a) - ) - ) - a - ) - ) - a - ] - [ (unwrap s) s ] - ) - ) - (fun a b) - } - s - ] - x - ] - ) - ] - ) - ) - ] - ) - ) - ) - (all Q (type) (fun [ F Q ] [ F Q ])) - } - (all Q (type) (fun [ F Q ] Q)) - } - (lam - rec - (fun - (all Q (type) (fun [ F Q ] [ F Q ])) - (all Q (type) (fun [ F Q ] Q)) - ) - (lam - h - (all Q (type) (fun [ F Q ] [ F Q ])) - (abs - R - (type) - (lam - fr - [ F R ] - [ - { - [ - by - (abs - Q - (type) - (lam fq [ F Q ] [ { [ rec h ] Q } [ { h Q } fq ] ]) - ) - ] - R - } - fr - ] - ) - ) - ) - ) - ] - ) - ) - ) - (let - (nonrec) - (termbind - (strict) - (vardecl - fix1 - (all a (type) (all b (type) (fun (fun (fun a b) (fun a b)) (fun a b)))) - ) - (abs - a - (type) - (abs - b - (type) - (lam - f - (fun (fun a b) (fun a b)) - [ - { - (abs - a - (type) - (lam - s - [ - (lam - a - (type) - (ifix - (lam - self - (fun (type) (type)) - (lam a (type) (fun [ self a ] a)) - ) - a - ) - ) - a - ] - [ (unwrap s) s ] - ) - ) - (fun a b) - } - (iwrap - (lam self (fun (type) (type)) (lam a (type) (fun [ self a ] a))) - (fun a b) (lam s [ @@ -234,96 +35,120 @@ a ) ) - (fun a b) + a ] - [ - f - (lam - x + [ (unwrap s) s ] + ) + ) + (fun a b) + } + (iwrap + (lam self (fun (type) (type)) (lam a (type) (fun [ self a ] a))) + (fun a b) + (lam + s + [ + (lam + a + (type) + (ifix + (lam + self + (fun (type) (type)) + (lam a (type) (fun [ self a ] a)) + ) a + ) + ) + (fun a b) + ] + [ + f + (lam + x + a + [ [ - [ - { - (abs - a - (type) - (lam - s - [ - (lam - a - (type) - (ifix - (lam - self - (fun (type) (type)) - (lam a (type) (fun [ self a ] a)) - ) - a + { + (abs + a + (type) + (lam + s + [ + (lam + a + (type) + (ifix + (lam + self + (fun (type) (type)) + (lam a (type) (fun [ self a ] a)) ) + a ) - a - ] - [ (unwrap s) s ] - ) + ) + a + ] + [ (unwrap s) s ] ) - (fun a b) - } - s - ] - x + ) + (fun a b) + } + s ] - ) - ] - ) + x + ] + ) + ] ) - ] - ) + ) + ] ) ) ) - [ - (lam - tup - (all r (type) (fun (fun (fun (con integer) (con integer)) r) r)) - (let - (nonrec) - (termbind - (strict) - (vardecl xxx (fun (con integer) (con integer))) - [ - { tup (fun (con integer) (con integer)) } - (lam arg_0 (fun (con integer) (con integer)) arg_0) - ] - ) - (con integer 1) + ) + [ + (lam + tup + (all r (type) (fun (fun (fun (con integer) (con integer)) r) r)) + (let + (nonrec) + (termbind + (strict) + (vardecl xxx (fun (con integer) (con integer))) + [ + { tup (fun (con integer) (con integer)) } + (lam arg_0 (fun (con integer) (con integer)) arg_0) + ] ) + (con integer 1) ) - (abs - r - (type) - (lam + ) + (abs + r + (type) + (lam + f + (fun (fun (con integer) (con integer)) r) + [ f - (fun (fun (con integer) (con integer)) r) [ - f - [ - { { fix1 (con integer) } (con integer) } - (lam - xxx - (fun (con integer) (con integer)) + { { fix1 (con integer) } (con integer) } + (lam + xxx + (fun (con integer) (con integer)) + [ [ - [ - { (builtin trace) (fun (con integer) (con integer)) } - (con string "hello") - ] - (lam z (con integer) [ xxx z ]) + { (builtin trace) (fun (con integer) (con integer)) } + (con string "hello") ] - ) - ] + (lam z (con integer) [ xxx z ]) + ] + ) ] - ) + ] ) - ] - ) + ) + ] ) \ No newline at end of file diff --git a/plutus-core/testlib/PlutusCore/Generators/QuickCheck/GenTm.hs b/plutus-core/testlib/PlutusCore/Generators/QuickCheck/GenTm.hs index 4ee92402686..d3b9d4f419d 100644 --- a/plutus-core/testlib/PlutusCore/Generators/QuickCheck/GenTm.hs +++ b/plutus-core/testlib/PlutusCore/Generators/QuickCheck/GenTm.hs @@ -75,7 +75,7 @@ One would be forgiven for thinking that you don't need `geAstSize` in `GenTm` be built-in to 'Gen'. However, if you use 'Gen's built-in size to control the size of both the terms you generate *and* the size of the constants in the terms you will end up with skewed terms. Constants near the top of the term will be big and constants near the bottom of the term will -be small. For this reason we follow QuickCheck best practise and keep track of the "recursion +be small. For this reason we follow QuickCheck best practice and keep track of the "recursion control size" separately from 'Gen's size in the 'geAstSize' field of the 'GenEnv' environment. I.e. we let the QuickCheck's size parameter to be responsible for the size of constants at the leaves of the AST and use 'geAstSize' to control the size of the AST itself.