John Nowak — 2008-11-19 14:13:33

Hello all. One of the problems I've run into with a second-order
language is that you don't get partial application. (I've recently
been able to extend the intersection-based type system to a higher
order language, so this second-order restriction may not last anyway.)

Essentially, the problem is something like this. Let's say I want to
write a function that has this effect:

('a0 .. 'aN) 'x -> ('a0 F 'x G .. 'aN F 'x G) 'x

In other words, given a list of objects 'a0 to 'aN and some object 'x,
we want to map over the list applying some function F to each element,
followed by applying G with 'x on the stack. We want to keep 'x around
at the end. An implementation in Cat would look as such:

pick [[quote [dip] compose] dip compose papply map] dip

We can demonstrate its correctness as follows:

('a0 .. 'aN) 'x [F] [G] pick [[quote [dip] compose] dip compose papply
map] dip
('a0 .. 'aN) 'x [F] [G] 'x [[quote [dip] compose] dip compose papply
map] dip
('a0 .. 'aN) 'x [F] [G] [quote [dip] compose] dip compose papply map 'x
('a0 .. 'aN) 'x [F] quote [dip] compose [G] compose papply map 'x
('a0 .. 'aN) 'x [[F]] [dip] compose [G] compose papply map 'x
('a0 .. 'aN) 'x [[F] dip] [G] compose papply map 'x
('a0 .. 'aN) 'x [[F] dip G] papply map 'x
('a0 .. 'aN) ['x [F] dip G] map 'x
('a0 F 'x G .. 'aN F 'x G) 'x

This works fine (there may be an nicer way to write it), but there are
two problems. One, it's too complicated. The same thing with named
variables (i.e. naming 'x and lifting it into the function) is *much*
more direct (where \ is a lambda of sorts):

('a0 .. 'aN) 'x \y. [F y G] map
('a0 .. 'aN) [F 'x G] map
('a0 F 'x G .. 'aN F 'x G) 'x

Two, there's no way to do it in a second order language as we're
relying on higher order functions.

The solution seems to be to introduce a retain stack a la Forth (and
Factor). Here, we indicate the value of the retain stack by placing it
to the right of the dot. '+r' copies the top element of the retain
stack to the data stack:

('a0 .. 'aN) 'x >r map[F +r G] r>
('a0 .. 'aN) map[F +r G] r> . 'x
('a0 F +r G .. 'aN F +r G) r> . 'x
('a0 F 'x G .. 'aN F 'x G) r> . 'x
('a0 F 'x G .. 'aN F 'x G) 'x

It's worth nothing here that we can only evaluate as such because
we're assuming F, G, and map do not alter the retain stack. This is
something a compiler could easily enforce by tracking the retain stack
on the type level and disallowing named functions or arguments to a
combining form from using elements already on the retain stack at the
time they're called. An annotation could be used to bypass this
restriction.

Considering how much simpler this is than the version without the
retain stack, I'm wondering if Joy and Cat are missing something by
not offering that second stack. Here's how the retain stack version
might work in Joy:

('a0 .. 'aN) 'x r> [F +r G] map r>
('a0 .. 'aN) [F +r G] map r> . 'x
('a0 F +r G .. 'aN F +r G) r> . 'x
('a0 F 'x G .. 'aN F 'x G) r> . 'x
('a0 F 'x G .. 'aN F 'x G) 'x

Any thoughts or am I just rambling?

- John

On Nov 19, 2008, at 9:13 AM, John Nowak wrote:

> ('a0 .. 'aN) 'x \y. [F y G] map
> ('a0 .. 'aN) [F 'x G] map
> ('a0 F 'x G .. 'aN F 'x G) 'x

Minor correction:

('a0 .. 'aN) 'x \y. [F y G] map y
('a0 .. 'aN) [F 'x G] map 'x
('a0 F 'x G .. 'aN F 'x G) 'x

William Tanksley, Jr — 2008-11-23 19:43:18

John Nowak <john@...> wrote:

> (I've recently
> been able to extend the intersection-based type system to a higher
> order language, so this second-order restriction may not last anyway.)

Even a fan of lower-order logic like myself can applaud this result. Good luck!

> The solution seems to be to introduce a retain stack a la Forth (and
> Factor). Here, we indicate the value of the retain stack by placing it
> to the right of the dot. '+r' copies the top element of the retain
> stack to the data stack:

Interestingly, Factor just eliminated its retain stack words. This
makes sense for them, since they've always been higher-order.

I really like the return stack (which is a retain stack on which
return addresses are stored) in Forth. When combined with the
appropriate vocabulary, it gives the low-level programmer the ability
to abstract control flow and data manipulations in an immense number
of ways. Without doubt, it's the most flexible and general approach
known.

The main problem is that it's very low-level. As you noted, it's
possible to use a typechecker to enforce proper usage, but it's more
more graceful to abstract it so that it's impossible to make those
errors. "dip" is one way of doing that. (Technically, locals are a
different abstraction of the same thing, but they're not really a
comfortable "fit" for a concatenative language.) Factor's "fry"
vocabulary is another solution.

It would be interesting to explore whether any better solutions exist.

> Considering how much simpler this is than the version without the
> retain stack, I'm wondering if Joy and Cat are missing something by
> not offering that second stack. Here's how the retain stack version
> might work in Joy:

I think Joy has a good reason to not offer the retain stack. It's
certainly not essential; it's merely handy. And Joy is an experimental
language in very many ways.

But I think you've pointed out an essential weakness of dip.

> - John

-Wm

John Meacham — 2008-11-24 22:57:31

On Sun, Nov 23, 2008 at 11:43:18AM -0800, William Tanksley, Jr wrote:

> John Nowak <john@...> wrote:
> > (I've recently
> > been able to extend the intersection-based type system to a higher
> > order language, so this second-order restriction may not last anyway.)
>
> Even a fan of lower-order logic like myself can applaud this result. Good luck!
>
> > The solution seems to be to introduce a retain stack a la Forth (and
> > Factor). Here, we indicate the value of the retain stack by placing it
> > to the right of the dot. '+r' copies the top element of the retain
> > stack to the data stack:
>
> Interestingly, Factor just eliminated its retain stack words. This
> makes sense for them, since they've always been higher-order.

Wouldn't a retain stack only give one just one order more expressive
power? as in, you have second order, and a psuedo third order (with a
different semantics/syntax) due to retain stack use. Sort of like axiom
schemas allow you to express some things that would normally require
second order logic in first order logic, but they are just shy of
actually being second order constructs. The value of retain stacks seems
dubious to me in this case.

explicit lambda forms seem to take care of all the cases that I have
seen retain stacks used, and they can be desugared quite
strightforwardly to the underlying concatenative language and don't
muddy the run-time semantics as they are simply a source -> source
transformation.

John

--
John Meacham - ⑆repetae.net⑆john⑈

John Nowak — 2008-11-25 02:11:47

On Nov 24, 2008, at 5:57 PM, John Meacham wrote:

> explicit lambda forms seem to take care of all the cases that I have
> seen retain stacks used

An additional benefit of retain stacks arises in the case of linear
types. Because it is easy to shuffle objects onto and off of the
retain stack, it's easy (or easier anyway) to keep values linearly
referenced. With lambdas, things get more complex. Additionally, you
suddenly have a capacity to "lift" arguments into functions which you
do not have with the retain stack. This brings its own share of
benefits and drawbacks.

> and they can be desugared quite strightforwardly to the underlying
> concatenative language

This is only the case in a higher order language (with a sufficiently
flexible type system). As it stands now, I'm still working with a
second order language, so such a desugaring is unfortunately not
possible. Adding lambdas requires extending the semantics.

I do think you're right that the retain stack is a poor option. After
some thought, I'm no longer considering it. A "resource-aware" lambda
seems like a better option for dealing with objects that must remain
singly referenced. Unfortunately, in order to operate on such objects
without excessive copying, it becomes necessary to remove objects from
their "slots" and to re-insert them after performing the operation.
This means we cannot use a simple substitution semantics and become
dependent on evaluation order.

I could offer a limited lambda that cannot lift objects into
functions. It would be possible to desugar in such a case and
explaining the rules with respect to linearity would be easy. It's not
clear how useful this is however; I'd expect not much.

If it's not clear, I manage to make a lot of problems for myself. It's
probably time to go with a more conservative (i.e. already
demonstrated to be useful), higher order, and persistent (as opposed
to linear) approach. My brain hurts too much this way.

- John

John Meacham — 2008-11-25 02:43:44

On Mon, Nov 24, 2008 at 09:11:47PM -0500, John Nowak wrote:

> > and they can be desugared quite strightforwardly to the underlying
> > concatenative language
>
> This is only the case in a higher order language (with a sufficiently
> flexible type system). As it stands now, I'm still working with a
> second order language, so such a desugaring is unfortunately not
> possible. Adding lambdas requires extending the semantics.

What type system are you currently using? Is your restriction to second
order due to your inference algorithm or something more fundamental to
the internals of your implementation? Is your intermediate
representation typed? I have been a big fan of the impredicative boxy
types alogorithm for inference

http://research.microsoft.com/~simonpj/papers/boxy/

which can support arbitrary rank polymorphism and is really
straightforward to implement. Since explicit recursive definitions or
definitions at all really are relatively rare in concatenative
languages, perhaps using this algorithm will allow functions to 'push'
the apppropriate higher order types downward so explicit annotations
arn't needed in general.

John

--
John Meacham - ⑆repetae.net⑆john⑈

John Nowak — 2008-11-25 08:12:12

On Nov 24, 2008, at 9:43 PM, John Meacham wrote:

> Is your restriction to second order due to your inference algorithm
> or something more fundamental to the internals of your implementation?

It was both, but now it's just the latter. Well, that, and certain
things are just easier to handle when first class functions aren't
involved.

> What type system are you currently using?

The higher order variant is similar to Cat's in that it uses row
variables to represent the stack. It adds intersection types in order
to give the language (I believe) principal typings. Here are a couple
of examples which might make a rough kind of sense:

twice : A [A -> B /\ B -> C] -> C
twice = dup dip i

m : A [A [B -> C] -> D /\ B -> C] -> D
m = dup i

> perhaps using this algorithm will allow functions to 'push' the
> apppropriate higher order types downward so explicit annotations
> arn't needed in general.

This is essentially what I'm doing with intersections.

Thanks for the suggestions.

- John