1. Why these docs?

This website has some updates to Koka's documentation with more information about less well-known or documented Koka features

1.1. New Features

In order of newness, the following features have been added to Koka:

1.1.1. Qualified Names and Overloading

Qualified names and Implicits are two new features of Koka.

Multiple dispatch style overloading (overloading that considers all the types of the arguments) has existed in Koka for a while, but was problematic for a few reasons:

• There was no way to disambiguate between functions with the same name if they were both brought into the same scope and operated on the same parameters, even if the return type was different.
• There was no good way to overload constants (i.e. zero for both types int and float64)

Recently we added a new feature called locally qualified names. Using qualifiers we can now precisely disambiguate when we have multiple functions with the same name. For example we can define two mapping functions for lists, and specialize them to work on different types of lists:

fun int/map(xs: list<int>, f: int -> int): list<int> ...
fun float64/map(xs: list<float64>, f: float64 -> float64): list<float64> ...

and these can coexist peacefully with the normal definition for map

fun list/map(l: list<t>, f: t -> r): list<r> ...

Additionally all functions are also qualified by their module path so that you can distinguish between different functions with the same name from different modules even if they are not locally qualified.

We split the standard library into smaller modules to avoid adding too many local qualifiers. This seems to work well in practice, and we recommend putting functions that are defined with the same first parameter type in a module together.

1.1.2. Implicits

Implicit arguments are Koka's answer to type classes or ad-hoc polymorphism. While several languages have implicit arguments, (e.g. Scala, Coq, Lean), most of them occur in proof systems, and are different than Koka's approach.

In particular, Koka's implicits are not resolved solely by finding an appropriate term of the matching type, but rather by finding a term matching the unqualified name of the parameter that unifies correctly. If multiple terms match, the type checker will report the ambiguity.

A simple use case is for showing a value that has generic type. For example, this is how show can be defined for a list.

fun list/show(l: list<a>, ?show: (a) -> string): string
  "[" ++ l.map(show).join(", ") ++ "]" 

Note the ? prefixing the show parameter. This marks this parameter as being inferred using the name show at the application site.

If you need more than one implicit resolved by the same name but with different types you can make implicit parameters locally qualified.

fun tuple/show(l: (a,b), ?a/show: (a) -> string, ?b/show: (b) -> string): string
  match l
    (a, b) -> "(" ++ a.show ++ ", " ++ b.show ++ ")"

Of course we can also define more specialized versions of show for specific lists, and they can be used when in scope.

// A special show for characters
//   When resolving an implicit parameter `?show` the
// `chars/show` will be preferred over `list/show` as the chain is shorter
fun chars/show( cs : list<char> ) : string
  "\"" ++ cs.map(string).join ++ "\""

Implicit arguments can also require other implicits, and the type checker will fill in the dependencies. For example, to show a list l2: list<list<int>> koka will fill in the implicit show parameter for the inner list as well.

l2.show
// will be inferred as
l2.list/show(?show=fn(l) l.list/show(?show=int/show))
// with all of the implicit parameters eta expanded and filled in explicitly.

VSCode will show you the inferred implicits and qualified identifiers when you press Ctrl+Alt.

As a consequence of this design, implicits have no runtime machinery. We plan on measuring the impact on code size and deduplicating implicits in the future (but this is not implemented yet).

Implicits are purely a compile-time feature, and are resolved during type inference at the same time as overloading is resolved. However due to the stage at which they are resolved, the compiler cannot tell that you need an overloaded name to be inferred and type checked prior to a usage of that definition when trying to resolve an implicit.

Therefore, implicits enforce the following rule on usage - Definitions used as implicit arguments should be defined prior to their usage in the file

