Re: [stack] stackless fixed-arity concatenative languages

On May 22, 2008, at 2:03 AM, John Nowak wrote:

> There are probably others as well. The huge issue here is that none of
> these types are instances of another! If you believe Cat could
> eventually type 'dup dip dip' in a satisfactory manner, what type
> would you want to give it? As far as I can tell, without a system that
> delays typing as necessary such as the one I've hinted at recently, it
> isn't possible to give a most general type even with annotations.
> Maybe a system with intersection types could do it.

Slava has suggested this intersection type for 'bi@':

    bi@ :: A b (A -> C /\ C b -> D) -> D

This is a rather interesting type. It only requires one element on the  
stack below the quotation; it applies the quotation to whatever is  
below the top element, then applies it again to whatever the first  
quotation did with 'b' added to the top. When using two (or more)  
elements below the quotation, it is not required that they be of the  
same type. This is a very general type that would cover all uses I can  
think of.

The downside, of course, is that the purpose of 'bi@' is not clear  
from the type. Additionally, many misuses of 'bi@' would not be caught  
until possibly much later. Still, the generality is appealing.

The kind people on #concatenative also pointed out that 'dup dip dip'  
behaves differently than the version of 'bi@' in Factor because it  
applies the quotation to 'y' first, not 'x'. In an impure language,  
these are obviously not equivalent. A definition that matches the  
semantics of 'bi@' in Factor is 'dup [ dip ] dip call', or '[ dip ]  
keep call'.

So far, I've only done a small about of work with intersection types  
in a concatenative setting. Perhaps it is worth more attention.

- John