Skip to content

Latest commit

 

History

History
81 lines (58 loc) · 2.85 KB

lazy-definitions.md

File metadata and controls

81 lines (58 loc) · 2.85 KB
Raw

Making recursive definitions lazy

In strict-mode, some types of recursive terms will unroll indefinitely.

This is a simple piece of code that works on many other functional programming languages, including hvm's lazy-mode, but hangs on strict-mode:

Cons = λx λxs λcons λnil (cons x xs)
Nil  =        λcons λnil nil

Map = λf λlist
  let cons = λx λxs (Cons (f x) (Map f xs))
  let nil = Nil
  (list cons nil)

Main = (Map λx (+ x 1) (Cons 1 Nil))

The recursive Map definition never gets reduced. Using the debug mode -d we can see the steps:

(Map λa (+ a 1) (Cons 1 Nil))
---------------------------------------
(Map λa (+ a 1) λb λ* (b 1 Nil))
---------------------------------------
(Cons (λa (+ a 1) 1) (Map λa (+ a 1) Nil))
---------------------------------------
(Cons (λa (+ a 1) 1) (Nil λb λc (Cons (λa (+ a 1) b) (Map λa (+ a 1) c)) Nil))
---------------------------------------
...

For similar reasons, if we try using Y combinator it also won't work.

Y = λf (λx (f (x x)) λx (f (x x)))

Map = (Y λrec λf λlist
  let cons = λx λxs (Cons (f x) (rec f xs))
  let nil = Nil
  (list cons nil f))

By linearizing f, the Map function "fully reduces" first and then applies f.

Map = λf λlist
  let cons = λx λxs λf (Cons (f x) (Map f xs))
  let nil = λf Nil
  (list cons nil f)

This code will work as expected, since cons and nil are lambdas without free variables, they will be automatically floated to new definitions if the float-combinators option is active, allowing them to be unrolled lazily by hvm.

It's recommended to use a supercombinator formulation to make terms be unrolled lazily, preventing infinite expansion in recursive function bodies.

If you have a set of mutually recursive functions, you only need to make one of the steps lazy. This might be useful when doing micro-optimizations, since it's possible to avoid part of the small performance cost of linearizing lambdas.

Automatic optimization

Bend carries out match linearization and combinator floating optimizations, enabled through the CLI, which are active by default in strict mode.

Consider the code below:

Zero = λf λx x
Succ = λn λf λx (f n)
ToMachine = λn (n λp (+ 1 (ToMachine p)) 0)

The lambda terms without free variables are extracted to new definitions.

ToMachine0 = λp (+ 1 (ToMachine p))
ToMachine = λn (n ToMachine0 0)

Definitions are lazy in the runtime. Floating lambda terms into new definitions will prevent infinite expansion.

It's important to note that preventing infinite expansion through simple mutual recursion doesn't imply that a program lacks infinite expansion entirely or that it will terminate.