When resolving any usage of an identifier Koka follows the following rules to resolve overloading - If a qualified name is used, than it refers to a definition unambiguously and proceeds to resolve implicits - If a local variable of the correct name and type is in scope, it is given preference over other definitions - If the name is unique and no overloads exists, that singular definition is used and implicits are resolved - If the name is ambiguous, try to infer the type of the minimum number of arguments that makes the overloaded identifier uniquely unifiable and then proceed to resolve implicits - If the name is still ambiguous, report an ambiguity When proceeding to resolve implicits - The name of the parameter (without local qualifiers) is used to search for a definition avaiable at the call site - The overloading an implicit rules are used recursively to resolve the implicits - Shorter chains of implicits are preferred over longer chains - If the compiler cannot find a unique shortest implicit chain, it will report an ambiguity - If the compiler cannot find a corresponding definition with the correct type it will report an error

As such, overuse of static overloading or deeply nesting implicits is bad practice for the following reasons: 1. It makes implicit resolution more expensive 2. It can make code harder to read and understand 3. It can result in ambiguities in the middle of an implicit chain which you have to expand manually

It is best practice to: 1. Only overload unambiguously (i.e. with different types) 2. Prefer overloading where the first argument type can distinguish the definitions completely 3. Avoid deeply nesting generic types

If you absolutely need to create an ambiguous overloaded definition that is likely to be used in a nested implicit there are ways to mitigate issue number (3), which has something to do with best practice (3). Let's suppose you have an overloaded definition for show on lists, because you want to show lists with each element on their own line.

fun nl/show(l: list<a>, ?show: (a) -> string): string
  l.map(show).join("\n")

And then lets suppose that you have a nested list of lists and you want the outer list to be shown with each element on its own line, but the inner list to be shown with each element on the same line. This is easy

val l2: list<list<int>> = ...
l2.nl/show()

Qualifying the outer show is enough in this case. However, let's say that you want to now overload show on integers, to pad them with a single zero if less than 10.

fun padded/show(i: int): string
  if i < 10 then "0" ++ i.show else i.show

Well now your deeply nested list is ambiguous, and you have to manually expand it.

val l2: list<list<int>> = ...
l2.nl/show(?show=list/show(?show=padded/show))

This is a bit of a pain. To mitigate this we can define a new value type that wraps our list of integers.

value struct paddedlist {inner : list<int>}
fun padded/show(pl: paddedlist): string
  pl.inner.show(?show=padded/show)

And now the list<paddedlist> using a shortest chain rule will definitely resolve to the correct definition.

I hope we add newtypes & proxying to Koka to make this even cleaner and not introducing a new type at runtime.

1.1.3. Named and Scoped Handlers

Named handlers allow us to define multiple handlers for the same effect that are lexically distinct from one another. For example, to define a handler for managing a file, we can write:

named effect file
  fun read-line() : string   // `:(file)   -> <exn> a`
// a (named) handler instance for files
fun file(fname, action) 
  var content := read-text-file(fname.path).lines
  with f <- named handler 
    fun read-line() 
      match content  
        Nil -> "" 
        Cons(x,xx) -> { content := xx; x }
  action(f)
pub fun main() 
  with f1 <- file("package.yaml")
  with f2 <- file("stack.yaml")
  println( f1.read-line() ++ "\n" ++ f2.read-line() )

This allows us to have two separate handlers for the same effect, and to use them in the same scope. The named keyword is used to define a handler instance, and the with statement is used to bind a handler instance to a variable. The handler instance can then be used as a regular handler, and it can be passed to other functions.

When used with handlers that involve multiple resumptions, you must be careful to ensure that the handler instance does not escape the scope of the resumption. For example, the following code is incorrect, and will fail at runtime:

fun wrong-escape1() 
  with f <- file("stack.yaml")
  f
pub fun test() 
  val f = wrong-escape1()
  f.read-line.println

To ensure that the handler instance does not escape, you can mark the effect as a scoped effect.

named scoped effect file<s::S> 
  fun read-line() : string  // `: (f : file<s>) -> scope<s> string`
// a handler instance for files
fun file(fname : string, action : forall<s> file<s> -> <scope<s>|e> a ) : e a 
  var i := 0
  with f <- named handler 
    fun read-line()
      i := i + 1
      (fname ++ ": line " ++ i.show)
  action(f)

