Thunks, Tasks, and Threads

A Thunk is defined as

# namespace Ex
# universe u
structure Thunk (α : Type u) : Type u where
  fn : Unit → α
# end Ex

A Thunk encapsulates a computation without evaluation. That is, a Thunk stores the way of how the value would be computed. The Lean runtime has special support for Thunks. It caches their values after they are computed for the first time. This feature is useful for implementing data structures such as lazy lists. Here is a small example using a Thunk.

def fib : Nat → Nat
  | 0   => 0
  | 1   => 1
  | x+2 => fib (x+1) + fib x

def f (c : Bool) (x : Thunk Nat) : Nat :=
  if c then
    x.get
  else
    0

def g (c : Bool) (x : Nat) : Nat :=
  f c (Thunk.mk (fun _ => fib x))

#eval g false 1000

The function f above uses x.get to evaluate the Thunk x. The expression Thunk.mk (fun _ => fib x) creates a Thunk for computing fib x. Note that fib is a very naive function for computing the Fibonacci numbers, and it would an unreasonable amount of time to compute fib 1000. However, our test terminates instantaneously because the Thunk is not evaluated when c is false. Lean has a builtin coercion from any type a to Thunk a. You write the function g above as

# def fib : Nat → Nat
#  | 0   => 0
#  | 1   => 1
#  | x+2 => fib (x+1) + fib x
# def f (c : Bool) (x : Thunk Nat) : Nat :=
#  if c then
#    x.get
#  else
#    0
def g (c : Bool) (x : Nat) : Nat :=
  f c (fib x)

#eval g false 1000

In the following example, we use the macro dbg_trace to demonstrate that the Lean runtime caches the value computed by a Thunk. We remark that the macro dbg_trace should be used for debugging purposes only.

def add1 (x : Nat) : Nat :=
  dbg_trace "add1: {x}"
  x + 1

def double (x : Thunk Nat) : Nat :=
  x.get + x.get

def triple (x : Thunk Nat) : Nat :=
  double x + x.get

def test (x : Nat) : Nat :=
  triple (add1 x)

#eval test 2
-- add1: 2
-- 9

Note that the message add1: 2 is printed only once. Now, consider the same example using Unit -> Nat instead of Thunk Nat.

def add1 (x : Nat) : Nat :=
  dbg_trace "add1: {x}"
  x + 1

def double (x : Unit -> Nat) : Nat :=
  x () + x ()

def triple (x : Unit -> Nat) : Nat :=
  double x + x ()

def test (x : Nat) : Nat :=
  triple (fun _ => add1 x)

#eval test 2
-- add1: 2
-- add1: 2
-- 9

Now, the message add1: 2 is printed twice. It may come as a surprise that it was printed twice instead of three times. As we pointed out, dbg_trace is a macro used for debugging purposes only, and add1 is still considered to be a pure function. The Lean compiler performs common subexpression elimination when compiling double, and the produced code for double executes x () only once instead of twice. This transformation is safe because x : Unit -> Nat is pure.