Re: [stack] improved parallel combinator

On Jan 7, 2009, at 6:41 PM, William Tanksley, Jr wrote:

> John Nowak <[email protected]> wrote:
>
>> Spread, cleave, and this are all easy to type check. The combinator I
>> proposed before this isn't; it might be doable, but I don't think  
>> it's
>> worth doing.
>
> Are you saying that (| |) is hard to typecheck? And I thought that
> spread and cleave were hard.

Spread, cleave, and (| |) are easy. That [( )] thing with the vector- 
like semantics I proposed before is not; it would require some sort of  
type coercion.

Here are some examples of cleave and spread combinators:

    bi   :: R x [R x -> S] [S x -> T] -> T
    2bi  :: R x y [R x y -> S] [S x y -> T] -> T
    3bi  :: R x y z [R x y z -> S] [S x y z -> T] -> T
    bi@  :: R x [R x -> S /\ S x -> T] -> T
    2bi@ :: R x y [R x y -> S /\ S x y -> T] -> T
    3bi@ :: R x y z [R x y z -> S /\ S x y z -> T] -> T
    bi*  :: R a x [R a -> S] [S x -> T] -> T
    2bi* :: R a b x y [R a b -> S] [S x y -> T] -> T

The "tri" versions are essentially the same, just with three  
quotations instead of two.

Here are the (| |), aka 'parallel' types:

    parallel1 :: R [R -> S] -> S
    parallel2 :: R [R -> S] [R -> T x] -> S x
    parallel3 :: R [R -> S] [R -> T x] [R -> U y] -> S x y
    parallel4 :: R [R -> S] [R -> T x] [R -> U y] [R -> V z] -> S x y z

All of these can be inferred in my current system; only the '@'  
versions are tricky because they require intersection types. Cat can  
handle the types for all except the '@' versions, although you can't  
actually *implement* the 'parallel' combinators in Cat because it  
doesn't support parameterized types (although they could be offered as  
primitives).

> Oh, I know -- cleave doesn't split into multiple stacks, which to me
> makes it harder to think about. I admit that what cleave does with
> multiple stacks IS useful, but I don't have a conceptual model yet for
> it.

I'm not sure how useful it is. The reason 'cleave' was invented was to  
convey intent. You *could* just write '[ F ] keep G', but you write  
'[ F ] [ G ] bi' if they're both operating on the same value to make  
the code more clear. The fact that 'cleave' allows G to access the  
results of F is, in my opinion, undesirable. Slava has shown me a  
couple of cases where it is intentionally used in such a way (I think  
with tuple selectors or something), but I don't think those use cases  
are particularly valuable.

The good thing about 'cleave' compared to 'parallel' is that the  
quotations can return multiple values directly on the stack, not just  
one. It would be nice to extend 'parallel' to do this, but again,  
you'd need those ugly concatenation types. The fact that we can type  
so much without them is actually somewhat surprising.

> The gatherer was intended to be a lot simpler than that. The type  
> should be:
>
>  Sn-1 -> Sn qn
>
> ...where q1 is a typed staticly-sized list or tuple, and the index /n/
> varies according to which quotation accepts it. And S0 = R (the
> starting stack).

Ah, I see. I think you're saying that the gatherer, given some stack  
R, returns some stack S with some first-class stack 'T' on top:

    R -> S {T}

That is easy to handle. If that's not exactly what you were saying,  
this should be roughly equivalent in functionality at least.

> (I'm not a typing expert; probably a list is the wrong structure;

> if you type tuples, use those instead. The size must be static.)


Yes, it's no trouble handling first-class stacks. For example:

    new   :: R -> R {0}              -- 0 is the empty row
    push  :: R {S} x -> R {S x}
    pop   :: R {S x} -> R x
    infra :: R {S} [S -> T] -> R {T}

> The quotation, when it runs, will see ONLY the items the gatherer put
> onto that list.

Right. Makes sense.

> Combiner: Un tn -> Wn
> The last combiner, when run, produces W as its result stack (in this
> case, W=W2).
> Final: R -> W
>
> I think I've eliminated all type concatenation

Yes, you have. What you've suggested is already typeable. Below is the  
type for your combinator; the first quotation is the gatherer, the  
second is the combiner, and then the following two are the quotations  
in the middle:

    R [R -> S {T}] [S {U} {V} -> W] [T -> U] [T -> V] -> W

I had to modify your design slightly. As odd as it might seem, the  
combiner must be allowed to access the result of the gatherer below  
the top element (which is the first class stack).

Alternatively, you could drop the combinator and just return the  
stacks directly (which is essentially just as useful as you could  
always compose your own combiner at the end):

    R [R -> S {T}] [T -> U] [U -> V] -> R {S} {T}

This combinator can be implemented as such:

    [i] 2dip [[infra] papply] bi@ bi

Or, with the combiner:

    rot [i] 2dip [[infra] papply] bi@ bi i

I came up with something very similar to your combinator a couple of  
months ago. It's what motivated me to try dealing with alternative  
data structures: It all works great, but pulling the values out of the  
stacks at the end is a pain in the ass. The [( )] combinator I  
proposed is essentially the same as yours except that it automatically  
converts the top element to a stack for you if necessary and  
automatically converts single element stacks in the output to just the  
elements they contain. The auto-coercion makes things less painful,  
but unfortunately I don't know how to type it. The semantics are  
awkward anyway.

> If tuples were statically internally typed "unstack" would be  
> possible... Right?

Joy's 'stack' and 'unstack' can be given types:

    stack   :: R -> R {R}
    unstack :: R {S} -> S

The problem had to do with the fact that you can't tell from unstack's  
type how many elements it would add or remove relative to the input  
stack. This is something I had to know to type the combinator I  
mistakenly thought you were proposing. Given that you're not proposing  
them though, forget I said anything! The 'stack' and 'unstack'  
primitives work fine.

- John