[stack] Re: Concatenative Research

--- In [email protected], John Nowak <john@...> wrote:
> I guess my point is that you can see concatenative languages as "just" your usual higher-order eager language with a different syntax for composition and lambda abstraction (e.g. '[f g] == (:) (\s -> (g . f) s)', with the eta-expansion there to delay evaluation). Since the difference is simply syntax, I'm not sure why the semantics would require special treatment.

You might be right. In fact, it may follow that my semantics can be thought of in terms of the lambda calculus. I'll ponder that. But couldn't one also view the concatenative calculus as an alternative to the lambda calculus which may in some circumstances prove more elegant? After all, there's no variables (and the accompanying alpha-renaming), no function application (and the accompanying order-of-evaluation questions), and even no function abstraction if you don't want it.


> I should mention that I assume quotations form a proper opaque abstraction (as in lambda calculus) and are not dissectible (as in Joy). My above semantics for quotation doesn't work for Joy and instead describing the semantics for 'i' would be the interesting part. I've been on the record many times now though as saying those semantics are undesirable for a programming language; the ability to form new abstractions is critical.

Agreed! Quotations should be opaque, functions should be unable to gauge the depth of the stack, and functions should be unable to discern anything about the parts of the program following them.


> >> Typing a concatenative language is straightforward. You introduce a new kind 'Stack_K' and an inductively-defined type 'Stack' of kind 'Stack_K' that's either 'Empty' or a 'Cons' of a value with kind '*' and another 'Stack'. Your arrow constructor then has kind 'Stack_K -> Stack_K -> *' and quotation is kinded '* -> *' with type 'forall a b (c :: Stack_K). (a -> b) -> c -> Cons (a -> b) c'.
> > 
> > Aha, that is a good way of looking at it. Have you written anything along these lines? I would be interested in reading it.
> 
> I've not, although I probably should before someone else does! Then again, there are only about 3 people interested in this problem...

Here, I've just written something up on types & kinds. It's based on your suggestion, in conjunction with what I had been thinking when I wrote the type inferencer.
http://dl.dropbox.com/u/17328602/concat/lang//medium/algorithm/types.pdf


> I think the cyclic types you're proposing, commonly called "equirecursive types", are unnecessary. The 'dup apply' combinator is basically equivalent to the 'm' combinator in lambda calculus (i.e. '\x -> x x'). This is ill-typed in most typed systems. O'Caml will permit it with the "-rectypes" flag (which enables equirecursive types), but that flag is disabled by default and for good reason: It adds little utility and makes for some ugly type errors.

And here I was thinking that "cyclic types" hadn't been well-studied.


> If you're interested in typing combinators like 'dup apply', I think intersection types are a more interesting approach:
> 
>    dup apply : for all a b c d. Cons ((b -> c) /\ (Cons (b -> c) a -> d)) a -> d
> 
> If you read that carefully, it should make sense. I believe Slava put the basis of the idea in my head originally. Of course, the problem with this approach is that you now have intersection types to contend with.  Again, for a practical system, I don't think it's worth it.

That certainly works. Do you know which is more powerful, equirecursive or intersection types?


> The last thing I'll point out with respect to the type system is that, due to recursive function calls working on a list that represents the entire program state (and not just its "arguments"), you have quite a lot of polymorphic recursion; any recursive function where the recursive call occurs on a stack that has "grown" is polymorphic recursive. You could try to infer some cases of this (Milner-Mycroft), but the problem is undecidable in general. I think requiring type signatures on many recursive functions would therefore be a requirement. It's not one that I consider particularly onerous however.

Wait, are you saying that typing a typical concatenative language (which allows functions to recursively grow the data stack) is undecidable?