Problem with u|n notation in Forth-94 and Forth-2012

[ruv]

Most people (including myself) interpret the following stack diagram as equivalent:

• ( c-addr u -- nt | 0 ) and ( c-addr u -- nt|0 )
• ( n1 n2 -- n1|n2 ) and ( n1 n2 -- n1 | n2 )
• ( c-addr -- xt|0 ) and ( c-addr -- xt | 0 )
• ( c-addr -- xt -1 | xt 1 | c-addr 0 ) and ( c-addr -- xt -1|1 | c-addr 0 )

In these stack diagrams, the symbol "|" denotes a binary infix operator over data types, meaning the union of data types.

Now, have a look at the stack diagram for the standard word 1+:
( n1|u1 -- n2|u2 )
In this case, either the symbol "|" does not denote the union of data types, or the stack diagram is incorrect for the word 1+.

If, in this stack diagram, n2|u2 is a union, we cannot write 1+ mod, since mod expects n at the top (not n|u), and we formally end up in an ambiguous condition because "an incorrectly typed data object is encountered".

The effective arrow type for 1+ is
( n -- n ^^ u -- u ^^ u -- n ^^ n -- u ),
where "^^" denotes intersection of arrow types.

Note that this arrow type is a subtype of ( n -- n ), and a subtype of ( u -- n ), so 1+ mod is correctly typed.

To fix this problem in all cases where u|n or d|ud is used, we should either write such a long intersection of arrow types, or introduce a syntactic sugar using a different symbol instead of "|".

Possible alternative for a different symbol:

• (a) ( n!u n!u -- n!u )
• (b) ( n~u n~u -- n~u )
• (c) ( n%u n%u -- n%u )
• (d) ( n,u n,u -- n,u )
• (e) ( [n,u] [n,u] -- [n,u] )
• (f) something else?

Which option do you prefer?

[RogerLevy]

I think | is the best symbol and that this is a wild goose chase.

In (classic) Forth, a data stack item can be whatever you want it to be at any time, and therefore stack diagrams are helpful hints and not much more. Signed can become unsigned, or address, or part of a double, or flag, or anything you can think of.

If you want reliable types you need a typed language. This fluidity is just a tradeoff.