Should stack descriptions document THROW?

[SirWumpus]

I'm curious what the convention is, should words document in some fashion that they THROW? Not necessarily every possible code, maybe just document the non-standard ones. Maybe a summary as part of the stack description, eg. WRITE-FILE ( caddr u fd -- ior T) or foo ( i*x -- j*x )(T: 1, 2, 3).

[alextangent]

No, since : oops -1234 throw ;: foo oops ;: bar foo ;foo and bar don’t throw but executing them will get you a throw. Sent from my iPhoneOn 6 Sep 2024, at 17:36, Anthony Howe ***@***.***> wrote: I'm curious what the convention is, should words document in some fashion that they THROW? Not necessarily every possible code, maybe just document the non-standard ones. Maybe a summary as part of the stack description, eg. WRITE-FILE ( caddr u fd -- ior T) or foo ( i*x -- j*x )(T: 1, 2, 3). —Reply to this email directly, view it on GitHub, or unsubscribe.You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[ruv]

The standard stack notation says nothing about throw.
See also my post: "ABNF for standard stack notation".

I think we could introduce a notation for cases where control is intentionally not transferred to the point just after the word. Personally, I already use such a notation.

Bottom type

In theory, there exists a notion of bottom type, as Wikipedia says:

[...] the bottom type of a type system is the type that is a subtype of all other types.

Where such a type exists, it is often represented with the up tack (⊥) symbol.

When the bottom type is uninhabited, a function whose return type is bottom cannot return any value, not even the lone value of a unit type.

Bottom type in the stack notation

The bottom type can be employed in the stack notation to describe a case when a Forth definition (or its some semantics) does not return control to the caller, or control is not transferred to a point just after the point where the corresponding semantics are performed.

Note that under some conditions any Forth word might not return control. For example, if the user presses Ctrl+C, control may be transferred to the nearest catch, or to a special error handler, or the process may simply terminates. Therefore, there is no any sense to document such cases in stack diagrams of all words.

Also, we should not describe behavior under ambiguous conditions. For example, if an input stack parameter for some word has an incorrect type — it's an ambiguous condition. If the system throws an exception and some caller will not get control back — we should not document this.

We should describe only the cases when a Forth definition intentionally does not return control to the caller.

For example:

• exit Run-time: ( R: nest-sys -- ) ( -- ⊥ )
• throw Execution: ( 0 -- | S: i*x x\0 -- ⊥ R: j*x -- )
• if Run-time: ( x\0 -- | 0 -- ⊥ )
• while Run-time: ( x\0 -- | 0 -- ⊥ )
• until Run-time: ( x\0 -- | 0 -- ⊥ )

A user-defined word:

: ?exit ( run-time:  0 --  |   S: x\0 -- ⊥  R: nest-sys -- )
  postpone if postpone exit postpone then
; immediate

NB: x\0 means the difference between the data type x and the singleton data type {0}.

[SirWumpus]

I dislike ASCII-art glyph _|_ for this purpose, because it is close to "|" and "_" that are used (or can be used) separately in a stack diagram, producing worse readability, e.g.: ( 0 -- _|_ | nz -- nz ) .

Agreed.

Please let me know if you have any arguments or better options.

A simple _ for "blank"? For example QUIT ( -- ) (R: i*x -- _ ) ABORT ( i*x -- _ )(F: k*x -- _ )( R: j*x -- _ ) BYE ( -- _ ) FOO ( x -- | _ )

[ruv]

When a word does not return control to the caller, it probably consumes some parameters from the return stack. Then, should we specify data types for parameters on the return stack when we specify "never" for the type of output tuple on the data stack?

Some examples:

• The word exit (the run-time semantics of):

  • the top parameter on the return stack shall be nest-sys, so it shall be specified;
  • correct stack diagrams:
    • ( -- never ) ( R: nest-sys -- )
    • ( -- never ) ( R: nest-sys -- never ) (this is better because the specified data type in the second diagram has fewer members)
    • ( S: -- never R: nest-sys -- ) (two stacks in one diagram; never for output in any stack implies never for output in all other stacks too).

• The word throw (the execution semantics of):

  • parameters on the return stack does not matter, so it is not necessary to specify them;
  • correct stack diagrams:
    • ( 0 -- | nz -- never )
    • ( S: 0 -- | S: nz -- never R: i*x -- ) (this is longer, and it does not impose any additional restrictions comparing to the above variant)

