Forsp: A Forth+Lisp Hybrid Lambda Calculus Language

Recently I've discovered a very interesting language / realization of the Lambda Calculus. I was unable to find any other language like it, which I find quite surprising. In hindsight, the language seems obvious and natural. And the language keeps surprising me. I say "discovered" in the same sense that Paul Graham says that McCarthy "discovered Lisp" (link).

It's a hybrid language combining Forth and Lisp, so naturally it's called Forsp (code)!

Forsp has:

It's evaluator is very simple. I suspect simpler than a McCarthy Lisp eval() function, but I haven't defined a "simplicity function", so you can be the judge.

In contrast to Lisp, apply() is trivial in Forsp, and instead we have a core function called compute()

Computation

Computation processes a list of instructions that work like a Forth.

Application

An example:

  foo bar

Semantically, this means:

  1. call foo
  2. call bar

Functions manipulate an operand/value stack implicitly like Forth. Therefore, operationally they take no formal arguments and return no values. However, semantically, they can be viewed as pure functions with stack -> stack signatures: take the stack as an argument and return a new stack.

Special Forms

There are 3 syntactic special forms, but only 1 is special at evaluation-time.

Syntax Parsed as Semantics
'foo quote foo The quoted literal (foo) is retained as-is and pushed to the stack
$foo quote foo pop A value will be popped from the stack and bound to "foo" in the environment
^foo quote foo push The name "foo" will be resolved in current environment and pushed to the stack

As you can see, "quote" is the only form that requires special handling by the evaluator. Both "pop" and "push" can be implemented as ordinary built-ins.

The syntax forms are not strictly required, but they make coding much more manageable.

Thunking and Forcing

()

In Forsp, parenthesis grouping is used as a thunking operator.

As an example:

(foo bar)

is the thunked-computation of:

foo bar

A thunk is pushed to the stack like any other value. Thunks can be forced by using the force term (see [1]). The force term pops a value from the stack and forces the computation. This means that:

(foo bar) force

is the same computation as:

foo bar

Similarly:

^a force

is the same computation as just

a

Furthermore, thunks are closures. They bind the current environment on creation.

This means that in the following:

(fn) 'a $fn force

We (1) thunk a computation involving fn, (2) rebind fn to a, (3) force the thunk.

The computation will use the original fn rather than the re-bound fn

What else?

That's all. Seems too simple?

We'll it's shockingly expressive. Let's demonstrate!

Lambda Calculus

Forsp can express the lambda calculus via very simple re-write/re-ordering rules.

Abstraction

In Lambda Calculus, an abstraction is written as:

λx.M

where x is a variable bound on application and M is some body, possibly using x

In Forsp, we can express this as:

($x M)

Application

In Lambda Calculus, an application is written as:

MN

where M and N are two different terms and we're applying M to N

In Forsp, this is similar but transposed:

^N M

Notice also that we use ^N because we don't wish to apply N at this moment

Let's translate some more complicated lambda terms:

TRUE  := λx.λy.x
FALSE := λx.λy.y
IF    := λp.λt.λf.(p t f)
IF TRUE 1 2

In Forsp (direct translation):

(
  ($x $y ^x) $true
  ($x $y ^y) $false
  ($p $x $y ^y ^x p) $if
  2 1 ^true if
)

After execution, 1 will be the only value left on the stack.

You can check by inserting the following after the if:

stack print

This is a very handy debugging code sequence.

Binding Names

Notice that the pattern:

(stuff here) $name
... SNIP ...

is used to bind names to function closures. The thunk is pushed after the closure is bound and then the $name operation pops it back off the stack and binds the name so we can use it.

This name-bind sequence is equivalent to the following lambda-calculus form:

(λname.(
  ... SNIP ...
))
λ.(stuff here)

which could be written more directly/verbosely in Forsp as:

(
  (stuff here)
  ($name
    ... SNIP ...
  ) force
)

Call-By-Push-Value (CBPV)

Most languages based on Lambda Calculus have to contend with a choice between Normal Order Evaluation (Call-By-Value,CBV) or Applicative-Order (Call-By-Name,CBN). Eager languages (most of them) are CPV and Lazy languages (notably Haskell) are CBN. But Forsp is neither, it is Call-By-Push-Value (CBPV).

CBPV treats lambda variable binding as being "popped" and application arguments as being "pushed". Further, there is a concept of "thunking" and "forcing". This should sound familiar, Forsp is inspired by Paul Levy's CBPV work.

In fact, while reading about CBPV, I couldn't help but think "That's Just Forth!", and thus Forsp was born.

The very interesting upshot of this is that Forsp can have the determinism/eagerness nature of a CBV language when desired, but also the deferred/lazy nature of a CBN language when useful.

Here's an example of this, defining a block-structured if:

(
  ; NOTE: "cswap" is a "conditional swap" primitive.
  ;       It consumes a "cond" argument and if it's equal to the atom "t", then it performs a swap
  ;       on the top two elements of the stack

  ; Explanation:
  ;   (1) conditionally swap the true and false blocks, (2) drop the unused one, (3) force the remaining one

  (cswap $_ force) $if

  ('false print)
  ('true print)
  't if
)

This code only prints "true", which shows that the false case never executed.

But, this is just a simple case, the full power is much more.

Recursion

In lambda calculus, achieving recursive functions can be cumbersome since lambda-abstractions don't have a way to refer to themselves. In Lisp, this leads to solutions like "LABEL". Usually, an implementation includes some special-form to help with it.

Forsp has no such special-form. It solves the issue the same way the Lambda Calculus does: a fixpoint combinator, the Y Combinator.

In Lambda Calculus:

Y := λf.(λx.f(x x))(λx.f(x x))
Yg = g(Yg) = g(g(Yg)) = g(g(g(Yg))) = ...

In CPV languages, the Y-Combinator leads to infinite recursion and cannot be used.

But, Forsp is CBPV, so it actually can:

;; Y-Combinator
(
  ($f
    ($x (^x x) f)
    ($x (^x x) f)
    force
  ) $Y
)

We can use it to define a classic recursive factorial as:

(
 ; ... SNIP ... Assuming "Y" and "if" are defined previously

 ($g (^g Y)) $rec  ; syntax sugar for applying the Y-Combinator

 ($self $n
    (^n 1 - self ^n *) 1 0 ^n eq if
 ) rec $factorial

  5 factorial print
)

Which will print "120" as desired. Notice that we defined a little "rec" helper function. This makes the syntax similar to the ML "let rec" syntax.

Stack Languages are Confusing

So you say "stack languages are confusing and backwards"? Well we can fix that too. Take our "if" construct.

Currently we write:

(
  ^false_block
  ^true_block
  ^condition
  if
)

Instead we'd prefer something like:

(
  ^if (condition computation)
    ^true_block
    ^false_block
  endif
)

Let's do it!

(
  (force cswap $_ force)       $if
  ($f $t $c $fn ^f ^t ^c fn)   $endif

  ^if (0 1 eq)
    ('true print)
    ('false print)
  endif
)

Much better.

With this, we can write a nicer "factorial":

(
 ; ... SNIP ... Assuming previously defined functions

 ($self $n
    ^if (^n 0 eq) 1
      (^n 1 - self ^n *)
    endif
 ) rec $factorial

  5 factorial print
)

Syntax Parsing

Syntax is S-Expressions, but like Lisp there is a tiny modification for special-forms. In Lisp, "'something" is converted to "(quote something)" by the parser. In Forsp, we convert somewhat similarly:

'something => quote something
^something => quote something push
$something => quote something pop

Similar to Lisp, the Forsp parser also skips line-comments that start with ";"

Implementation

The implementation is simple and ~600 lines of clean C code. It's effectively a Lisp interpreter implementation with different semantics. That is to say, Forsp has atoms, interning, cons cells, environment, read, print, eval, etc.

The core "eval/compute" routines are given below to demonstrate their stunning simplicity:

void eval(obj_t *expr, obj_t **env);

void compute(obj_t *comp, obj_t *env)
{
  while (comp != state->nil) {
    // unpack
    obj_t *cmd  = car(comp);
    comp = cdr(comp);

    if (cmd == state->atom_quote) {
      if (comp == state->nil) FAIL("Expected data following a quote form");
      push(car(comp));
      comp = cdr(comp);
      continue;
    }

    // atoms and (...) get ordinary eval
    eval(cmd, &env);
  }
}

void eval(obj_t *expr, obj_t **env)
{
  if (IS_ATOM(expr)) {
    obj_t *val = env_find(*env, expr);
    if (IS_CLOS(val)) { // closure
      return compute(val->clos.body, val->clos.env);
    } else if (IS_PRIM(val)) { // primitive
      return val->prim.func(env);
    } else {
      return push(val);
    }
  } else if (IS_NIL(expr) || IS_PAIR(expr)) {
    return push(make_clos(expr, *env));
  } else {
    return push(expr);
  }
}

There are 10 core primitives (needed to self-implement):

/* Core primitives */
void prim_push(obj_t **env) { push(env_find(*env, pop())); }
void prim_pop(obj_t **env)  { obj_t *k, *v; k = pop(); v = pop(); *env = env_define(*env, k, v); }
void prim_eq(obj_t **_)     { push(obj_equal(pop(), pop()) ? state->atom_true : state->nil); }
void prim_cons(obj_t **_)   { obj_t *a, *b; a = pop(); b = pop(); push(make_pair(a, b)); }
void prim_car(obj_t **_)    { push(car(pop())); }
void prim_cdr(obj_t **_)    { push(cdr(pop())); }
void prim_cswap(obj_t **_)  { if (pop() == state->atom_true) { obj_t *a, *b; a = pop(); b = pop(); push(a); push(b); } }
void prim_tag(obj_t **_)    { push(make_num(pop()->tag)); }
void prim_read(obj_t **_)   { push(read()); }
void prim_print(obj_t **_)  { print(pop()); }

Some extra "non-essential" primitives are also included:

void prim_stack(obj_t **_) { push(state->stack); }
void prim_env(obj_t **env) { push(*env); }
void prim_sub(obj_t **_)   { obj_t *a, *b; b = pop(); a = pop(); push(make_num(obj_i64(a) - obj_i64(b))); }
void prim_mul(obj_t **_)   { obj_t *a, *b; b = pop(); a = pop(); push(make_num(obj_i64(a) * obj_i64(b))); }
void prim_nand(obj_t **_)  { obj_t *a, *b; b = pop(); a = pop(); push(make_num(~(obj_i64(a) & obj_i64(b)))); }
void prim_lsh(obj_t **_)   { obj_t *a, *b; b = pop(); a = pop(); push(make_num(obj_i64(a) << obj_i64(b))); }
void prim_rsh(obj_t **_)   { obj_t *a, *b; b = pop(); a = pop(); push(make_num(obj_i64(a) >> obj_i64(b))); }

And, as any good Forth has low-level functions, so does Forsp (if desired):

#if USE_LOWLEVEL
/* Low-level primitives */
void prim_ptr_state(obj_t **_)    { push(make_num((int64_t)state)); }
void prim_ptr_read(obj_t **_)     { push(make_num(*(int64_t*)obj_i64(pop()))); }
void prim_ptr_write(obj_t **_)    { obj_t *a, *b; b = pop(); a = pop(); *(int64_t*)obj_i64(a) = obj_i64(b); }
void prim_ptr_to_obj(obj_t **_)   { push((obj_t*)obj_i64(pop())); }
void prim_ptr_from_obj(obj_t **_) { push(make_num((int64_t)pop())); }
#endif

There's really not much else besides standard Lisp implementation details.

The full source is here

Self-Evaluator

Naturally, A Lisp needs to be able to implement itself elegantly.

Forsp succeeds here too. The core "eval/compute" routines are given below (in just 18 non-comment lines!):

  ; compute [$comp $stack $env -> $stack]
  ($compute $eval
    ^if (dup is-nil) (rot $_ $_) ( ; false case: return $stack
      stack-pop
      ^if (dup 'quote eq)
        ($_ stack-pop rot swap stack-push swap ^eval compute)
        (swap $comp eval ^comp ^eval compute) endif
    ) endif
  ) rec $compute

  ; eval: [$expr $stack $env -> $stack $env]
  ($eval
    ^if (dup is-atom) (
      over2 swap env-find dup $callable
      ^if (dup is-closure) (swap $stack cdr unpack-closure ^stack swap ^eval compute)
      (^if (dup is-clos)   (force)
                           (stack-push)  endif) endif)
    (^if (dup is-list)
      (over2 swap make-closure stack-push)
      (stack-push) endif) endif
  ) rec $eval

The full implementation with all utility functions, type-checking, recursion, environment, stack operations, closure operations, compute/eval, and primitives is under 80 lines of Forsp code!

It can be found here

Unexpected Discoveries

I stumbled across Forsp while thinking about CBPV and minimalist bootstrapping languages (unrelated project). It kind of just appeared and then has continued to surprise me. In many ways it feels more fundamental than Lisp or Forth. It appears to be both simpler than Lisp and more powerful than Forth.

A fascinating thing about Forsp is that is seems to naturally express multiple computation fundamentals. For starters, a stack is a very natural computational structure. For example: a Turing Machine can be viewed as two-stacks and a process moving values between them. Between the value stack and cons'ing lists, it often feels like exactly this. On the other side, it expresses lambda calculus quite comfortably, and the variable binding syntax is naturally similar to A-Normal Form.

It's also curious that Forsp programs can be viewed as either as one big long list of instructions (much like a Turing Machine) or as a realization of Lambda Calculau.

The addition of variables to a Forth style language is very helpful. Rather than dealing with a complicated stack dance, you can just do ($x do a bunch of things ^x USE). This pattern has occurred enough that I've started calling it "value lifting".

Because of the stack+variable combination, Forsp code can express the same code in multiple ways:

Variable-binding / sequenced / imperative:

($a $b $c
   ^c ^b * $result
   ^a ^result + $result
   ^result
) $multiply_add

Functional / Point-free / Pipelined / Data-flow

(* +) $multiply_add

Even though this example makes the later look more elegant, both forms are quite useful. Often the later form is hard to achieve so elegantly in practice.

Other discoveries that surprised me:

I suspect there are more discoveries. Let me know if you find some.

Conclusion

There's so much more I could say, but this seems like a good time to wrap up.

If you're interested in learning more, the repository is here.

There are many good examples to explore here.

And, if you enjoyed this, you can:

Footnotes

[1] "force" is not a primitive. But, it can be easily defined as:

($x x) $force