When creating the file the function file quantifies the action function by a polymorphic scope s, and connects that to the scope of the file instance passed to the action. Each action is guaranteed to not escape the scope of the action method due to the scope polymorphism. Scope types which are recognized by the ::S kind annotation are not limited to just effect handlers, and can be used with other variables. See the samples/named-handlers directory on github or in your Koka installation for more complex examples of both named handlers and scoped effects and types.

1.2. Less Documented Features

The following keywords or features are less well-known or documented in Koka:

1.2.1. Type Definitions

Abstract Types

abstract in front of a type declaration will make the type non-constructible outside the current module. In addition it will not auto create the copy function or value accessors. This is used in the standard libraries for external types defined by the runtime, as well as types such as sslice which has specific guarantees about relations between its fields that it needs to take serious responsibility for to avoid undefined behavior such as segfaults.

Coinductive Types

Coinductively defined types have no special aspect to them at this point as far as I know other than to be reserved for functional completeness.

Extensible Types

Exensible types allow you to add constructors to a type from outside the type's definition. It is used for example in the standard library's exception-info type, which allows you to add additional information to an exception.

The syntax is as follows:

open type mytype
  Constr1(a: int)
  Constr2(b: string)

extend type mytype
  Constr3(c: float64)

Note that for extensible types, the extended type must have public visibility pub or you will run into a known bug. Also note that pattern matching will no longer be exhaustive so you must have exn in the effect row when pattern matching on an extensible type if there is no sensible default or catch all case.

There is still work to do to make extensible types work well with the rest of the language, in particular with implicits and overloading.

1.2.2. Generated Functions

Types have a number of generated functions for convenience. These include: - copy for copying a value while replacing some values (typically specified via named parameters) - is-<constructor> for checking if a value is of a certain constructor (e.g. is-nil or is-cons for lists). Note that the name of the constructor has it's first character lowercased. - <field> for accessing a field of the value (all constructors in an enumerated type must have the field with identical type to generate this function).

It should be noted that reference counting works better with pattern matching at the moment. However, we will make these generated functions more efficient in the future.

The copy function is typically invoked by directly postfixing the value with () and specifying the named parameters. (It looks like you are calling the value as a function).

Type Aliases

Type aliases are a way to give a new name to an existing type. This can be useful for documentation purposes or to make the code more readable. For example, you could define a type alias for a function type that takes an integer and returns a string as follows:

alias i-to-s = int -> string
alias i-to-s-e<e> = int -> e string

Type parameters are allowed in type aliases. Type aliases are transparent, meaning that they are sometimes expanded when type checking, and do not hide any methods on the original type.

While this might not seem useful, they are particularly useful for giving aliases to groups of effects that you often use, or to give names to function types.

For example, in the standard library we have the following type aliases:

alias pure = <div,exn>
alias st<h> = <alloc<h>,read<h>,write<h>>

Vectors

Vectors in koka are implemented as a fixed sized array. They allow mutable updates when used as a local variable, which typically results in functional behavior.

Additionally in the extended standard library available here, we have a new module std/data/vector-list which exposes a type vector-list<t> with a short alias vlist<t> which provides a functional interface to vectors. This means that it uses expensive copies when the vector is updated, unless there is a single reference to the vector. Unfortunately locally mutable variables at the moment keep around too many references, to work around this for now you can rebind the update to another local binding, or bind it recursively.

Matching

All defined types (except abstract ones outside their definiting module), can participate in pattern matching.

The syntax is very familiar to most functional programmers, including an expression descriminant, and a series of cases separated by newlines.

fun sum(xs: list<int>): int
  match xs
    Nil -> 0
    Cons(x, xs) -> x + sum(xs)

Each case is indented and separated from it's body by an arrow ->. The bodies can follow on the next line (indented), or be on the same line as the arrow. Additionally additional guards can be added to each case by adding a | and a boolean expression before the arrow.

For example to gather the integers greater than 0 from a list we can do:

// BEGIN:sum-first-two
fun sum-first-two(xs: list<int>): list<int>
  match xs
    Cons(x, tail as Cons(y, _)) -> Cons(x + y, tail)
    xs' -> xs'
// END:sum-first-two

