Perceus: Garbage Free Reference Counting with Reuse [pdf]
microsoft.com
microsoft.com
> These “scoped life-time” reference counts are used by the C++ shared_ptr⟨T⟩(calling the destructor at the end of the scope), Rust’s Rc⟨T⟩(using the Drop trait), and Nim (using a finally block to call destroy)
So Rust's non-lexical lifetimes doesn't remedy this? Meaning the actual drop of xs needing to occur at the end of the example in the beginning of section 2.2, as opposed to right after the map. I would have thought that ys borrows nothing from xs, and the drop can be inserted right after map? Perhaps it's too early in the morning for thinking for me.
Their implementation requires annotations on all functions which are effectful (throw exceptions, log to the console, etc). What wasn’t clear to me was whether or not the callers of those functions also need to be annotated, but I presume they do. If so, that’s a pretty tedious limitation. While I like explicitness, changing the signature of a deep, oft-called function (e.g. to add temporary debug logging) requires changing a lot of other code.
If so, you still might have to annotate some library functions that are implemented outside the language, but that would be it. The annotations are there for the programmer as, without them, it would be hard to keep track of which of your functions are pure, which might throw, etc.
That being said, even if your standard for synthesis is "works in practice" rather than some halting-related criterion, it's still really easy to find type systems that don't qualify. There are also sometimes practical concerns around separate compilation--if you're relying on introspection and not just interfaces for typechecking, and someone just tells you what interface will be satisfied at runtime, you won't be able to repeat this kind of analysis; the same sorts of problems occur when you perform reflection.
If the compiler can do such a check, and the number of possible annotations is finite, it can check each of them, thus computing the set of annotations that the function adheres to.
This is a problem you run into very quickly--for example, Hindley-Milner is only decidable because it will only infer "forall a" in prenex form (so its "most general" annotation is only most-general in that context). Type inference if you allow non-prenex quantification--even very mild non-prenex quantification--is undecidable, despite these being just as easy to typecheck as the prenex versions!
Now, in practice programs are made up finite numbers of terms, so for some of these type systems you could certainly come up with some sort of semidecision procedure by iterating through every possible sequence of type annotations. But as this kind of brute force algorithm will not terminate if it can't find the right set of annotations, and in practice will not terminate within human lifespans even in most cases where the right set of annotations exist, I don't think people would be very happy with such a system.
This is especially true if the only reason to find the annotations was to perform program optimizations, and not to enforce correctness. People are already wholly unwilling to give compilers unlimited amounts of time to do interprocedural analysis, which is mostly done in LLVM and such by just inlining everything. If having effect annotations were actually critical for being able to apply the optimizations from the paper (which, like I said earlier, I don't know that they are), this would pretty much be another instance of a global program rewrite too expensive for an optimizing compiler to perform in practice.
For example, to write down (not prove!) an equality between two vectors indexed by their length, at least in Coq (and other type theories without extensional equality, which is in general undecidable), you have to first show that they have the same length--otherwise the expressions are not well-typed. The length can be any well-typed term of type nat, and like I said before Coq is far more than powerful enough to express Peano arithmetic, so you can see already that synthesizing an equality type between two vectors is just as difficult as proving an equality between two natural numbers, so it is very much undecidable in general. In fact, it is quite difficult to write down in practice even in some surprisingly simple cases! The actual proof term, however, is usually something like a pattern match on some other equality followed by the creation of a function that pattern matches on another equality, etc. down the line, until it returns the unhelpful constructor `eq_refl` (which basically just says `x = x`). So all of the interesting work in such cases has transferred to the type system, with the proof term basically just there to perform type casts and coercions.
And then potentially be hooked up to a prettier plugin to adf explicit annotations if desired.
This might be one of the only benefits to monopolistic presences -- the amount of great minds in the same place, set free to mingle and create can produce amazing results when a benevolent sponsor exists and it's tunnel-visioned on profit.
I'm quite cynical towards Microsoft but I am very grateful that they publish at least some of their papers/insights and their links (to existing papers) generally don't die.
https://github.com/koka-lang/koka https://github.com/microsoft/mimalloc
“ In practice, mutable references are the main way to con- struct cyclic data. Since mutable references are uncommon in our setting, we leave the responsibility to the programmer to break cycles by explicitly clearing a reference cell that may be part of a cycle. ”
Right now I'm looking towards Nim, which has some pros and cons. I'm still not good enough to build complex APIs with it, but it's really easy to integrate. Nim feels like Python for systems programming.
A big issue is that while GC is technically optional, a lot of the standard library depends on GC (at least last time I checked) and using D without those parts of the standard library is much less ergonomic.
Compile to C include Gambit, Gerbil, and Chicken, embed include Guile, S7, Gambit. (And others I'm forgetting).
It's possible this could still be done with the described approach, but it looks much more difficult.
> Finally,Java performs best on this benchmark; we can see whilerunning the benchmark that it can run the G1 collectorfully concurrent on another core.