6.1.0890 CELLS CORE

What does "the size of -3 cells" mean?

What does -3 mean? One definition is that it is the result of a subtraction. Others are "magnitude of loss or deficiency".

You can use these (and probably other) definitions to think about negative sizes. E.g., when you subtract one address from another one, the result may be negative. When you allot a negative size, you deallocate dictionary space.

ambiguous condition on overflow

Actually, I see the text that references cells only in the description of the proposal, not in the normative part, and, OTOH, it's not obvious to me that the standard without the proposal makes overflow explicitly ambiguous. If we specify explicitly that cells wraps around, it becomes not only obvious that the result is probably not what the programmer wants, but also what the result is, which is much better than an ambiguous condition.

Concerning the stack diagram, the usual approach is to write ( n1|u1 -- n2|u2 ). If we want refined stack diagrams, I think that would be a different proposal that affects a lot of words. I don't agree that we should only specify the intersection of n and u, but if we wanted that, the stack diagram would be ( +n1 -- +n2 ).

Concerning your alternative text: it is correct, but harder to understand. Given that there has never been a question about what cells (as currently defined) means, not even for corner cases, I don't think that the alternative text is an improvement.

Thinking about it again, the alternative text (together with the 2s-complement proposal) describes exactly what happens if the result does not fit in a cell, while the current text does not, so the alternative text is more appropriate for the normative text, while the current text is appropriate for the rationale.

When does it matter? E.g., with the well-defined result for all n|u, the distributive law "+ cells is equivalent to cells swap cells +" holds, while with an ambiguous condition or a lack of definition, it does not or is at least questionable.

Cell+ and char+ are also affected. Chars, OTOH, is no longer affected, thanks to the "1 chars = 1" proposal.

Actually, I see the text that references cells only in the description of the proposal, not in the normative part, and, OTOH, it's not obvious to me that the standard without the proposal makes overflow explicitly ambiguous.

It is in 4.1.2. The omission in the proposal was mentioned by Peter Knaggs.

I don't agree that we should only specify the intersection of n and u, but if we wanted that, the stack diagram would be ( +n1 -- +n2 ).

There is a subtle point about the differences between data types and arrow types.

In Forth, data types and arrow types constitute two distinct sorts of types. Data types are inhabited by data objects, whereas arrow types are inhabited by Forth definitions. Each sort forms a bounded lattice under the subtyping relationship. Intersection and union of types are defined as the meet and join induced by the subtyping order.

Let's denote intersection of data type with the symbol "^".

The intersection of the data type n and u is +n (that is their meet) : ( n^u ) = ( +n ).

But the arrow type ( n -- n ^^ u -- u ) is not equivalent to the arrow type ( +n -- +n ), that is ( n^u -- n^u ). The type ( n -- n ^^ u -- u ) is inhabited by all and only those Forth definitions that inhabit both ( n -- n ) and ( u -- u ) arrow types.

Unlike data types, arrow types are ordered contravariantly in their argument types and covariantly in their result types. Consequently, the arrow type ( n|u -- n|u ) is a subtype of neither ( n -- n ) nor ( u -- u ). Therefore, a definition with the arrow type ( n|u -- n|u ) cannot be used in a context where ( n -- n ) is required. For example, if the word cells were assigned the type ( n|u -- n|u ), then the phrase ( d n ) cells ( n|u ) sm/rem would be formally ambiguous due to data types mismatch.