// BEGIN:gather-positives
fun gather-positives(xs: list<int>): list<int>
  match xs
    Nil -> Nil
    Cons(x, xs) | x > 0 -> Cons(x, gather-positives(xs))
    Cons(_, xs) -> gather-positives(xs)
// END:gather-positives

Using guards reduces nesting a bit compared to using if statements. However, the guard expression must not use any effects including divergence. Otherwise it could manipulate state, or prevent any matches! If you really need to use effects, you can always use an if statement inside the case, or bind a value prior to the match. Each case is checked in order, and if the cases are not exhaustive, the compiler will infer an exception effect, which will throw a message at runtime stating where the pattern match failed.

Additionally Koka has support for naming subpatterns which can then be used in the body of the case. For example to return a list where the first element of the new list is the sum of the first two elements of the old list, but with the rest of the list unchanged, we can do the following:

// BEGIN:sum-first-two
fun sum-first-two(xs: list<int>): list<int>
  match xs
    Cons(x, tail as Cons(y, _)) -> Cons(x + y, tail)
    xs' -> xs'
// END:sum-first-two

// BEGIN:gather-positives
fun gather-positives(xs: list<int>): list<int>
  match xs
    Nil -> Nil
    Cons(x, xs) | x > 0 -> Cons(x, gather-positives(xs))
    Cons(_, xs) -> gather-positives(xs)
// END:gather-positives

To match on two values at once, join them together in a tuple and match on the tuple.

1.2.3. Parameters

All parameters to top level functions must be named. As such, arguments can be passed named or in order.

Additionally parameters can be marked as borrowed by prefixing the name with the caret ^.

This can be useful to avoid unnecessary reference counting on parameters that you know will be live for the duration of the function call (such as higher order function parameters, including implicits). However, it will mean that the parameter including any variables captured under a lambda will not be freed as early as it could. For data structures that will be destructed using a match statement, it is almost always better to rely on the default owned semantics, which will let Koka reuse the memory in place.

1.2.4. Return Statement

The return statement allows you to return early from a block of code. However, the rest of the function after the early return must also type check to the same type as the expression given to return.

1.2.5. Function Modifiers

The various function modifiers to guarantee certain properties related to reference counting are more details now here 1.7.

1.2.6. Divergence Inference

Koka infers the divergence effects in four particular situations:

1. When a function is self-recursive
2. When functions call each other in a mutually recursive way.
3. When a heap allocated reference is read, but it's value also could reference the same heap, (which could diverge due to self referential functions).
4. Where handlers could cause divergence through their operations involving functions that reference the effect itself.

Of these only the first (self-recursion) can be eliminated by the compiler automatically by using an inductive argument, and realizing that the discriminant will always get smaller.

To augment this you can add an import for the std/core/undiv module and use the pretend-decreasing on arguments that you know to be decreasing (such as parallel reduction on multiple parameters). This will allow the compiler to finish the argument for removing div.

However, this technique will not work for mutual recursion or any other form of divergence.

One solution for these cases is to internally name the mutually recursive functions name and then expose a function that wraps the internal function and with a call to pretend-no-div from the std/core/undiv module (e.g. pretend-no-div(fn() internal())). This will remove the div effect without removing any other effects.

1.2.7. Final Effects

You can use final ctl to denote that the effect operation never resumes.

pub effect fail<b>
  final ctl fail(info: b) : a

1.2.8. Linear Effects

Linear effects are effects whose handlers are always guaranteed to be used in a linear fashion. This severely restricts what kinds of handlers can be implemented for those effects (including disallowing calls to any potentially other non-linear effect within the handler operations - for example exn).

You can create a linear effect by prefixing the effect definition with linear

linear effect pretty
  val indentation: int
  fun print(s: string): ()

In practice it does reduce the generated code size quite a bit, but doesn't have a large impact on performance, since Koka already provides information about the linearity of handlers in the runtime system. So it is more of a semantic guarantee and restriction, and should not be used for performance reasons.

For more fine grained restrictions on handlers and operations make your handler use fun or val operations. (You can even allow general ctl operations in the effect definition, but then give it a more restricted definition in the handler).

1.3. Less Known Features

1.3.1. Integrated External Definitions

