[RFC] Cat: A Typed Functional Stack Based Language

I have posted a near final draft (in PDF and PS format) of my paper on the semantics of Cat at http://www.cat-language.com/paper.html, and I wanted to make a public request for comments.

Here is the abstract:

Cat: A Typed Functional Stack Based Language

Stack-based application languages, such as Forth and Postscript,
traditionally have provided little or no support for functional programming and have lacked a formal static type system. This changed when Manfred von Thun introduced Joy, a functional stack-based language,
and Stephan Becher provided an implementation of StrongForth, a
dialect of Forth with an informal type system. This paper introduces
the semantics and type system for a pure functional programming
language which is entirely stack based.

By the way Lambda-the-Ultimate.org is already acknowledged for the boundless help everyone has provided me so far. Thank you!

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

The type of quote

The papers says the type of quote is ('a -> ( -> 'a)), but shouldn't that be ('A -> ( -> 'A)), i.e. a stack variable instead of a type variable?

Quote is typed correctly

The type annotation is correct because the "quote" primitive only quotes a single item on the stack. You can also quote an expression using "[ ... ]", the type of which is expressed in the abstract syntax. Perthaps this was the source of confusion? The english translation of the T-QUOTE typing rule is roughly:

if a program p has type ('A -> 'B) then [p] has type ( -> ('A -> 'B))

Does this make sense? Thanks for looking at the paper. I'd love to hear any other comments you have.

my comments

page 2:
"Pure stack-based application programming languages, such as Forth [6], DC
[1], Postscript [7], Joy [3] and others, have been in continuous usage for at
least 40 years." - Forth is from the 70s and Postscript is later, so I think you're mistaken.
'escribed'
Inconsistent usages:
imperative vs. procedural
type system vs. type-system
well typed vs. well-typed

I'm entirely unconvinced by the argument in your second to last paragraph.
It also seems odd not to give the titles of books, but maybe that's just me.

Age of stack-based languages

Hi David,

Thank you for corrections. I also agree that I should add the titles of books. After more research, I realized that the time-span of stack-based languages is over-stated. The first Forth paper appeared in 1970 and I believe was essentially the same as the language Mohasco which was first implemented in 1968 (http://colorforth.com/HOPL.html). The predecessors of Mohasco ( RSI, SLAC ) aren't clear to me to be examples of stack-based langauge. Either way I will definitely rephrase the sentence to be non-contentious. Thanks!

I'm not sure imperative vs

I'm not sure imperative vs procedural is necessarily an inconsistency - I'd take procedural to refer to a more specific paradigm whereas OO is also typically imperative, for example.