FP2: Fully In-Place Functional Programming [pdf]

This paper was published in May, but it doesn't look like Koka's had much acitivity for about a year now (based on Github). Any idea if Koka's still in development?

I stopped monitoring roc after feldman's early youtube chats, but it seems evolving in term of team size.

I don't really mind Roc-lang not being mentioned since Koka is referenced with its novel idea of functional-but-in-place and Perceus Reference Counting which are the theoretical basis of Roc's implementation[0]. So it doesn't really bring anything theoretically unique to the table in comparison, although I'm interested in Roc as a practical language because of this too.

[0] Ctrl-f "Perceus" on the following page and you will see a paper about Koka mentioned. https://www.roc-lang.org/

In-place mutation in a functional language dates back as far as 1994, when it was introduced for Clean in the paper 'Guaranteeing safe destructive updates through a type system with uniqueness information for graphs'[1]. The FP2 paper references a subsequent 1995 paper from the same authors, 'Uniqueness Type Inference'[2].

More publications about Clean here: https://clean.cs.ru.nl/Publications

[1] http://www.mbsd.cs.ru.nl/publications/papers/1994/smes94-gua...

[2] http://www.mbsd.cs.ru.nl/publications/papers/1995/bare95-uni...

Lean 4 uses FBIP, but it looks like this paper is about something called FIP, which is related but about guaranteeing there are no allocations or deallocations. FBIP as I understand it is more about being able write functional code in a natural away while avoiding allocations or deallocations.

(I agree about Lean 4 as becoming a great general purpose language though!)

The two things, Perseus and what Daan calls "FIP" here are a bit apples/oranges. But they are very related. FBIP/Perseus is an algorithm for efficient reference counting with reuse. "FIP" is actually a calculus (and thus a class of programs) for which you can guarantee in place updates. It's like the difference between an interface and an implementation of that interface. Perseus is an algorithm (implementation), FIP is a calculus (interface which can be implemented multiple ways.)

So yes, Lean 4 does use "FBIP", but "FBIP" is sort of more like an evaluation/compilation strategy, it's not any one algorithm or specific semantics. To be more precise, Lean uses Perseus, which basically has the insight "if an object's refcount is 1, I can do an in place update." You could say FIP is the natural evolution from taking a specific algorithm -- Perseus -- and sort of taking it and thinking about it from a language design POV. Perseus is the dynamic runtime implementation of FIP. But the calculus also has a static approach, too, which the paper describes using a uniqueness-typing algorithm.

These things do influence the language directly and are visible to programmers, so I don't think it's fair to say Lean 4 uses the FIP calculus described in this specific paper. For example, this semantic calculus is going to be user-visible in the next release of Koka; you'll be able to annotate functions as 'fip' or 'fbip' where the compiler will do linearity checks on the given function to guarantee that it doesn't use stack space, without needing the code generator to insert the dynamic reference counting checks required by Perseus. This also requires a notion of second-order function, stack space, etc. So it's not just some implementation detail, this is something Lean 4 would need to go out of their way to support and design for users.

I'm sorry, I think I missed your point. The paper is focused on a language that can do fully in-place FP for a broad class of programs, with the checks done at compile-time.

I believe jq code is interpreted, so while it might be able to mutate some values in place, that doesn't mean the interpreter wouldn't allocate and release memory.

Constant folding means you calculate the result of an expression at compile time.

In-place updating means you re-use the memory location of an earlier variable that's not needed anymore. Simple example in pseudo-C:

  BigInt increment_twice(const BigInt x) {
      const BigInt y = x + 1;
      const BigInt z = y + 1;
      return z;
  }

There are no compile-time constant expressions that could be folded here. But since y is not used after z is assigned, we can re-use the memory location of y for the memory location of z.

And if the caller is not using the argument after the function returns, the memory location of the argument can be used to store the return value. This means the function call does not need to allocate memory at all, not even on the stack.