Koka supports the integration of external definitions from other languages. This is useful when you want to use a library that is not available in Koka, or when you want to use a library that is not yet available in Koka. The external definitions are integrated into the Koka program and can be used as if they were written in Koka.

You use the extern keyword to declare an external definition.

The simplest way to integrate external definitions is to provide an inline implementation for each target language. For example, the following code provides an inline implementation for C and JavaScript: (targets include “c”, “js”, and “cs” (csharp))

extern sizeofint(): int32
  c inline "sizeof(int)"
  js inline "4"

To provide arguments simply use a # followed by the argument number. For example, the following code provides an inline implementation for C and JavaScript:

extern add(x: int32, y: int32): int32
  c inline "($1 + $2)"
  js inline "$1 + $2"

To delegate to a function defined already in the target language you can omit the inline keyword and provide the function name:

extern add(x: int32, y: int32): int32
  c "add"
  js "add"

If you need access to Koka's context parameter in your external definition, prefix the function name with “kk_” as follows:

extern kk_add(x: int32, y: int32): int32
  c "kk_add"
  js "kk_add"

In your C code you would then need to provide a function matching the number of arguments and types but with an additional kk_context_t parameter:

int32_t kk_add(int32_t x, int32_t y, kk_context_t ctx) {
  return x + y;
}

Note that you should always use int32 or int64 in Koka for C interop, as Koka int is arbitrary precision and not compatible with C's int.

To include external files use extern import and provide the path to the file. For example, the following code includes the file my_file.h (relative to the current file) for the C/Wasm backends and my_file.js for the Javascript backend.

extern import
  c file "my_file.h"
  js file "my_file.js"

To include both a “.h” and “.c” file for the C backend, just omit the file extension:

extern import
  c file "my_file"

To control where it get's placed in the generated code, you can use the header-file or header-end-file special identifiers instead of file.

To use koka's closures in C, you can use the kk_function_t type:

extern kk_closure(f: () -> int32): int32
  c "kk_closure"

int32_t kk_closure(kk_function_t f, kk_context_t _ctx) {
  // The signature of the kk_function_call macro is
  // return type, (arg types), closure, (arguments), context
  // Ensure that the closure always has a reference to itself as first argument, and the context as last argument
  return kk_function_call(int32_t, (kk_function_t, kk_context_t), f, (f, _ctx), _ctx);
}

1.4. Best Practices

• utf8
• tests
• vectors
• implicits versus effects
• formatting

1.4.1. Effects

Always use the most restricted operation type in handler definitions. For example, you can use fun for an operator even if the effect definition allows ctl operations.

1.4.2. Implicits Versus Effects

1.5. Some Known Rough Edges

1.5.1. Partial Type Checking

1.5.2. Standard Library

Documentation

Testing Library

Red Black Tree

List / Ssslice

Tuple accessors on parameters

1.5.3. Conditional Effects

1.6. Other Doc Updates

Here are some updates to pre-existing Koka documentation, including a few small updates to the fip section highlighting some of the new keywords.

1.7. FBIP: Functional but In-Place

With Perceus[??] reuse analysis we can write algorithms that dynamically adapt to use in-place mutation when possible (and use copying when used persistently). Importantly, you can rely on this optimization happening, e.g. see the match patterns and pair them to same-sized constructors in each branch.

This style of programming leads to a new paradigm that we call FBIP: “functional but in place”. Just like tail-call optimization lets us describe loops in terms of regular function calls, reuse analysis lets us describe in-place mutating imperative algorithms in a purely functional way (and get persistence as well).

Koka has a few keywords for guaranteeing that a function is optimized by the compiler.

The fip keyword is the most restrictive and guarantees that a function is fully optimized by the compiler to use in-place mutation when possible. Higher order functions, or other variables used multiple times in a fip function must be marked as borrowed using the ^ prefix on their name (eg. ^f). Borrowed parameters cannot be passed as owned parameters to functions or constructors, cannot be matched destructively, and cannot be returned.

The tail keyword guarantees that a function is tail-recursive. These functions will not use stack space.