Where nz = x\0 ; nz ⇒ x.

[ruv]

@SirWumpus wrote:

A simple _ for "blank"? For example QUIT ( -- ) (R: i*x -- _ ) ABORT ( i*x -- _ )(F: k*x -- _ )( R: j*x -- _ ) BYE ( -- _ ) FOO ( x -- | _ )

Yeah, I thought about that too. When "_" is used for a parameter in other programming languages, it's most likely used for a parameter that does not matter.

So, my vote still for ⊥ and never as its synonym. Maybe we can find a better synonym.

---

FOO ( x -- | _ )

Given _ = ⊥, FOO ( x -- | _ ) is equal to FOO ( x -- ).

Proof:

1. ⊥ ⇒ 0*x (by definition)
2. _ ⇒ 0*x
3. 0*x | _ = 0*x (from above)
4. ( x -- | _ ) = ( x -- 0*x | _ ) = ( x -- 0*x ) = ( x -- )

Therefore, FOO ( x -- | _ ) is an excessive expression without any profit comparing to FOO ( x -- ).

[SirWumpus]

Maybe we can find a better synonym.

void = containing nothing, absence of anything, Zen (as oppose to C returning nothing)? I still like _ as an alternative to ⊥ for void/blank.

[ruv]

@SirWumpus wrote:

Maybe we can find a better synonym.

void = containing nothing, absence of anything, Zen (as oppose to C returning nothing)?

The data type void in C, C++, Swift is inhabited, it formally has one member; this type corresponds to 0*x in Forth. In turn, the data type ⊥ (empty type) is uninhabited, it has no members.

In Haskell the void type denotes the empty type. But due to a strong association of void with C, it would be confusing to use void for the empty type in Forth.

I still like _ as an alternative to ⊥ for void/blank.

I think, _ has a more strong association with void/blank (which is inhabited) than with never/falsity/NIL (which is uninhabited). So, it can be used for void/blank, but I don't see any arguments to write ( _ -- _ ) instead of ( -- ) .

---

It could be difficult to understand why the data type 0*x in Forth has one and only one member, and what that member is.

The only member of 0*x is a data object that is a 0-tuple of bits, which occupies zero cells in the stack. This data object is an artifact of the type system. This artifact is needed to formally (in terms of the type system) specify the cases when a Forth word consumes "nothing" from the stack or produces "nothing" on the stack.

The type system in Forth language is a purely formal system, existing at the documentation level. It is not necessary for the artifacts of this type system to exist (in any sense) in a Forth system, or to be accessible to a program.

[alextangent]

