Re: [stack] syntax preference question

On Jun 17, 2008, at 8:03 PM, William Tanksley, Jr wrote:

> John Nowak <[email protected]> wrote:
>
>> Say I write this definition for a combining form:
>>   foo(a, b) = [a, b]
>> If cleave is type-directed, there's no way to give this a type. You'd
>> need to require an annotation in such a case.
>
> I don't get it. Can you provide a specific counterexample where this
> doesn't receive a type?

Ah, I knew I didn't explain that properly (well, at all really). Let  
me recap briefly so I can be sure I've covered it.

Factor has a family cleave combinators like bi, tri, etc, which I  
assume you're familiar with (otherwise this may not make any sense).  
Here is the type of 'bi' in 5th:

    bi(A b -> C, C b -> D) => A b -> D

What this says is that bi takes one function of type 'A b -> C' and  
one of type 'C b -> D' and yields a function of type 'A b -> D'.  
(Remember that 'bi' is a combining form (aka functional) in 5th, so it  
takes functions as arguments and yields a function as a result.) The  
type of 'tri' is just an extension of the type of 'bi':

    tri(A b -> C, C b -> D, D b -> E) => A b -> E

Factor has a combinator named 'cleave' that generalizes these. For  
example, instead of writing '[ a ] [ b ] [ c ] tri', you can write  
'{ [ a ] [ b ] [ c ] } cleave'. 5th can handle cleave properly. To be  
clear on the translation:

    bi(a, b)      =  cleave(a, b)     =  keep(a) b
    tri(a, b, c)  =  cleave(a, b, c)  =  keep(a) keep(b) c

