4 ms·

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

kmill 3y ago
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!)
- francasso 3y ago
  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 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 :)
aseipp 3y ago
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.

kmill 3y ago

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!)

francasso 3y ago
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 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 :)

aseipp 3y ago

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.