The fbip keyword guarantees that a function is optimized by the compiler to use in-place mutation when possible. However, unlike fip, fbip allows for deallocation, and also allows for non tail calls, which means these functions can use non-constant stack space.

Both fip and fbip can allow for a constant amount of allocation using fip(n) or fbip(n) where n is the number of constructor allocations allowed. This allows them to be used in insertion functions for datastructures, where at least one constructor for the inserted element is necessary.

Following are a few examples of the techniques of FBIP in action. For more information about the restrictions for fip and the new keywords, see the recent papers: [Lorenzen et al. [4];@Lorenzen:fip-t]

1.7.1. Tree Rebalancing

As an example, consider insertion into a red-black tree [1]. A polymorphic version of this example is part of the samples[??] directory when you have installed Koka and can be loaded as :l samples/basic/rbtree[??]. We define red-black trees as:

type color
  Red
  Black

type tree
  Leaf
  Node(color: color, left: tree, key: int, value: bool, right: tree)

The red-black tree has the invariant that the number of black nodes from the root to any of the leaves is the same, and that a red node is never a parent of red node. Together this ensures that the trees are always balanced. When inserting nodes, the invariants need to be maintained by rebalancing the nodes when needed. Okasaki's algorithm [8] implements this elegantly and functionally:

fbip(1) fun balance-left( l : tree, k : int, v : bool, r : tree ): tree
  match l
    Node(_, Node(Red, lx, kx, vx, rx), ky, vy, ry)
      -> Node(Red, Node(Black, lx, kx, vx, rx), ky, vy, Node(Black, ry, k, v, r))
    ...

fbip(1) fun ins( t : tree, k : int, v : bool ): tree  
  match t
    Leaf -> Node(Red, Leaf, k, v, Leaf)
    Node(Red, l, kx, vx, r)
      -> if k < kx then Node(Red, ins(l, k, v), kx, vx, r)
         ...
    Node(Black, l, kx, vx, r)
      -> if k < kx && is-red(l) then balance-left(ins(l,k,v), kx, vx, r)
         ...

The Koka compiler will inline the balance-left function. At that point, every matched Node constructor in the ins function has a corresponding Node allocation – if we consider all branches we can see that we either match one Node and allocate one, or we match three nodes deep and allocate three. Every Node is actually reused in the fast path without doing any allocations! When studying the generated code, we can see the Perceus assigns the fields in the nodes in the fast path in-place much like the usual non-persistent rebalancing algorithm in C would do.

Essentially this means that for a unique tree, the purely functional algorithm above adapts at runtime to an in-place mutating re-balancing algorithm (without any further allocation). Moreover, if we use the tree persistently [9], and the tree is shared or has shared parts, the algorithm adapts to copying exactly the shared spine of the tree (and no more), while still rebalancing in place for any unshared parts.

1.7.2. Morris Traversal

As another example of FBIP, consider mapping a function f over all elements in a binary tree in-order as shown in the tmap-inorder example:

type tree
  Tip
  Bin( left: tree, value : int, right: tree )

fbip fun tmap-inorder( t : tree, f : int -> int ) : tree
  match t
    Bin(l,x,r) -> Bin( l.tmap-inorder(f), f(x), r.tmap-inorder(f) )
    Tip        -> Tip

This is already quite efficient as all the Bin and Tip nodes are reused in-place when t is unique. However, the tmap function is not tail-recursive and thus uses as much stack space as the depth of the tree.

void inorder( tree* root, void (*f)(tree* t) ) {
  tree* cursor = root;
  while (cursor != NULL /* Tip */) {
    if (cursor->left == NULL) {
      // no left tree, go down the right
      f(cursor->value);
      cursor = cursor->right;
    } else {
      // has a left tree
      tree* pre = cursor->left;  // find the predecessor
      while(pre->right != NULL && pre->right != cursor) {
        pre = pre->right;
      }
      if (pre->right == NULL) {
        // first visit, remember to visit right tree
        pre->right = cursor;
        cursor = cursor->left;
      } else {
        // already set, restore
        f(cursor->value);
        pre->right = NULL;
        cursor = cursor->right;
      }
    }
  }
}

