Skip to content

Commit

Permalink
Add 'Note [Recursion combinators]'
Browse files Browse the repository at this point in the history
  • Loading branch information
effectfully committed May 6, 2024
1 parent 783503a commit a9056ed
Show file tree
Hide file tree
Showing 2 changed files with 48 additions and 2 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -142,7 +187,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
Expand Down Expand Up @@ -335,6 +379,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)
Expand All @@ -344,6 +389,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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down

0 comments on commit a9056ed

Please sign in to comment.