4. HeapLang🔗

4.1. Introduction🔗

HeapLang is an untyped concurrent programming language with a heap. It is an ML-like language, sporting many of the usual constructs such as let expressions, lambda abstractions, and recursive functions. It also supports higher-order functions. The evaluation order is right to left and it is a call-by-value language.

The syntax for HeapLang is fairly standard, but there are some quirks as we are working inside Lean. As the features of HeapLang are fairly standard, the focus in this chapter is mainly on showcasing the syntax of the language through simple examples.

HeapLang in iris-lean has two notable characteristics:

Expressions live in the type Iris.HeapLang.Exp, and are written inside an embedded DSL hl( ... ) rather than via top-level notation. Values are inside hl_val(...).
Variable names are still strings underneath, but you do not need to quote them: write x rather than "x".

4.2. The HeapLang Interpreter (Optional)🔗

At the time of this writing, iris-lean does not include a HeapLang interpreter, so we cannot evaluate expressions to their runtime values directly in Lean. We still see, however, that HeapLang expressions are pieces of syntax we can inspect with #check.

TODO (upstream — iris-lean): once an exec evaluator lands, add #eval exec 10 ... lines to display the runtime value for each example below.

4.3. Pure Constructs🔗

open Iris.HeapLang

namespace HeapLangExamples

HeapLang has native support for integers and booleans. With these, we can do basic arithmetic and control flow. Note that values in HeapLang are prefixed by a #.

def arith : Exp := hl(#1 + #2 * #3)

The expected result of evaluating arith is 7.

def booleans : Exp := hl((#1 + #2 * #3 = #7) && #true || (#true = #false))

The expected result is #true.

-- TODO (upstream — iris-lean): use the unit literal here once the
-- `hl` DSL gains a sugared form for `Val.lit BaseLit.unit`.
def if_then_else : Exp := hl(if #true then #1 else #0)

iris-lean does not yet have a sugared spelling for the unit literal, so we use an integer in the consequent here instead.

HeapLang supports let expressions. Technically, let expressions are not native to HeapLang — they are sugar for application of a lambda to its argument. Note that variables in HeapLang are strings; in the Lean DSL, you write them as plain identifiers, and they elaborate to Exp.var "x".

def lets : Exp := hl(
  let a := #4;
  let b := #2;
  a + b)

HeapLang has native support for pairs, with tuples being notation for nested pairs.

def pairs : Exp := hl(
  let p := (#40, #1 + #1);
  fst(p) + snd(p))

def tuples : Exp := hl(
  let t1 := (#1, #2, #3, #4);
  let t2 := (((#1, #2), #3), #4);
  snd(fst(fst(t1))) = snd(fst(fst(t2))))

We can also do pattern matching using sums. A common use case of sums is the option construction.

def sums : Exp := hl(
  let r := injr(#1);
  match r with
  | injl(_) => #0
  | injr(n) => n + #1
  )

def option : Exp := hl(
  let r := some(#1);
  match r with
  | none() => #0
  | some(n) => n + #1
  )

Finally, we have lambda abstractions and recursive functions. As with let expressions, lambda abstractions are also a derived construct — they are recursive functions that do not recurse. In HeapLang, functions are first-class citizens, which gives support for higher-order functions.

def lambda : Exp :=
  hl(let add5 := (λ x, x + #5);
     let double := (λ x, x * #2);
     let compose := (λ f g, λ x, g (f x));
     compose add5 double #5)

def recursion : Exp :=
  hl(let fac := (rec f n := if n = #0 then #1 else n * f (n - #1));
     (fac #4, fac #5))

4.4. References🔗

References are dynamically allocated through the ref(_) construct. Given a value, ref(_) finds a fresh location on the heap and stores the value there. The location is then returned.

def alloc : Exp := hl(
  let l1 := ref(#0);
  let l2 := ref(#0);
  (l1, l2))

After allocation, we can read and update the value at the returned location l with !l and l ← v, respectively. The store uses the left-arrow ←.

def load : Exp := hl(
  let l := ref(#5);
  !l)

def store : Exp := hl(
  let l := ref(#5);
  l ← #6;
  !l)

To allow for synchronisation between threads, HeapLang provides a single primitive called compare-and-exchange, written cmpXchg(l, v1, v2). This instruction atomically reads the contents of location l, checks if it is equal to v1, and, in case of equality, updates l to contain v2. The instruction returns a pair (v, b), with v being the original value stored at l, and b a boolean indicating whether the location was updated.

def cmpxchg_fail : Exp := hl(
  let l := ref(#5);
  cmpXchg(l, #6, #7))

def cmpxchg_suc : Exp := hl(
  let l := ref(#5);
  cmpXchg(l, #5, #7))

iris-lean also provides a variant of cmpXchg called compare-and-set, written cas(l, v1, v2). The only difference is that cas only returns the boolean.

-- TODO (upstream — iris-lean): use the unit literal in the success
-- branches once the `hl` DSL gains a `#()` form.
def cas_example : Exp := hl(
  let l := ref(#5);
  if cas(l, #6, #7) then #0 else
    let a := !l;
    if cas(l, #5, #7) then
      let b := !l;
      (a, b)
    else
      #0)

We substitute #0 in the success branches here for the same reason as in the if_then_else example above: there is not yet a sugared spelling for the unit literal.

4.5. Concurrency🔗

HeapLang has only one primitive for concurrency: fork(_). The instruction fork(e) creates a new thread which executes e. The invoking thread continues execution after creation. If the computation of e terminates, then the resulting value is simply thrown away. Hence, e is only run for its side effects.

def forkEx : Exp := hl(
  let l := ref(#5);
  fork(l ← #7);
  !l)

From the fork primitive, we can implement several other constructions for concurrency, such as spawn and par, which are derived from fork. At the time of writing, iris-lean has not yet ported these libraries, so this chapter does not include examples that use them.

TODO (upstream — iris-lean): once the spawn / par libraries are ported, add the two corresponding examples here. A reference implementation (to port once the prerequisite lands) is reproduced below.

(* Reference implementation — to port once iris-lean has spawn/par *)
Example spawn_ex : expr :=
  let: "l" := ref #5 in
  let: "handle" := spawn (λ: "_", "l" <- #6;; #2) in
  let: "res" := spawn.join "handle" in
  let: "v" := !"l" in
  ("res", "v").
(* Evaluates to (2, 6). *)

Example par_ex : expr :=
  let: "l" := ref #5 in
  let: "res" := (!"l" + #1) ||| (!"l" + #2) in
  Fst "res" + Snd "res".
(* Evaluates to 13. *)

end HeapLangExamples