In 1968, Knuth posed the problem of visiting a tree in-order while using no extra stack- or heap space [3] (For readers not familiar with the problem it might be fun to try this in your favorite imperative language first and see that it is not easy to do). Since then, numerous solutions have appeared in the literature. A particularly elegant solution was proposed by Morris [7]. This is an in-place mutating algorithm that swaps pointers in the tree to “remember” which parts are unvisited. It is beyond this tutorial to give a full explanation, but a C implementation is shown here on the side. The traversal essentially uses a right-threaded tree to keep track of which nodes to visit. The algorithm is subtle, though. Since it transforms the tree into an intermediate graph, we need to state invariants over the so-called Morris loops [5] to prove its correctness.

We can derive a functional and more intuitive solution using the FBIP technique. We start by defining an explicit visitor data structure that keeps track of which parts of the tree we still need to visit. In Koka we define this data type as :visitor:

type visitor
  Done
  BinR( right:tree, value : int, visit : visitor )
  BinL( left:tree, value : int, visit : visitor )

(As an aside, Conor McBride [6] describes how we can generically derive a zipper [2] visitor for any recursive type $\mathpre{\mu \mathid{x}.~\mathid{F}}$ as a list of the derivative of that type, namely $\mathpre{\mathkw{list}~(\pdv{\mathid{x}}~\mathid{F}\mid_{\mathid{x}~=\mu \mathid{x}.\mathid{F}})}$. In our case, the algebraic representation of the inductive :tree type is $\mathpre{\mu \mathid{x}.~1~+~\mathid{x}\times \mathid{int}\times \mathid{x}~~\,\cong\,~\mu \mathid{x}.~1~+~\mathid{x}^2\times \mathid{int}}$. Calculating the derivative $\mathpre{\mathkw{list}~(\pdv{\mathid{x}}~(1~+~\mathid{x}^2\times \mathid{int})~\mid_{\mathid{x}~=~\mathid{tree}})}$ and by further simplification, we get $\mathpre{\mu \mathid{x}.~1~+~(\mathid{tree}\times \mathid{int}\times \mathid{x})~+~(\mathid{tree}\times \mathid{int}\times \mathid{x})}$, which corresponds exactly to our :visitor data type.)

We also keep track of which :direction in the tree we are going, either Up or Down the tree.

type direction
  Up
  Down

We start our traversal by going downward into the tree with an empty visitor, expressed as tmap(f, t, Done, Down):

fip fun tmap( f : int -> int, t : tree, visit : visitor, d : direction )
  match d
    Down -> match t     // going down a left spine
      Bin(l,x,r) -> tmap(f,l,BinR(r,x,visit),Down) // A
      Tip        -> tmap(f,Tip,visit,Up)           // B
    Up -> match visit   // go up through the visitor
      Done        -> t                             // C
      BinR(r,x,v) -> tmap(f,r,BinL(t,f(x),v),Down) // D
      BinL(l,x,v) -> tmap(f,Bin(l,x,t),v,Up)       // E

The key idea is that we are either Done (C), or, on going downward in a left spine we remember all the right trees we still need to visit in a BinR (A) or, going upward again (B), we remember the left tree that we just constructed as a BinL while visiting right trees (D). When we come back up (E), we restore the original tree with the result values. Note that we apply the function f to the saved value in branch D (as we visit in-order), but the functional implementation makes it easy to specify a pre-order traversal by applying f in branch A, or a post-order traversal by applying f in branch E.

Looking at each branch we can see that each Bin matches up with a BinR, each BinR with a BinL, and finally each BinL with a Bin. Since they all have the same size, if the tree is unique, each branch updates the tree nodes in-place at runtime without any allocation, where the :visitor structure is effectively overlaid over the tree nodes while traversing the tree. Since all tmap calls are tail calls, this also compiles to a tight loop and thus needs no extra stack- or heap space.

Finally, just like with re-balancing tree insertion, the algorithm as specified is still purely functional: it uses in-place updating when a unique tree is passed, but it also adapts gracefully to the persistent case where the input tree is shared, or where parts of the input tree are shared, making a single copy of those parts of the tree.