recursion

Sub-cards (0)Archived
Comments (2)
Reply

Mutual recursion can be expressed by taking a fixed point over the entire strongly-connected component.

Then if we ban explicit recursion from the language and make fix a primitive (or do the transformation under the hood), then the dependency graph is guaranteed to be acyclic!

Without cyclic dependencies, we can use content-addressable storage for definitions (as Unison does) and alpha-equivalent definitions get the same hash.

To be more precise, before hashing a definition:

  • references to local variables are replaced by de Bruijn indices

  • references to global definitions are replaced by hashes

Then renaming definitions/variables does not affect the computed hash.

Profile picture

So Unison also bans explicit recursion? Is it annoying to work with this restriction in practice?

Profile picture

Unison applies this transformation before hashing, but the surface language supports explicit recursion.

Profile picture

Oh great, sounds like the best of both worlds then.

Reply

Open recursion. Take a recursive function:

fib :: Natural -> Natural
fib =
  \n ->
  if n < 2 then n else fib (n - 1) + fib (n - 2)

Replace explicit recursion with fix:

fib :: Natural -> Natural
fib =
  fix \self ->
  \n ->
  if n < 2 then n else self (n - 1) + self (n - 2)

And now just remove fix from the definition (it can be used by the caller instead):

fib :: (Natural -> Natural) -> (Natural -> Natural)
fib =
  \self ->
  \n ->
  if n < 2 then n else self (n - 1) + self (n - 2)

Now this function is open-recursive. You can recover the original one by calling fix fib, but you can also transform each recursive call by e.g. adding memoization:

memo :: (Natural -> a) -> (Natural -> a)
memo f = \i -> table !! fromIntegral i
  where table = map f [0 ..]

Now by calling fix (memo . fib) instead of fix fib you get an asymptotic improvement.