Comment by jcparkyn

13 hours ago

Thanks, some interesting reading there that I will check out (I wasn't aware of PCF). Perhaps I should've used more precise wording: "All types are value types".

> Standard ML [...] It has all you dream of and more

The main thing here that's missing in Standard ML (and most other functional languages) is the "mutable" part of "mutable value semantics" - i.e., the ability to modify variables in-place (even nested parts of complex structures) without affecting copies. This is different from "shadowing" a binding with a different value, since it works in loops etc.

1 comment

jcparkyn

throwaway17_17 7 hours ago

Quick note then a more wordy response (and after being dinged in another thread yesterday, the tl;dr is your usage is correct, ignore purposely avoiding context criticism of wording):

SML has mutation, but only for Ref Cells, which humorously are values themselves. Not that’s what you’re really talking about here.

Now for the wordy part…

As another of your sibling commenters said GP was being incredibly pedantic. While his reference to Plotkin/Winskel and the PCF thread of research is formative, it is of particular note for Structural Operational Semantics.

The real issue GP is raising that in programming language semantics there are two distinct ways in which the term ‘value’ is used. Worse still is that the terms are not just distinct but are broadly from two very distinct fields in PLT. So, what are the two uses:

  1) when the domain of discourse is Operational Semantics of Programming Languages, a ‘value’ is a term in the formal abstract syntax of the language which is not subject to reduction via any other transition defined over the syntax;

  2) when the domain of discourse is the Evaluation and Default Kinds of arguments passed to functions and the semantic implications of those defaults, a ‘value’ is defined in the negative as those semantic objects which ARE NOT references [1];

which from the definitions alone, it is clear your designation of your language as ‘pass-by-value’ is a distinct thing from GP’s usage of the term.

While GP’s usage of ‘value’ is in line with a long standing tradition, that tradition is firmly within the academic/functional programming language syntax and semantics sphere. Your usage, as is PLAINLY APPARENT from context, is absolutely correct and in line with long standing usage within discussion (and academic work) on imperative (and otherwise non-functional) programming language semantics. So keep phrasing discussions about Herd using the ‘pass-by-value’ and ‘everything is a value’. It’s not only contextually correct and historically justified, it is utterly within the ‘vernacular’ of normal programming language discussions.

One last thought, your language’s adoption of totally defaulting to passing arguments (to functions, threads, basically any control construct), with copy-on-write being an optimization only, should make implementing a non-reified linearity qualifier on types relatively simple to implement, that would address some of the locking anti-optimizations and address some of your static analysis that you mentioned where not working 100%.

———————

1: Reference here include Rust/C++ style lightly abstracted references, nearly zero abstraction pointers, and then the references as discussed when talking about Python, Ruby, JavaScript, C++ smart pointers, Rust’s higher level abstractions over references, etc which are a very abstract concept of reference.