Re: [stack] stackless fixed-arity concatenative languages

On May 21, 2008, at 11:19 AM, Christopher Diggins wrote:

> That Cat type issues you have identified are appreciated. They are
> related to the inability to properly assign the correct level of
> nesting of nested forall qualifiers, and to do renaming properly. This
> is still something that I have on my to-do list, to try and improve.

I think you may be underestimating the problem here. The issue is  
that, for 'dup dip dip', all of these are valid and (somewhat) useful  
types:

    // Call a quotation yielding a single value on some stack twice
    A (A -> A b) -> A b b

    // Call a quotation on two separate values (the intended use)
    A b b (b -> c) -> A c c

    // Destroy the top two values of the stack in some special
    // way, such as displaying them or specially deconstructing
    A b b (b ->  ) -> A

    // Apply a binary function such as equality to two pairs on top
    // of the stack
    A b c b c (b c -> d) -> A d d

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.

I'm guessing here, but I think a system similar to Cat's cannot have  
principal types if you allow non-row polymorphic functions alongside  
row polymorphic functions. Given that you do need them for typing  
things like 'bi@' in a satisfactory manner and for typing things like  
callbacks (where you save a function that uses no more than N stack  
elements somewhere), this seems to be a real problem.

It does seem though that row polymorphic functions or non-row  
polymorphic functions alone do not cause an issue. For example, if you  
have a version of 'dip' for every arity combination, you don't run  
into this issue. If you only have row polymorphic functions, then 'A  
(A -> A b) -> A b b' is a most general type. It's the combination of  
an n-ary dip with non-row polymorphic constraints that causes the  
issue (because you can make many more uses of a function type check).

Even though the new system I'm working on can handle 'dup dip dip'  
properly, it's not at all clear if that's even a desirable property!  
After all, 'dup dip dip' can do quite a few different things depending  
on how you constrain it. It may very well be better to have the  
programmer give different types for each intended use and document the  
possible uses separately. From an implementation point of view, 'A b b  
(b -> c) -> A c c' and 'A b c b c (b c -> d) -> A d d' are very  
different combinators anyway.

My issue then is that Fifth, as it is now, infers a type which is not  
most general (as indeed no most general type exists for 'dup dip dip'  
in my system). This is likely to confuse the programmer as their  
function is (sort of) correct and type checks but cannot be used in  
the intended manner. The only way I can think of right now to avoid  
this problem is to get rid of n-ary combinators like 'dip' and require  
the programmer to use a more specific combinator.

I'm also looking at taking an approach similar to FP or FL where you  
have certain combining forms that take functions directly. For  
example, I could use the 'dip' combining form to do something like  
'(dip +)' which would add two values below the top of the stack. The  
difference here is that the '+' function is supplied directly to the  
combining form and hence is known statically. Because of this, there's  
no need for any sort of arity specification or multiple versions of  
'dip'. If you wanted to 'dip' a quotation only known at runtime, you  
could combine the 'dip' combining form with the 'i' combining form  
that requires an arity specification. For example, to dip any binary  
function on top of the stack, you could do '(dip (i 2 1))'. What I  
like about this approach is that the static uses avoid redundant arity  
annotations and dynamic uses make their intent explicit.

- John