Lambda the Ultimate

I think first you should try to understand the existing literature so that you can state as clearly as possible what it is you're contributing. If your main contribution is a type system, then I'd think a soundness proof would probably be in order.

So far it appears to me that the contribution of Cat is that it is a statically typed stack based function language based on the SK calculus rather than the Lambda calculus. Unfortunately I am not yet convinced others would see it the same way (my viewpoint is colored by my inexperience).

I have the view that the presentation of a programming language with novel semantics, is interesting in of itself even if the outline is incomplete. Hopefully others would feel similarly.

Nonetheless, I plan to continue reading, studying, and discussing the subject. Perhaps I'll be able to make a coherent argument for the contribution of Cat to the literature other than "ain't it neat" ;-)

I couldn't understand the typing around 'eval'. I'd think you'd need some form of meta-level typing for typing quoted terms. Is this what your * notation accomplishes?

Since I wrote the original documentation, Andreas Rossberg showed me that Cat actually requires a kind system. There are types and stacks (which are a variation on rows). So a:any represents a type variable, and a:any* represents a stack variable.

To be honest the current documentation is very weak. The more literature I read the more I realize this. The next draft of the technical report should be much more coherent in explaining the type of "eval" and other core primitives.

I didn't see much justification for the "second stack." If that's novel then I would justify it well.

Thanks for letting me know. I'll attempt to do that in the paper. If you are interested in an informal explanation, I've posted an entry about it on my blog.

So far it appears to me that the contribution of Cat is that it is a statically typed stack based function language based on the SK calculus rather than the Lambda calculus. Unfortunately I am not yet convinced others would see it the same way (my viewpoint is colored by my inexperience).

One way to demonstrate that point would be to start with a definitional interpreter (or other reasonably formal semantic description) for SK calculus, and show what's needed to change it into some core version of Cat. This doesn't necessary prove anything formal, except in the case of an exact equivalence, since by arbitrary additions and subtractions you can change anything into anything. But it will provide a more formal characterization of the relationship between the two.

I'll give it my old college try. Hopefully you'll be willing to provide some input to the product? :-)

Sure, within reason.

Oops - I actually intended to write 'If that's novel then I would justify it AS well'. Little difference I suppose - I'm told that if it's worth doing, it's worth doing well :).

I don't see how to make the row variable idea work - I'd be interested to see your type system when you get it documented. (What's the type of eval?)

Regarding the second stack: In the blog entry you linked, you note that Joy doesn't use a second stack, but then at the end speculate that a second stack is needed to make the language turing complete. I'm clearly missing something. Is a second stack required to implement 'dip' in Joy, and you're just exposing it for other uses?

To implement dip, linrec and similar combinators in Joy you'd need to expose the second stack to the user. Joy takes the approach of having these combinators written in the implementation language. I suspect Cat allows the user to write these type of combinators in Cat itself. Factor takes the same approach, exposing the second stack using Forth style >r and r> words.

I suspect Cat allows the user to write these type of combinators in Cat itself.

That is correct.

Is a second stack required to implement 'dip' in Joy, and you're just exposing it for other uses?

That is precisely it.

I don't see how to make the row variable idea work - I'd be interested to see your type system when you get it documented. (What's the type of eval?)

Hopefully I'll be able to share a preliminary draft with the group shortly. I'll look forward to your comments.

I've no idea about your experience in academic publishing, ...

None. I've written several articles for trade journals like the C++ Users Journal and Doctor Dobbs Journal, but academic writing is a whole other ballgame.

Also, it might be good to consider that getting a paper accepted that 'just' presents a programming language is rather difficult these days. Various recent programming language papers had quite some problems with getting papers accepted at major conferences. It is probably a better idea to abstract a bit from the concrete language that you have developed and discuss aspects of the design, or the underlying formalism.

This sounds like good advice, and it is much appreciated.

That is indeed useful stuff.