r/ProgrammingLanguages • u/RishabhRD • 6d ago
Safe Systems-programming with Mutable Value Semantics | Dave Abrahams | Keynote at IWACO 2026
https://youtu.be/op51SyyPJmw?si=P5QH6M8Hdf4_CUUZ3
u/tmzem 5d ago
The basic idea of value semantics is simple and easy to understand and reason about. However, the main issue are stored references/projections, which are necessary for many common patterns that project parts of an object/collection in a more general way:
Indexing-like operations that might fail: index_at(inout Container, let Index) -> Optional<inout Value>
Failable operations that might return projections: append_within_capacity(inout ArrayList<T>, sink T) -> Result<inout T, sink T>
Generalized slices: split_at_inout(inout ArrayList<T>, at_index: Int) -> Pair<ListSlice<T, inout>>
Any kind of iterators and iterator-adapters
Map entries returned from map data structure subscripts and map iterators need to be able to have stored projections: KeyValuePair<let K, inout V>
Rust also allows more complex patterns by allowing multiples paths/lifetimes per user-defined type, but those are rarely used and there is probably some explorable design space (or patterns) to do those cases in a simpler way.
2
u/processeus1 5d ago
Great examples, thanks a lot for the thoughts!
> Indexing-like operations that might fail: index_at(inout Container, let Index) -> Optional<inout Value>
If the operation might not yield an element, then instead of wrapping the reference into an optional, we can just simply not yield anything. We can extend the subscript ABI with a boolean flag that indicates whether the callee yielded anything, and we can require the caller to pattern match that if they want to use the result.
```hylo
subscript min(a: inout Int, b: inout Int) inout? -> Int {
if a < b { yield &a }
else if b < a { yield &b }
}
fun main() {
var (a, b) = (1, 3)
if let m ?= min[&a, &b] {
&m += 1
} // else no value yielded
print(a, b)
}
```> Failable operations that might return projections: append_within_capacity(inout ArrayList<T>, sink T) -> Result<inout T, sink T>
This is pretty interesting, and I don't immediately see a better way to handle that than asking the function to move the object into the returned result. `sink` in, independently stored value out. Otherwise, you have to introduce lifetime dependencies and things get complicated. Do you have use cases where moving the result would be inappropriate?
> - Generalized slices: split_at_inout(inout ArrayList<T>, at_index: Int) -> Pair<ListSlice<T, inout>>
> - Map entries returned from map data structure subscripts and map iterators need to be able to have stored projections: KeyValuePair<let K, inout V>These are both examples of yielding more than one elements at once. We were thinking of allowing to yield a tuple of projections. We should be careful though, because unless we do something special, yielding the tuple `{T, U}` would look just like yielding a single object-a whole, so we would either need to mark the elements as remote parts (value-semantic references), or indicate that this is not a regular tuple but a tuple of projections. The latter version I could by not having a special tuple in the type system, just part of the signature of a function/subscript - The same way a function can have multiple parameters with different conventions, it should be possible to have a subscript with a list of yielded bindings:
A dummy example:
```hylo
subscript entry<K, V>(xs: inout ArrayList<K, V>, at key: K) -> let K, inout V {
let i = xs.keys(key)
inout v = xs.values[i]
yield k, &v
}
```> Any kind of iterators and iterator-adapters
As far as I know, index based APIs can go pretty far, but these are I think the most challenging to design. u/RishabhRD, could you summarize our ongoing designs or link some discussions on this topic?
4
u/NomagnoIsNotDead 6d ago
I'm no experienced programming language theory person, but in my opinion the way Hylo is being presented doesn't do it justice, please correct me if what I'm about to say is somehow not the main focus of the language. The presentation spends most of the time speaking about value semantics when most programmers know what it is intuitively, and the website puts the emphasis on features that are kind of secondary and present in many other languages. What neither the presentation nor the site put in the forefront is 'but how does Hylo make mutable value semantics USABLE and PERFORMANT?'. After looking into Hylo, it genuinely blows all other languages out of the water a this! I advise a marketing strategy change, basically.
Let me explain it as best as I can. Take a look at the language's website and the examples as this explanation is meant to help get up to speed faster, also this is just my understanding. https://hylo-lang.org/
Hylo is linearly typed, meaning all values must be produced and consumed exactly once. Since it has no references, you may call the .copy() method for guaranteed deep copies of any object, allowing you to 'circumvent' the limitation when needed.
Functions either produce nothing (void return type) or produce something. The arguments can be read-only and not consumed (no keyword), moved into the function and consumed (sink keyword), produced/initialized 'by-reference' with a compilation error if the parameter was already initialized (set keyword), or modified in-place (inout keyword)
By default, as in with all linear typing, types can not simply drop out of a scope, which is annoying. You can make a type implement the empty Deinitializable trait to fix this. Type can also have 'sink' methods which consume the very value it is called on, and 'inout' methods to modify it imperatively. So, if a type is not Deinitializable, you either have to explicitly consume it, or call a cleanup method. Which means resource handling for e.g. memory allocation and files is safe by default, without needing to resort to lifetime analysis. There's also an empty Movable trait which I think has to be implemented to allow a type to be modified in-place by an 'inout' method/'inout' function argument, meaning locality is also guaranteed by default. I believe with this combination of restrictions, the only type checking you'd need to ensure no aliasing is only verifying that you don't pass the same variable twice to a function call that contains 'inout' arguments, which would go against the spirit of linear typing anyways. Also, mutation (assignment) has to be explicitly marked with an ampersand like this: '&var = val;' which helps visualize mutation points.
Overall, I think this is genius! This is an extremely simple to implement type system that provides a wild amount of safety and is pretty comfortable. And the breakthrough is somehow just removing references at the type level.
7
u/dabrahams 5d ago edited 5d ago
u/NomagnoIsNotDead thanks for your thoughts!
Keep in mind that the talk was for an academic conference, where using a term like “value semantics” without a clear definition (either in commonly-known literature or given in the talk) is… not done. But I think you might be surprised at how deeply inadequate ”most programmers'“ understanding of value semantics is. These days “most programmers” who aren't just doing HTML/CSS are working in JavaScript and Python, where value semantics for user-defined types isn't even possible. I can tell you from personal experience that at least some Python programmers have an incredibly hard time even imagining a world without reference semantics.
What neither the presentation nor the site put in the forefront is 'but how does Hylo make mutable value semantics USABLE and PERFORMANT?'. After looking into Hylo, it genuinely blows all other languages out of the water a this!
That's very kind of you to say; we have paid a lot of attention to usability and performance. But have you looked at Swift? The fundamental design elements Hylo uses to do that are present there.
Hylo is linearly typed, meaning all values must be produced and consumed exactly once.
Well, I would say all objects are produced and consumed exactly once (I can produce an object with the value 5 any number of times). But I don't think that makes it different from almost any other language, other than those that let you produce objects and leak them without any eventual consumption.
Since it has no references, you may call the .copy() method for guaranteed deep copies of any object, allowing you to 'circumvent' the limitation when needed.
Not… exactly.
First, if I may pick a nit, there's no such thing as a “deep” or “shallow”
copyoperation. There's justcopy(), which returns an object with an equivalent and independent value. That's one of the important insights that comes from understanding value semantics well (See §2.4 of this paper for more detail).Secondly, Hylo doesn't have a classical strict linear type system: while objects can only be consumed once you can access them for reading or for in-place mutation using
letandinoutbindings respectively. If you want to complicate your mental model you can think of those bindings as references but we feel justified in saying Hylo doesn't have references, since they don't create reference semantics, can't be stored or returned, and can be understood using a much simpler mental model. The point here is that the usual limitation of strict linear type systems is already circumvented before copying enters the picture. Also, non-copyable types are “a thing” so that's not always available.(Minor point: passing an initialized object as a
setparameter is fine as long as it isDeinitializable. The compiler will deinitialize it implicitly if necessary).By default, as in with all linear typing, types can not simply drop out of a scope, which is annoying. You can make a type implement the empty
Deinitializabletrait to fix this.It's not empty; it has a
fun deinit() sinkrequirement with a default implementation.x.deinit()gets called implicitly at the first opportunity on everyxin local storage that hasn't already been consumed. You need a place to release memory, for example.So, if a type is not
Deinitializable, you either have to explicitly consume it, or call a cleanup method. Which means resource handling for e.g. memory allocation and files is safe by default, without needing to resort to lifetime analysis.It seems to me the ability to have deinitialization (whether via
deinit()or other consuming methods) release resources exists in many mainstream languages and is not very remarkable. As far as I can tell, the only reason to have a non-Deinitializabletype withsinkmethods is so you can force an instance to be united with some other value. That pattern can be useful, but in marginal cases, and if safety depends on it, usually must be accompanied by a runtime check since we don't have a dependent type system. Please let me know if I'm missing something.There's also an empty
Movabletrait which I think has to be implemented to allow a type to be modified in-place by an 'inout' method/'inout' function argument, meaning locality is also guaranteed by default.
Movableisn't empty; its requirement is a method bundlefun take_value(from source: sink Self) auto { set inout }.Movableconformance is not needed forinoutbinding/parameter passing; it's only required for implicitly re-seating a value into a new piece of memory (or returning it, although we're not sure whether to keep that tied toMovableconformance). I don't know what you mean by “locality” in this context. Care to elaborate?I believe with this combination of restrictions, the only type checking you'd need to ensure no aliasing is only verifying that you don't pass the same variable twice to a function call that contains
inoutarguments, which would go against the spirit of linear typing anyways.Upholding the Law Of Exclusivity is not quite as simple as that in practice. For a trivial example, you have to prohibit
swap(&x[0], &x[1]). Dimi and I wrote a paper about how it all works (and she gave a very nice talk) if you want the details.I think this is genius! This is an extremely simple to implement type system that provides a wild amount of safety and is pretty comfortable. And the breakthrough is somehow just removing references at the type level.
If we've made the right bets with our design, then you are right! If not, it's back to the drawing board ;-) We are excited to get the implementation to the point where we can prove/disprove that the system lets us express all the things we think are important.
1
u/NomagnoIsNotDead 5d ago
Thanks for the detailed reply! I did miss quite a few things
It seems to me the ability to have deinitialization (whether via
deinit()or other consuming methods) release resources exists in many mainstream languages and is not very remarkable. As far as I can tell, the only reason to have a non-Deinitializabletype withsinkmethods is so you can force an instance to be united with some other value. That pattern can be useful, but in marginal cases, and if safety depends on it, usually must be accompanied by a runtime check since we don't have a dependent type system. Please let me know if I'm missing something.Well, I'm not a fan of RAII-style destruction, but the thing I like with the current set-up is you can force deinitialization to be handled explicitly (where you can even require parameters I guess which is interesting!), or you can make it be handled automatically, and the type system takes care of both equally well. Also, I'm not sure how I feel about set-parameters being capable of deinitializing variables. That might create unexpected side-effects, not all data can be constructed and destructed 'almost for free', so maybe it should not be possible to accidentally/implicitly 'reinitialize' a piece of data, maybe a distinct Reinitializable trait associated to this behaviour would be safer. I'm talking about system calls or even interfaces to external hardware.
Movableisn't empty; its requirement is a method bundlefun take_value(from source: sink Self) auto { set inout }.Movableconformance is not needed forinoutbinding/parameter passing; it's only required for implicitly re-seating a value into a new piece of memory (or returning it, although we're not sure whether to keep that tied toMovableconformance). I don't know what you mean by “locality” in this context. Care to elaborate?Makes sense. So basically, Movable is similar to the implicit-copy trait I'm reading about in the Hylo docs, where it just allows a type to be used less verbosely. It would be nice if this wasn't needed to return values, indeed. After taking a more thorough look at the hylo docs, this part of my understanding was just a bit confused overall. I believe the main thing I missed is the different kinds of bindings: let, var, and specifically inout, which is... basically a stored reference that you can't store in a data structure. In my opinion, it would be better if inout was just available as a keyword for function parameters, and references were relegated to function interfaces. This would practically force writing in a style that preserves locality of reasoning, where code that does spooky action at a distance has a clear interface and can't be sprinkled in wherever.
Thanks for you and everyone else's work! I'll be trying out the language, this has opened up my eyes quite a bit as to how to achieve safety in an unexpected way, and linear (or 'linear-in-spirit') type systems are such an area of interest in recent years for a reason, they're just delicious.
3
u/dabrahams 5d ago
Whoa there, pardner! As noted in the talk, we don't have and don't want an implicit-copy trait (similar to Rust's `Copy`). We've discussed having an `@implicitcopy` directive that allows you to say copies should happen implicitly, for prototyping, scripting, etc.
And copying and moving are completely orthogonal operations, so I'm not sure what the connection is.
In my opinion, it would be better if inout was just available as a keyword for function parameters,
Local bindings and function parameters are intimately related; you can almost express one in terms of the other and making that different for inout would make the language less uniform. I don't think prohibiting a local
inoutchanges much other than to make some things less convenient. I would then just writemodify(&x.y, fun (y) { ... })and have a local bindingyinside the lambda.Spooky action at a distance is not “all mutation.” The point of MVS is that you can't write any code that does spooky action at a distance—as we define it—in the safe core language subset. Of course people will define things like Rust's `RefCell` using unsafe code and subvert that, and once they do, the properties of the core language can't force the spooky action to be visible in interfaces.
0
u/y0shii3 5d ago
It fascinates me how people are so scared of aliasing and use-after-free bugs that an entire genre of programming languages has sprung up with the common goal of creating just the right abstractions to make such bugs theoretically impossible.
1
u/4SlideRule 4d ago
Why? Use after free bugs are common enough and bad enough, but aliasing bugs are very common and can be quite vexatious to track down in complex code. What could be more natural than to try to categorically exclude them?
6
u/processeus1 6d ago
I'd be curious to hear if anyone has use cases where saved references are necessary and cannot be replaced with another design pattern using value semantics without significant loss of efficiency or correctness safeguards.
As a starter: one example would be to project an optional out of a map to access its element at a key, but we can fix that issue with subscripts that yield 0 or 1 times, and allowing the caller to directly pattern match on the result. This works, because we don't need to save the "optional" for longer period.