Re: [stack] stackless fixed-arity concatenative languages

After doing some thinking, I've come up with an example of where an n- 
ary 'dip' combinator makes a complete mess of things. The example is  
Factor's 'bi@' combinator. The 'bi@' combinator takes some x, some y,  
and a quotation which it applies to both. As an example, '4 5 [ dup  
* ] bi@' yields '16 25'.

Here's one way we might think to implement 'bi@' in Factor:

    : bi@ ( x y quot -- x' y' ) dup dip dip ;

The thinking here is that we duplicate the quotation, apply it below  
the original quotation to 'y', then apply the original quotation to  
'x'. Just to be clear, I'll trace the execution of an expression as if  
Factor used term rewriting (which I find is the easiest way to show  
this sort of thing):

    4 5 [ dup * ] bi@
    4 5 [ dup * ] dup dip dip
    4 5 [ dup * ] [ dup * ] dip dip
    4 5 dup * [ dup * ] dip
    4 5 5 * [ dup * ] dip
    4 25 [ dup * ] dip
    4 dup * 25
    4 4 * 25
    16 25

Great. It worked as we wanted it to. There is, however, a bug. The bug  
is that the first call to the quotation has both 4 and 5 on the stack,  
while the second call only has 4 on the stack. In other words, the  
quotations are exposed to stacks of different sizes. If the quotation  
supplied uses two elements on the stack rather than one, very weird  
things will happen.

Surely a type system like Cat's would catch this, yes? Well, sort of.  
Unfortunately, it does it in the worst way possible; it gives bi@ the  
type 'A [A -> A b] -> A b b'. What this means is that the quotation  
must keep the type of the stack the same and add another element. This  
means doing '4 5 [dup *] bi@' would be a type error since '[dup *]' is  
not an instance of '[A -> A b]'; it's an instance of '[A b -> A b]'.  
Furthermore, it doesn't even indicate that two elements must be below  
the quotation on the stack! As a result, all you can do are things  
like '4 5 [6] bi@' to yield '4 5 6 6' which makes the function  
completely useless.

One way to solve this problem is to use a version of 'dip' that calls  
a quotation with only one element and requires the quotation to yield  
one element. Cat's type system cannot enforce this, but Fifth's type  
system can. Below are the types of the unrestricted 'dip' combinator  
and the restricted version:

    dip    :: A b [A -> C] -> C b
    dip1-1 :: a b [a -> c] -> c b

As you can see, the types are basically the same, except the quotation  
can only take one element 'a' and transform it to one element 'c'  
rather than the stack 'A' to the stack 'C'. Using the restricted  
combinator, our function would look like this:

    bi@ = dup dip1-1 dip1-1

We could then assign it the following type:

    bi@ :: a a [a -> b] -> b b

This type is much more like what we wanted. Indeed, it'll let us do '4  
5 [dup *] bi@'. It does have the restriction however that both  
elements below the quotation must be of the same type. To solve this  
we need higher rank types which is another discussion altogether.

Now the nasty bit: 'bi@ = dup dip dip' can be assigned the type above  
in Fifth provided that you give it a signature. The signature 'a a [a - 
 > b] -> b b', however, is not an instance of the type that is  
inferred (which is the same as Cat's: 'A [A -> A b] -> A b b'). This  
is very unfortunate as it means Fifth does not have principal types in  
the presence of n-ary combinators! This problem would hold for Cat as  
well if it had a way of enforcing similar arity restrictions (which it  
will need to be able to eventually for things like callbacks if  
nothing else).

This is rather damning, and it may mean that n-ary combinators have to  
be completely eliminated unless a more expressive system can be found.  
One way to do this would be fixed arity versions of 'dip' and 'i',  
along with built-in mechanisms for pattern matching and deconstruction  
(a la Haskell, et al) rather than simply using normal functions like  
'unlist' as I've talked about previously. There would still need to be  
some way to address the need to allow the user to write new  
combinators like '2dip' that apply a quotation below the top two  
elements of the stack rather than just one. Introducing something like  
lambda expressions would be one way to do this (similar to how  
Backus's Formal FP allowed lambda expressions for creating new  
combinators).

It's important to remember that 'dup dip dip' works fine for our  
expected use case, but has some very strange behaviors lurking about!  
The new type system I'm working on does capture this by giving 'dup  
dip dip' the type '[$A] => $A [$A] dip'. Essentially, it types 'dup  
dip', realizes there's no most general way to proceed, and stops and  
waits for more information about $A (the quotation passed in).  
Unfortunately, this type system is undecidable, expensive, and yields  
ugly types. What fun!

So what's the correct way to write 'bi@' so that Cat gives it the  
correct type without placing an arity restriction on the quotation? It  
turns out there isn't one. I thought maybe something like 'under apply  
slip' would work, but I get the rather insane type 'A b (A self b -> C  
(C -> D) e) -> D e'. Amusing. Another attempt was 'under [[apply dip]  
dip apply', but this gets the type 'A b b -> (A b -> A) -> A' which  
means you can only do things like '3 4 [pop] bi@' and hence it's  
rather useless. If you think about it, there's really no way it could  
possibly give a useful type without an arity restriction. Well,  
actually it could if you had first-class stacks. That's something else  
I have to consider as a possible solution...

Hey, I thought concatenative languages were supposed to be simpler!

- John