> Effects would retain the qualifiers "io" and "unsafe". Users could continue
> to lie about the effect of a function using "auth" clauses in the crate file.
> Writing to a non-local mutable field would be considered an io action for the
> sake of effect calculation -- after all, mutating a PRNG is more or less
> observationally indistinguishable from "doing IO" -- but effects would
> strictly describe *code*, not data. If you make a function into a first class
> value, of course, that value will have a function type and that function type
> will have an effect. But the type as a whole won't have an effect; only a
> function has an effect, and the effect occurs when you *call* the function.
> You can pass the type around all you want without worrying about its effect.
> Effect checking would remain useful for helping users enforce purity and
> safety in their code, of course.
I think what you're describing here is roughly the difference between saying
"types have effects" and "function types have effects". In the effect system
literature, effects are placed above the arrow of a function type to indicate
this distinction, e.g.:
io
int --> bool
It sounds right to me that effects are a property of function and method types,
rather than all types.
And IIUC, it sounds like the other concept you're introducing, which is a
property of all types, is something like a memory storage classifier, and a
property of all types. Yes?
> ...users would not be allowed to lie about the stratum of a type. This is
> important, because as it stands presently the ability to lie about state
> means that *everything* that touches a mis-classified stateful value is not
> only "likely unsafe" (in the "crash the system" sense) but also very
> difficult -- almost impossible -- to make safe: you would have to co-ordinate
> with every other reader and writer in manipulating refcounts and
> malloc/realloc/free actions, and ensure that everyone agreed on statefulness
> any time critical combinations of those actions occurred. This is not
> something likely achievable on a whole-program basis.
This sounds right to me. Rust isn't about disallowing all unsafe constructs,
it's about keeping them in a reasonably well-contained box.
> Part #2 of the proposal is a bit juicier: add a third stratum back in, "gc".
> We had this briefly a year or so ago, called "cyclic" back then, but I think
> "gc" is a pithier qualifier. We merged the concept into "state" when devising
> the current effect system, but I suspect that was a mistake.
>
> Under proposal-part-#2, the state and gc strata would both still be
> task-local, but splitting state from gc would have three interesting
> implications:
>
> - State values could be frozen and thawed, reasonably, to and from
> stateless values. State means acyclic-and-mutable, after all, so
> in the singly-referenced case this would even wind up a no-op. This
> is the easy case of freeze/thaw, and it'd be formally denoted in
> the type system. This would provide a great utility for two idioms
> we currently have no good way to support: freeze-and-apply-predicate
> and freeze-and-transmit-over-channel.
I've been meaning to ask about freeze and thaw. Both of them require some kind
of restriction to be safe, and I was wondering what you had in mind. In
particular:
- I think typestate can ensure that after you freeze something, you don't make
local mutations to it, but how do you enforce that you haven't leaked the alias
to someone non-local who might retain a mutable view of the data?
- Similarly, if non-local code has references to something immutable and you
thaw it, their belief that the data is immutable is violated.
If you do have restrictions in mind that make these operations safe, in what
situations can you usefully use freeze and thaw?
As for the idioms you mention, the second one sounds compelling, but I'm not
sure about the freeze-and-apply-predicate. That seems sort of question-begging
-- the only reason you'd use freeze-and-apply-predicate is if you were already
going to freeze anyway, because you were all done mutating the data.
> - State values could also have a our structural comparison definition
> extended to them. Again, acyclicality wins here.[2]
Same question as Patrick: how do you enforce acyclic stateful types?
> - State objects could have destructors. Acyclicality, again. Yay!
> No more telling users to make artificial immutable sub-objects :)
Ditto Patrick again: sounds good, if you really can enforce lack of cycles.
> [1] Does anyone have a better term than "stratum" to describe the storage
> category of a type? I'm almost partial to "heap" or "pool", but that is both
> slightly misleading and also makes for sentences with strange grammar: "the
> heap of a type". Yuck.
Stratum is pretty stilted, yeah. No brilliant ideas ATM, though.
> [2] we could even extend comparison to gc types if we say "gc types are
> compared by address". It would be a little unpredictable though; I'm tempted
> to define a "std.util.addrcmp[gc T](&T a, &T b) -> order" that compares
> anything by address, along with a memcmp that compares by memory-content, and
> make the "built-in" operators <, =, etc. structural on acyclic types and
> errors when applied to a gc type. Safer, no?
What would == do for gc types? Fail dynamically? Fail to type check?
Dave
_______________________________________________
Rust-dev mailing list
[email protected]
https://mail.mozilla.org/listinfo/rust-dev