Hmmm. Not a big fan of this proposal. Never is related to time, not to an action. As in, it will never happen. He was never there. There is never a good reason to procrastinate. I struggle to understand what noreturn means. A coroutine? And goodness knows what bottom might imply. What value does this stack-based documentation bring? — Alex From: ruv ***@***.***> Sent: Wednesday, September 11, 2024 12:11 PM To: ForthHub/discussion ***@***.***> Cc: Alex McDonald ***@***.***>; Comment ***@***.***> Subject: Re: [ForthHub/discussion] Should stack descriptions document `THROW`? (Discussion #170) use of up tack ( ⊥ ) U+22A5 [...] is painful to type Agreed. There can be an alternative name like bottom, noreturn, never. The variant noreturn is confusing for run-time semantics that cannot be called. I would prefer never. \ DataType: nz = x\0 \ throw ( 0 -- | S: i*x nz -- never R: j*x -- ) \ while ( runtime: nz -- | 0 -- never ) \ exit ( runtime: S: -- never R: nest-sys -- ) The standard stack notation does not allow to indicate several stacks in one diagram. But this is required in some cases. — Reply to this email directly, view it on GitHub <#170 (reply in thread)> , or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAOB6OWQX2PJJSVXF335R5LZWAQLTAVCNFSM6AAAAABNY5JNP6VHI2DSMVQWIX3LMV43URDJONRXK43TNFXW4Q3PNVWWK3TUHMYTANRRGMZDGMI> . You are receiving this because you commented. <https://github.com/notifications/beacon/AAOB6OTMWCK5IBXPATHPSRLZWAQLTA5CNFSM6AAAAABNY5JNP6WGG33NNVSW45C7OR4XAZNRIRUXGY3VONZWS33OINXW23LFNZ2KUY3PNVWWK3TUL5UWJTQAUHY66.gif> Message ID: ***@***.*** ***@***.***> >

[SirWumpus]

Granted the word forms are no clearer than ⊥. Bottom type, other than the poor name, clearly has a purpose in Type Theory.

From Wikipedia Bottom Type:

In such a language, the bottom type may therefore be known as the zero, never or empty type ...

[ruv]

What value does this stack-based documentation bring?

It allows us to better understand the behavior of a word without its text description. Namely, the bottom data type in a stack diagram shows that on some input parameters control is never transferred to the point just after this word, or, the caller of the word never get control back.

For example:

\ ['] ( "<spaces>name" -- xt | ⊥ )
\ ['] ( "<spaces>name" -- xt | never )

The variants: "bottom", "never", "noreturn" — are examples from other programming languages.
See: https://en.wikipedia.org/wiki/Bottom_type#In_programming_languages

Perhaps you can suggest a better option.

[SirWumpus]

Bottom Type obviously the opposite of Top Type ( T ) for "all types". The list of used types in Table 3.1 Data Types has no represent for "no type" aka "bottom type". I see where @ruv is going with this and it makes sense to describe the case when a word leaves the stack in some unknown state.

[SirWumpus]

nil or unknown any one?

[ruv]

it makes sense to describe the case when a word leaves the stack in some unknown state.
nil or unknown any one?

When a word leaves the stack in unknown state, it is shown as i*x, j*x, etc.

For example: execute ( i*x xt -- j*x )

Actually, i*x expresses the top data type (among the types whose all members can be placed on the data stack). Of course, we can introduce a distinct name (symbol) for this data type. I sometime use for that the symbol t (from "tuple"), or ut (from "unspecified tuple"), where ut = i*x . It makes some diagrams clearer.

Note that when a word consumes or produces "nothing", it consumes or produces the empty tuple of parameters. And the empty tuple is a member of i*x.

In turn, the bottom type does not have any member at all (it is the empty type). Therefore, it's impossible that a word (or a function) returns a member of this type.

Therefore, if we document the bottom type for a result, we actually document that the word never returns control.

One more example for the bottom type: bye ( -- ⊥ )

[alextangent]

I understand that. But the result of executing a THROW is not a type. The result is that “the stack depth is the same as it was just before CATCH <https://forth-standard.org/standard/exception/CATCH> began execution. The values of the i * x stack arguments could have been modified arbitrarily during the execution of xt.” — Alex From: Anthony Howe ***@***.***> Sent: Wednesday, September 11, 2024 5:37 PM To: ForthHub/discussion ***@***.***> Cc: Alex McDonald ***@***.***>; Comment ***@***.***> Subject: Re: [ForthHub/discussion] Should stack descriptions document `THROW`? (Discussion #170) Granted the word forms are no clearer than ⊥. Bottom type, other than the poor name, clearly has a purpose in Type Theory. From Wikipedia Bottom Type <https://en.wikipedia.org/wiki/Bottom_type> : In such a language, the bottom type may therefore be known as the zero, never or empty type <https://en.wikipedia.org/wiki/Empty_type> ... — Reply to this email directly, view it on GitHub <#170 (reply in thread)> , or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAOB6ORTRUG2IFKHWKZJQGDZWBWT3AVCNFSM6AAAAABNY5JNP6VHI2DSMVQWIX3LMV43URDJONRXK43TNFXW4Q3PNVWWK3TUHMYTANRRGY3TINQ> . You are receiving this because you commented. <https://github.com/notifications/beacon/AAOB6OUZHQO47BO7OHS2E7TZWBWT3A5CNFSM6AAAAABNY5JNP6WGG33NNVSW45C7OR4XAZNRIRUXGY3VONZWS33OINXW23LFNZ2KUY3PNVWWK3TUL5UWJTQAUH72U.gif> Message ID: ***@***.*** ***@***.***> >

[ruv]

@alextangent wrote:

But the result of executing a THROW is not a type.

Well, there is no a word at all whose execution result is a type.

The result is that “the stack depth is the same as it was just before CATCH began execution.

From a program point of view, this is the result of CATCH. Because the program cannot check what is the stack depth after THROW on a nonzero parameter. The program only can check the stack depth after CATCH. Because THROW never returns control to the caller if its argument is a nonzero.

[alextangent]

It may be that the top i*x entries may have arbitrarily been modified on execution of CATCH , and there may be other disturbances to the system’s total state, but the stack is not in an unknown state. The standard clearly states that the stack depth is deterministic, and is at the same depth as on execution of CATCH.It might be better to document (in a glossary entry?) the other effects to the system’s state if words may THROW. We understand exactly what happens to the stack on a THROW. Some year’s ago THROW was clarified (at least, modified) to address at least one of those changes of state issues by requiring the input sources to be restored to their pre-CATCH state. Interestingly, iirc the only word that THROWs in the whole spec is ABORT. Not even 0 0 / does that. — Alex From: Anthony Howe ***@***.***> Sent: Wednesday, September 11, 2024 5:52 PM To: ForthHub/discussion ***@***.***> Cc: Alex McDonald ***@***.***>; Comment ***@***.***> Subject: Re: [ForthHub/discussion] Should stack descriptions document `THROW`? (Discussion #170) Bottom Type <https://en.wikipedia.org/wiki/Bottom_type> obviously the opposite of Top Type ( T ) for "all types". The list of used types in Table 3.1 Data Types has no represent for "no type" aka "bottom type". I see where @ruv <https://github.com/ruv> is going with this and it makes sense to describe the case when a word leaves the stack in some unknown state. — Reply to this email directly, view it on GitHub <#170 (reply in thread)> , or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAOB6OWWWG5EP7UJY3KN22DZWBYJHAVCNFSM6AAAAABNY5JNP6VHI2DSMVQWIX3LMV43URDJONRXK43TNFXW4Q3PNVWWK3TUHMYTANRRGY4TGNY> . You are receiving this because you commented. <https://github.com/notifications/beacon/AAOB6OWCBQNDOI73YTPQHD3ZWBYJHA5CNFSM6AAAAABNY5JNP6WGG33NNVSW45C7OR4XAZNRIRUXGY3VONZWS33OINXW23LFNZ2KUY3PNVWWK3TUL5UWJTQAUIAGS.gif> Message ID: ***@***.*** ***@***.***> >

[alextangent]

Because the program cannot check what is the stack depth after THROW on a nonzero parameter. The program only can check the stack depth after CATCH. Because THROW never returns control to the caller if its argument is a nonzero.. Then the program will eventually get to ABORT then QUIT, and we know what the stack looks like there. I’m still unsure what problem you’re proposing to fix here. This is documentation (which is good) in the stack diagram (which is not the right place for it). — Alex From: ruv ***@***.***> Sent: Wednesday, September 11, 2024 6:05 PM To: ForthHub/discussion ***@***.***> Cc: Alex McDonald ***@***.***>; Mention ***@***.***> Subject: Re: [ForthHub/discussion] Should stack descriptions document `THROW`? (Discussion #170) @alextangent <https://github.com/alextangent> wrote: But the result of executing a THROW is not a type. Well, there is no a word at all whose execution result is a type. The result is that “the stack depth is the same as it was just before CATCH began execution. From a program point of view, this is the result of CATCH. Because the program cannot check what is the stack depth after THROW on a nonzero parameter. The program only can check the stack depth after CATCH. Because THROW never returns control to the caller if its argument is a nonzero. — Reply to this email directly, view it on GitHub <#170 (reply in thread)> , or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAOB6OSN3KOLKSDBWRXWOLLZWBZ2XAVCNFSM6AAAAABNY5JNP6VHI2DSMVQWIX3LMV43URDJONRXK43TNFXW4Q3PNVWWK3TUHMYTANRRG4YDQMY> . You are receiving this because you were mentioned. <https://github.com/notifications/beacon/AAOB6OU6DD2FRXL25UWHO53ZWBZ2XA5CNFSM6AAAAABNY5JNP6WGG33NNVSW45C7OR4XAZNRIRUXGY3VONZWS33OINXW23LFNZ2KUY3PNVWWK3TUL5UWJTQAUIAPW.gif> Message ID: ***@***.*** ***@***.***> >

[alextangent]

A slightly longer reply. The stack documentation has always had a semi-formal status. Enclosed in a comment ( ) it is not required to be parsed. This is unlikely to change, since there are a significant body of existing programs where there are either no stack comments at all, or their contents are irregular and not amenable to consistent parsing. Much code has stack comments like ( a b | c ). Even so, over the years stack comments have become more widely accepted, and more regularly used. There are a number of formalisms that have also been adopted; notably an attempt at typing (n x xt nt and so on) and the use of | to indicate the state of the stack on entry to the left, and the state of the stack on exit to the right. Prefixes have been introduced; F: R: C: for example to indicate other than the data stack. These are all fine and noble attempts to document the system’s stack effects *in the standard* so that standard words can have their stack effects correctly described. Which they all do; and there have been discussions over the years to tighten up on those types to be more consistent and less ambiguous. My objections are: * This proposal is not about the stack. It’s about the expected execution or run time behaviour. This is most un-stack-like information. * This will be a formal attempt to document the return action (not stack effect) of words *in the standard* * There is exactly one word that would require this new documentation in the standard; THROW. * THROW and CATCH already describe the state of the stack. * You keep saying that the stack is in an unknown state. It’s not. The state of the stack is deterministic and well defined. IMHO, no special word in the stack diagram is required to be documented in the standard. This is a word for a Forth best practices document. — Alex From: ruv ***@***.***> Sent: Wednesday, September 11, 2024 5:50 PM To: ForthHub/discussion ***@***.***> Cc: Alex McDonald ***@***.***>; Comment ***@***.***> Subject: Re: [ForthHub/discussion] Should stack descriptions document `THROW`? (Discussion #170) What value does this stack-based documentation bring? It allows us to better understand the behavior of a word without its text description. Namely, the bottom data type in a stack diagram shows that on some input parameters control is never transferred to the point just after this word, or, the caller of the word never get control back. For example: \ ['] ( "<spaces>name" -- xt | ⊥ ) \ ['] ( "<spaces>name" -- xt | never ) The variants: "bottom", "never", "noreturn" — are examples from other programming languages. See: https://en.wikipedia.org/wiki/Bottom_type#In_programming_languages Perhaps you can suggest a better option. — Reply to this email directly, view it on GitHub <#170 (reply in thread)> , or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAOB6OVJLTHWVDVQP53ZQGTZWBYDFAVCNFSM6AAAAABNY5JNP6VHI2DSMVQWIX3LMV43URDJONRXK43TNFXW4Q3PNVWWK3TUHMYTANRRGY4TAMQ> . You are receiving this because you commented. <https://github.com/notifications/beacon/AAOB6OXNJY5ID7SMHHHXVZ3ZWBYDFA5CNFSM6AAAAABNY5JNP6WGG33NNVSW45C7OR4XAZNRIRUXGY3VONZWS33OINXW23LFNZ2KUY3PNVWWK3TUL5UWJTQAUIAEM.gif> Message ID: ***@***.*** ***@***.***> >

[ruv]

@alextangent wrote:

This proposal is not about the stack. It’s about the expected execution or run time behaviour. This is most un-stack-like information.

Any stack diagram is about execution or run-time behavior, on some extent.

A stack diagram specifies the data type of input and the data type of the corresponding output. The output is what a word returns. If a word never returns control, a standard stack diagram will be incorrect (update: this is wrong, see bellow), because any standard stack diagram specifies the type of the output (even when output is "nothing" — it is a the empty tuple of parameters, which is the only member of the corresponding unit type, which is a member of i*x).

If we introduce the bottom type, we will be able to correctly specify the type of the output for a word that never returns control.

There is exactly one word that would require this new documentation in the standard; THROW.

Not only throw, but also bye, exit, and run-time semantics for ahead, if, while, until, again.

Also, the bottom type can be used in stack diagram for any words that throw an exception on some input parameters (such words will appear as part of some ambiguous condition elimination, for example, all words that do parsing for a word name: ['], ', postpone, to, action-of).

I also have doubts in this regard, but they are of a theoretical/formal nature.

The bottom type (say, never) is a subtype of any other type; consequently, for any type foo, foo|never = foo .

It means, there is a sense to specify the bottom type only when it is the only possible type for some input.
For example: throw ( 0 -- | nz -- never )

But this does not make sense: ['] ( "name" -- xt|never ).
There is a sense if it is written as: ['] ( "name" -- xt | "notfound-name" -- never ).

[ruv]

If a word never returns control, a standard stack diagram will be incorrect,

It seems, I'm incorrect in this. If, for any data type foo, foo = foo|never, then a standard stack diagram is correct even for a word that never returns control.

Therefore, introducing of the bottom type just allows us to make some diagrams more precise.

[ruv]

@alextangent wrote:

You keep saying that the stack is in an unknown state. It’s not. The state of the stack is deterministic and well defined.

Of course, the actual stack is deterministic.

When I said that the stack state is unknown, I meant that the state of the stack at the place where a word will be executed is unknown from the place where the word is documented.

[alextangent]

Yes. Don’t do it. See my next email (which may take me a few days to write; thanks for your patience). — Alex From: ruv ***@***.***> Sent: Thursday, September 12, 2024 12:02 PM To: ForthHub/discussion ***@***.***> Cc: Alex McDonald ***@***.***>; Mention ***@***.***> Subject: Re: [ForthHub/discussion] Should stack descriptions document `THROW`? (Discussion #170) In general, "empty type <https://en.wikipedia.org/wiki/Empty_type> " is more appropriate to describe a case when a function does not return control. And the notion of bottom type may be used for that only as far as a bottom type is empty type. So, from a terminological point of view, it is probably better to talk about an empty type. In the same time, an empty type should not be confused with the empty tuple of parameters. The empty tuple of parameters is not a member of an empty type. An empty type has no members at all, by definition (i.e., it is uninhabited).

…

_____ I would like to choose a short name for an empty type in the Forth type system. The up tack ( ⊥ ) is good, but we need a synonym in ASCII that is easy to enter. I dislike ASCII-art glyph _|_ for this purpose, because it is close to "|" and "_" that are used (or can be used) separately in a stack diagram, producing worse readability, e.g.: ( 0 -- _|_ | -- nz ) . The word "empty" does not fit because it is associated with the empty tuple. The word "unreachable" is a possible variant. But I think "never" is better, because it's shorter. Please let me know if you have some arguments or better options. — Reply to this email directly, view it on GitHub <#170 (reply in thread)> , or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAOB6OSSJBWBG3KZPLAGBPDZWFYA5AVCNFSM6AAAAABNY5JNP6VHI2DSMVQWIX3LMV43URDJONRXK43TNFXW4Q3PNVWWK3TUHMYTANRSGQ4TIOA> . You are receiving this because you were mentioned. <https://github.com/notifications/beacon/AAOB6OT73QMU6ZWHAUSLSE3ZWFYA5A5CNFSM6AAAAABNY5JNP6WGG33NNVSW45C7OR4XAZNRIRUXGY3VONZWS33OINXW23LFNZ2KUY3PNVWWK3TUL5UWJTQAUIP3I.gif> Message ID: ***@***.*** ***@***.***> >

[ruv]

@alextangent wrote:

Don’t do it. See my next email (which may take me a few days to write; thanks for your patience).

Alex, thank you for your criticism. I'll be waiting for your next email.

Note that I already use this notation in my code, I find it useful, and I don't see why I shouldn't use it. If some people find it useful, they will use it too. But most people don't use data types in they stack diagrams at all.

[alextangent]

What I mean by “don’t do it” is don’t formally document it in the standard. Of course you can use whatever notation you see fit in your code; as we all know, anything between ( and ) is entirely there for the author and reader’s benefit.  : callback: ( n <name> -- ) \ generate callback head My code makes extensive use of <brackets> to indicate parsing words. It documents that we’re expecting `1234 callback: mycallback` . The standard suggests using quotes as in:  : callback: ( n “name”  -- ) \ generate callback head It’s a shame (at least to me) that much of section 2 of the standard is normative.  — Alex From: ruv ***@***.***> Sent: Thursday, September 12, 2024 3:35 PMTo: ForthHub/discussion ***@***.***> Cc: Alex McDonald ***@***.***>; Mention ***@***.***> Subject: Re: [ForthHub/discussion] Should stack descriptions document `THROW`? (Discussion) ***@***.*** wrote:

Don’t do it. See my next email (which may take me a few days to write; thanks for your patience).

Alex, thank you for your criticism. I'll be waiting for your next email. Note that I already use this notation in my code, I find it useful, and I don't see why I shouldn't use it. If some people find it useful, they will use it too. But most people don't use data types in they stack diagrams at all.

[ruv]

@alextangent wrote:

What I mean by “don’t do it” is don’t formally document it in the standard.

Why not? This does affect neither programs nor systems.

Anyway, this can only be formally documented if every committee member agrees with it. There is a very small chance for that.

[alextangent]

Why not? This does affect neither programs nor systems.

If it affects nothing, then why have it in the standard? Just leave it out and have the discussion here. — Alex

On 12 Sep 2024, at 20:59, ruv ***@***.***> wrote: @alextangent wrote: What I mean by “don’t do it” is don’t formally document it in the standard.

Why not? This does affect neither programs nor systems. Anyway, this can only be formally documented if every committee member agrees with it. There is a very small chance for that.

[ruv]

@alextangent wrote:

If it affects nothing, then why have it in the standard?

It makes specifications for some words more clear, also it makes explicit some things that are implicit at the moment.

Have a look at the word abs ( n -- +n ). Note that the stack diagram ( n -- x ) is also correct for abs, because +n is a subtype of x and any output parameter of abs is a member of x.

Why should not we use ( n -- x ), but ( n -- +n ) for abs?

We should use the smallest suitable data type to describe a stack parameter or a mapping of the input parameters to the output parameters. Where "smallest" data type means the one having the least number of members among suitable data types.

Obviously, +n has fewer members than x, and it includes all possible output parameters of abs. Therefore, we should use +n.

Now let's apply this logic to the word bye. The size of the type ( -- ⊥ ) is less than the size of the type ( -- ) (because ⊥ has fewer members than 0*x), and they both are suitable for bye. So, we should prefer the former: bye ( -- ⊥ ).

The Forth type system already implies the empty type ( ⊥, "never"), the 0-tuple of parameters and the corresponding unit type (0*x, "nothing"), but it does not name them.

[alextangent]

Here’s a quick 2 cents on this one. You want to use the most restrictive (or narrowest or smallest) type for the return value of abs. It’s defined in the standard as abs ( n -- u ). Bernd Paysan has given a reference implementation of abs ( n -- +n ). It could be written as abs ( n -- x ). What the difference is between u or x or +n isn’t really the argument here; I think you’re attempting to define what abs does, but by using the stack diagram to do so. abs should always return the absolute value of n, but that is evident from the text (and the name, although I admit that’s not always guaranteed), and we really don’t need to describe the value that the word abs returns. If we were to be absolutist about this, then we ought to fix up MOD and NEGATE and other similar words, and invent a whole bunch of other symbols for other words with imprecise stack diagrams that seem to require more narrowly defined values. The stack diagram’s usefulness isn’t that it describes the *values* of the stack entries, but that it describes the *depth of the stack* on entry and exit and the *use* of the stack cell or cells. So xt, nt, ior and so on; they are silent about the values but describe their use. Having x or u or n as the stack on exit from abs isn’t in any way confusing or ambiguous, and as you can clearly see I’m not in the “should use the most restrictive type” camp because we’ll keep inventing types to describe (actually, proscribe) values when we don’t need to; there’s no extra information in them that can’t be had from other comments or the text in the standard. A case in point; bye ( -- ⊥ ). The stack diagram in the standard is fine. It requires nothing on the stack, and guess what – after it has been executed, there aren’t any stacks to worry about, as the standard text makes abundantly clear. Run bye. Poof. They’re gone. But here we are inventing symbols for something that is self-evident. The other suggestion that ⊥ indicates no return to the caller breaks for me the simplicity of the stack diagram. It’s no longer about the stack, but about the state of the system after execution and side effects that the word may have. We could define a whole host of symbols; how about indicating that after the execution of PARSE the parse area has moved forward n chars with ->+n? (More general note. Document your words as you like, but please don’t make Forth look like APL. I consider my time decades ago using APL well spent, but the symbol set was always a nightmare. The up-tack is the dyadic function decode; A⊥B is the value of a polynomial whose coefficients are B at A. Great function, nightmare to type and read. No, I can’t remember what it does or how to use it.) I think I’m all argued out. Have a nice day :) — Alex From: ruv ***@***.***> Sent: Friday, September 13, 2024 11:14 AM To: ForthHub/discussion ***@***.***> Cc: Alex McDonald ***@***.***>; Mention ***@***.***> Subject: Re: [ForthHub/discussion] Should stack descriptions document `THROW`? (Discussion #170) @alextangent <https://github.com/alextangent> wrote: If it affects nothing, then why have it in the standard? It makes specifications for some words more clear, also it makes explicit some things that are implicit at the moment. Have a look at the word abs ( n -- +n ). Note that the stack diagram ( n -- x ) is also correct for abs, because +n is a subtype of x and any output parameter of abs is a member of x. Why should not we use ( n -- x ), but ( n -- +n ) for abs? We should use the smallest suitable data type to describe a stack parameter or a mapping of the input parameters to the output parameters. Where "smallest" data type means the one having the least number of members among suitable data types. Obviously, +n has fewer members than x, and it includes all possible output parameters of abs. Therefore, we should use +n. Now let's apply this logic to the word bye. The size of the type ( -- ⊥ ) is less than the size of the type ( -- ) (because ⊥ has fewer members than 0*x), and they both are suitable for bye. So, we should should prefer the former: bye ( -- ⊥ ). The Forth type system already implies the empty type ( ⊥, "never"), the 0-tuple of parameters and the corresponding unit type (0*x, "nothing"), but it does not name them. — Reply to this email directly, view it on GitHub <#170 (reply in thread)> , or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAOB6OVL725XPRNFUG3V74TZWK3FJAVCNFSM6AAAAABNY5JNP6VHI2DSMVQWIX3LMV43URDJONRXK43TNFXW4Q3PNVWWK3TUHMYTANRTGYZDCNY> . You are receiving this because you were mentioned. <https://github.com/notifications/beacon/AAOB6OQDU7TMBUQY7UKHDJDZWK3FJA5CNFSM6AAAAABNY5JNP6WGG33NNVSW45C7OR4XAZNRIRUXGY3VONZWS33OINXW23LFNZ2KUY3PNVWWK3TUL5UWJTQAUJF3S.gif> Message ID: ***@***.*** ***@***.***> >

[ruv]

@alextangent wrote:

If we were to be absolutist about this, then we ought to fix up MOD and NEGATE and other similar words, and invent a whole bunch of other symbols for other words with imprecise stack diagrams that seem to require more narrowly defined values.

There is no point in introducing a data type symbol for some subtype without a good reason. There was probably a good reason to introduce +n. And since we already have this data type symbol, it must of cause be used when appropriate.

A rule of thumb: if using of a new data type symbol excludes some incorrect combinations of words, then it is worth introducing (see an example below).

The other suggestion that ⊥ indicates no return to the caller breaks for me the simplicity of the stack diagram.

This is not quite correct. The only elements of a stack diagrams are: stack identifiers, parsed text abbreviations, data types (denoted by data type symbols) and operators (namely, |, --, and a whitespace). There is no any other indicators.

And the symbol ⊥ denotes a data type, namely the empty data type. It does not directly indicate "no return".
"No return" is a consequence of the fact that this data type is uninhabited (has no members).

A case in point; bye ( -- ⊥ ). The stack diagram in the standard is fine.

Given the stack diagram bye ( -- ), the code «123 bye . » is formally correct, although meaningless.

Given the stack diagram bye ( -- ⊥ ), the code «123 bye . » is formally incorrect.
Explanation:

  123 ( n )
  bye ( n never )
  .   \ expected: ( n )  actual: ( never )

Where never is a synonym for ⊥.
NB: A Forth system is not obligated to abort in this case, it may show a warning or just ignore.

The stack diagram’s usefulness isn’t that it describes the values of the stack entries, but that it describes the depth of the stack on entry and exit and the use of the stack cell or cells. So xt, nt, ior and so on; they are silent about the values but describe their use.

Actually, this is not about "depth of the stack", but abut the size of a tuple in cells. Anyway, if this was only about depth/tuple size, it would be enough to use i*x notation, like find ( 1*x -- 2*x ), search-wordlist ( 3*x -- 1*x | 2*x ), etc.

The most important thing is that more narrowed data type annotations make some wrong combinations of words formally incorrect. One more example: if we use x instead of xt in execute ( i*x xt -- j*x ), then «here execute» is a formally correct code. Using of xt in the stack diagram makes this code formally incorrect.

[...] but please don’t make Forth look like APL

It is acceptable for me to use "never" or other noun to denote the empty data type.