1. 29
  1. 12

    Linear typing. Rust can emulate this by a Drop impl calling some undefined extern fn. In release mode it will fail to compile if dead code elimination doesn’t clean it up.

    1. 1

      Oh, that’s a really neat trick. I might need to try that out in my code. I have a simple HTML generator class, but you need to close it to write </html> at the end (and handle the error if for example your disk is fully or the socket has disconnected). Right now I just write in the destructor and warn on errors but I would love to be able to force that people call close instead.

      Edit: Ah, this doesn’t work in my case because I want to allow automatic dropping on the error path. But a neat trick for cases like in the article where you absolutely need to clean something up.

      1. 1

        Might be important to note that the totally safe mem::forget can prevent all Drops from being called.

      2. 6

        This sounds like linear typing, where values must be consumed exactly once (rather than at most once with affine types)

        I really like the rephrasing of C++’s RAII here:

        C++’s “RAII” […] automatically calls a zero-argument non-returning function (often called a “destructor”) just before we destroy an object

        1. 1

          I agree that this is useful but I don’t see that it is different from normal C++ RAII. For example, things like std::lock_guard / std::unique_lock use the destructor to provide scoped locks. If I have a field protected by a lock then I normally make it private and add a method that returns a std::lock_guard and a reference to the field. You call it like this:

          auto [guard, thingy] = obj.getThingy();

          Both guard and thingy have the same scope and so the lock is automatically dropped when the object that it’s protecting goes out of scope. After inlining, the compiler lowers this to the equivalent of explicitly writing:


          LLVM’s error classes do exactly what the article describes in one of the Higher RAII examples in Vale: The accessors set a flag indicating that you’ve checked the error, the destructor kills the program if you haven’t. This means that, even in non-error dynamic execution traces, you must check the error. C++ RAII includes a great many things like this.

          The second example is implementing a weak reference (the map holds a reference that goes away when the object goes away). C++‘s std::weak_ref provides this on top of a reference-counted object abstraction (there’s no weak-reference abstraction for std::unique_ptr, though one would be useful) and this is built on top of C++ RAII.

          1. 5

            The fact that it moves the “did you call the consuming function?” check from run time to compile time is neat.

            1. 1

              Regarding weak references, wouldn’t the entry with the weak pointer to something expired still exist in the table after the object it pointed to is destructed? It seems like that’s the benefit of this feature in Vale, it’s a compile-time reminder to implement the table cleanup in the article’s use case.

              1. 1

                Weak references are an off-the-shelf construct that’s built on top of RAII. You can implement your own thing that handles removal. I don’t really like the ‘error when the programmer does the wrong thing’ model when the alternative is to make it impossible to express the wrong thing. If you can check that everything that deletes something removes it from a collection then you can simply remove it and reduce the cognitive load on the programmer.

                I do agree that compile-time reminders are nice but they depend a lot dataflow analysis in the compiler and that isn’t possible in the general case.