Factor also has the combinators '2bi' and '2tri'. These save and push  
on the top two elements for each quotation rather than just one. The  
types are as follows (forgive me if I'm stating the obvious):

    2bi(A b c -> D, D b c -> E) => A b c -> E
    2tri(A b c -> D, D b c -> E, E b c -> F) => A b c -> F

And the equalities:

    2bi(a, b)      =  2cleave(a, b)     =  2keep(a) b
    2tri(a, b, c)  =  2cleave(a, b, c)  =  2keep(a) 2keep(b) c

Now, for a brief digression. Factor also has 'bi@' 'tri@' combinators.  
Appending the "@" means that the same function is used for all cases:

    bi@(a)   =  cleave(a, a)     =  keep(a) a
    tri@(a)  =  cleave(a, a, a)  =  keep(a) (a) a

To type these properly, we need to use intersection types:

    bi@(A b -> C /\ C b -> D) => A b -> D
    tri@(A b -> C /\ C b -> D /\ D b -> E) => A b -> E

If you want, I can get into the reason this is necessary. For now,  
back on track.

An important thing to note about 'cleave' and '2cleave' is that they  
don't care at all what the arities of the functions are; they push on  
one (or two, in the case of '2cleave') elements for each quotation  
regardless. For example, these are all equivalent:

   5 cleave(neg, *) = 5 bi(neg, *) = 5 keep(neg) * = 5 neg 5 * = -25

Alright, now onto the "type-directed cleave". Agh, so much to say.

I came up with the idea for a type-directed cleave when trying to  
figure out the concatenative equivalent of the functional form of  
"construction" from Backus's FP. What construction does is take  
several functions and some 'x' and return an array of all of the...  
well, I'll just show it:

    [neg, sqr, sqrt]:9
    [neg:9, sqr:9, sqrt:9]
    [-9, 81, 3]

It turns out that construction is the same as the normal 'cleave':

    9 cleave(neg, sqr, sqrt)
    9 neg 9 sqr 9 sqrt
    -9 81 3

In FP, there's no way to have something like '2cleave'. What you need  
to do is bundle the two arguments into an array and use a combination  
of construction and "insert" (which is the same as 'foldl1' in  
Haskell, i.e. a fold with the head of the list as the initializer). To  
be clear, the slash denotes the "insert":

    [/+, /-, /*]:<5, 3>
    [/+:<5, 3>, /-:<5, 3>, /*:<5, 3>]
    [5 + 3, 5 - 3, 5 * 3]
    [8, 2, 15]

This works, but the downside is the need to explicitly use insert for  
each function. The equivalent in 5th using cleave is rather ugly (and  
grossly inefficient):

    (5, 3) cleave(reduce(+), reduce(-), reduce(*))
    (5, 3) reduce(+) (5, 3) reduce(-) (5, 3) reduce(*)
    5 3 + 5 3 - 5 3 *
    8 2 15

Hence, we have '2cleave', which doesn't require the bundling and  
inserting/reducing of the FP and 'cleave' versions:

    5 3 2cleave(+, -, *)
    5 3 + 5 3 - 5 3 *
    8 2 15

Anyway, the point of the "type-directed cleave" was to be able to  
write ' 5 3 [+, -, *]' and have it magically work. Of course, in order  
to know how many items to copy and push on for each function, you need  
to know their arities. There are *three* ways you can go about doing  
this.

The first way is to require all functions have the same arity (at  
least in terms of what they consume -- the productions don't matter).  
This works great for the '[+, -, *]' example, but it's a bit  
restrictive.

The second way is to allow each function to have a different arity. In  
order to figure out how many items to save, you save as many as  
necessary for the function with the greatest arity. For example:

    2 3 4 [+, dup, rot]
    2 3 4 + 2 3 4 dup 2 3 4 rot
    2 7 2 3 4 4 3 4 2

The third way is the most bizarre, but perhaps the most useful. What  
you do is save as many items as necessary for the function with the  
greatest arity. However, for each function, you only push on as many  
items as it directly uses. For example:

    2 3 4 [+, dup, rot]
    3 4 + 4 dup 2 3 4 rot
    7 4 4 4 2 3

Of the three, the third possibility, I think, is the most useful; the  
second is awkward to use in many cases and the first is just a special  
case of the second and third.

Now, there are a couple things to point out here.

With the normal 'cleave', as shown earlier, we can do things like '5  
cleave(neg, *)' to get '-25. This is impossible with any of the type- 
directed variants above. This isn't really a big problem however as '5  
cleave(neg, *)' is really misusing 'cleave'. It should be written as  
'5 keep(neg) *' instead.

The other, and much more important thing thing to note, is that it is  
impossible to figure out how many items to save and push on for the  
first two type-directed variants unless at least one function is  
provided. In other words, you can't give a rewrite rule or any sort of  
dynamic semantics for this definition of 'foo':

    foo(a, b) = [a, b]

However, with the first two type-directed variants, you could for this  
definition of 'bar':

    bar(a, b) = [a, b, +]

The rewrite rule here would be 'x y (a, b) = x y a x y b'. Again,  
without the additional context given via '+', there's no way to do  
this for the first two type-directed variants.

For the third type-directed variant, there's no way to give a dynamic  
semantics unless *all* functions are provided. As interesting as this  
third variant is, it is just too powerful to include in the language.  
Of the three, only the first is really sensible. In that case however,  
all it does is save you a character so that you can avoid specifying  
the arity of the quotations.

I don't think saving that character is worth the clutter in the  
language definition. It would mean you can't look at the type system  
as merely a means of restricting the dynamic semantics of the  
language. This is the same nasty situation Haskell is in with respect  
to type classes. Type classes, however, at least provide some real  
expressive powerful.

To very briefly clarify on what I mean about the type system no longer  
simply restricting the language, I'll give a brief example. Let's say  
we write something like this:

    id1 = dup drop
    id2 = swap swap

All 'id1' does is ensure one element is on the stack. All 'id2' does  
is ensure two elements are on the stack. On a stack with many items,  
they're identical. However, when using them in a type-directed cleave,  
they have different properties. For example, '1 2 3 type-cleave(id1,  
id1)' is not the same as '1 2 3 type-cleave(id2, id2)', even though  
they would be with a normal cleave.

It should hopefully be obvious now that, since a type-directed cleave  
is essentially meaningless unless sufficient context is given, that we  
also can't type it without that same context. I hope it is also clear  
why I said in the previous email that they're almost certainly a bad  
idea. I apologize for taking the *long* way to get to this conclusion,  
but I'm far too tired to write something concise.

- John