[stack] fundamental type system problems + possible solutions

It seems there's a fundamental problem with typing concatenative  
languages: Most type systems are not compositional which destroys the  
simple algebra of concatenative programs. Take these equivalencies for  
example:

    [$A] i       ==  $A       -- application
    [$A] [$B] o  ==  [$A $B]  -- composition
    $a [$B] pa   ==  [$a $B]  -- partial application
    [$A] m       ==  [$A] $A  -- self-application

Unfortunately, all of these rules (except perhaps for partial  
application) fall apart once types are involved. This is of practical  
concern as it makes cut-and-paste refactoring impossible and will  
cause problems with many macro transformations.

What is needed is a type system that is compositional. One system that  
meets this requirement is System E developed by Carlier and Wells [1].  
While this seems like an appealing solution at first, the types  
produced by System E are so complex that they're not really human- 
decipherable. Even if a solution to making error reports  
understandable could be found via some form of type error slicing [2],  
there would still be no way to make types useful as documentation.

As I see it, there are three main benefits of static type systems:  
Automatic and correct documentation, increased safety, and increased  
efficiency. Of these three, I consider documentation to be the most  
important. After all, there are language implementations without  
static type systems that perform quite well such as SBCL and LuaJIT.  
As for safety, dynamic languages are used to build highly-reliable  
systems (see Erlang); ultimately, the design of a program and ability  
of the implementors contributes much more to software reliability than  
the presence of a type system (compare Haskell/Darcs to C/Perl/Git).

The need for documentation, however, you can't escape. This is  
especially so in stack-based languages where stack effect comments are  
necessary to make sense out of things. While no type system will  
replace the need for such comments entirely, as it is often necessary  
to state not just the type of a value but its purpose, a type system  
can at least ensure the correct number of arguments will always be  
passed and that type constraints will be respected.

I would rather have no type system than one which makes simple  
transformations, and hence macros and much refactoring, impossible.  
Static type systems seem doomed to being either non-compositional or  
not suited to producing human-readable documentation.  Therefore, as I  
see it, there are two possibilities going forward.

One is to develop a soft type system that hopefully will be able to  
report most errors without rejecting any program. If a language is  
designed with a soft type system in mind, the quality of error  
reporting can be quite good. For example, dynamic checks can be  
inserted to ensure lists are used homogeneously and type declarations  
can be required for data types to avoid the need for equi-recursive  
types.

The other approach would be some way of inferring the equivalences  
mentioned at the beginning of this email. I guess this would take the  
form of some kind of abstract interpretation. The goal here would not  
be to catch all type errors (although some would be catchable), but  
rather to provide a detailed description of what a function does  
beyond what an HM-based type system would be capable of yielding. It  
seems the primary issue here would be giving equivalencies for  
functions involving recursive data types. For example, if we define  
some 'each' function that simply places an element from a list on the  
stack and then calls some function repeatedly until the list is empty,  
how would we express this?

Anyway, these are just my current thoughts. As for Fifth, I've decided  
to delay inclusion of the type system until I can find a solution that  
won't cause problems with macros or inhibit cut-and-paste refactoring.  
(I'll credit Slava Pestov for reminding me of how critical this is.)  
Any thoughts would be appreciated, especially regarding the second  
approach described above.

- John

[1] http://www.church-project.org/modular/compositional/system-E/
[2] http://www.macs.hw.ac.uk/ultra/compositional-analysis/type-error-slicing/slicing.cgi