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?
> yes! Currently the active development is in dev-fbip, see also our recent tech report:
https://www.microsoft.com/en-us/research/publication/fp2-ful...
We hope to put out a fresh release after the POPL deadline (Jul 11) that will include the new fip keyword and other goodies.
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].
This is also used in Lean 4, which as it turns out is not just great for math proofs, but is also becoming a great general purpose programming language
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.
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!)
I'm sure the details are different, but the general idea, to me, seems the same as the one descibed by Leo and Sebastian in https://arxiv.org/abs/1908.05647. Both Koka and Lean 4 use reference counting to know if it's safe to reuse a structure.
This paper (Daan is a collegue of Leo at MS Research) gives a different formalization and proofs. The file is still named "fbip.pdf" though :)
Interesting article, I wonder if FIP procedures could be useful even in non functional oriented languages as a safer means of reusing allocations (in languages that support reference counting or ownership?).
Noob question: the Top type here is exactly the Node constructor of the stree type. It seems useful to declare a type that is “this ADT, but limited to these constructors”, but even Haskell seems to avoid it. Why?
I mean, `jq` does in-place mutations when the values being mutated have just one reference. With a lot of care one can really make that shine. `jq` has been doing this since day 1, years ago, though it's had a few bugs in `reduce` that had to get fixed.
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.
The paper is about trying to statically analyze this. As I understand it, fip-annotated functions are ones that are checked to neither allocate nor deallocate.
