It occurred to me a few times that I have been wanting for a way to make sure a deep record type received as an argument was immutable. Something like:
type thing =
{ ... many fields with many sub-records ... }
let copy_thing (thing [@immutable]) = thing (* yes? *)
Does something similar exist already?
Or am I looking in the wrong direction?
No such thing exists at the moment, as far as I know.
I don’t think it is possible to implement in a way that does not reject a bunch of immutable types, because you can’t inspect the definition of an abstract type.
Would be very useful at present, although I think the purpose of such an annotation will be less important once we get typed effects, since, in principle, it’s less important whether a type is mutable and more important to know if an operation mutates.
But right now we don’t have either, and I also find myself wishing there was a more explicit way to reason about effects in OCaml, particularly now that we have multicore.
Typed effects won’t do that.
Thats because they are typed algebraic effects. Regular effects are still going to be available and untyped. I guess you could try to use only algebraic effects, but IMO thats very unlikely to be the dominant style across the whole ecosystem
Oh. A talk I watched some time ago mentioned that they wanted to add typed effects outside of algebraic effects, but I admit that I haven’t followed the development of typed effects closely and perhaps this information is not current. Sad to hear this, though I can imagine that it would be difficult to add it in a backward-compatible way that isn’t ugly.
How so? Can you give an example?
If you’re in a concurrent context and you want to ensure that no object that can be reached from multiple threads has any operations which mutate. You could simply enforce this at a type level.
I dont think thats the right way to solve your issue. Look up janestreet’s oxidizing ocaml blog posts, they do something that solves your issue. It more about who owns a value than what value is mutable.
Wouldn’t you normally do this with a synchronization mechanism like a mutex?
I mean, normally you wouldn’t wrap an immutable data structure in a mutex because it’s unnecessary and slows down access—but if you don’t know about hidden state, you’re in trouble.
I think I’ve read it before, but I’ll search it up again for a refresher. Thanks! I am aware of how Rust restricts mutation (only one mutable borrowing at a time), but I don’t remember how they were suggesting this might be implemented in OCaml.
But at the end of the day, what Rust is doing is encoding mutation into the type system, which is what we want.
Though note that this is modulo interior mutability. So an apparently immutable type could have a field with internal mutability buried deep inside somewhere (perhaps with dynamic checks to panic if conditions violating type safety are detected). Be careful trying to use the rust types to mean more than “rust type safety”.
Hello,
I think the classical ML way is to hide details of the type (e.g. in a module) to the part needing immutable access and use accessors for read & write access to parts you would like to modify.
Another approach is to leave your type open but make immutable fields you don’t want to be modified. If a field is not marked “mutable”, it is immutable in a record (Mutability and Imperative Control Flow · OCaml Documentation).
Does it help? Or why wouldn’t it work for your use case?
Best regards,
david
I wouldn’t presume to speak for the OP, but the reason I’d be interested in this would be to be able to reason about mutation in types I didn’t define—both in terms of constraints to client code in libraries I publish, as well as cases where I am the client using a data structure with an opaque type.
Hopefully I at least know if the types I define myself are mutable! (of course, I may still forget, and therefore these constraints could still be useful in my own code)
Indeed in the use case that triggered my question, I did create all the nested records myself but I’d still like a static check in this case because it’s simpler, more robust than me checking 50 record definitions though as many distinct compilation units, and will break in the future if/when I do turn a field mutable somewhere.
Like the tailcall anotation that I use for non trivial functions that I write myself, both to check my current assumption and to prevent me from inadvertantly breaking something in the future.