## Designing a Type Notation for a Stack Based Functional Language

I am designing a dialect of Joy called 'Big Cat'. Like Joy, Big Cat is a pure stack based functional language (or concatenative language, if you like the term). This means that every function takes a single stack as a parameter, and returns a new stack as a result. Most programs expect a certain stack configuration, so I am devising a syntax for expressing the desired type configuration.

One of the changes is the introducction of a type notation for operations. Here is my current proposal:

  swap (T, U) => (U, T);
dup (T) => (T, T);
dupN (int, T) => (T*);
pop (T) => ();
popN (int, T*) => ();
if (() => T, () => U, bool) => (U|T);


I welcome feedback, and suggestions. Let me know if the syntax is not intuitive and you need clarification, thanks!

## Comment viewing options

### you should include a way of

you should include a way of representing the rest of the stack. If I recall correctly, certain papers by greg morrisett and david walker should give you a good idea of how to do what is called Stack Polymorphism.

### Good point!

How about "_"? For example, a function which takes the top element and places it at the bottom of the stack:

TopToBottom (T, _) => (_, T);


Most of the time, the "rest-of-stack" marker is implicit. So:

Dup (T, _) => (T, T, _);


is equivalent to:

Dup (T) => (T, T);


I realized I haven't explicitly stated that in the proposed notation that the left-most element is the top of the stack.

### Interesting

Something interesting to me is that, since the language knows everything is in terms of the stack, these type annotations are very close to the actual action that the function does.

If you introduce a new layer of notation, you could almost skip the implementation

e.g.

TopToBottom (T, _) => (_, T);


You don't have to write the code for TopToBottom, since it can be inferred from the type information whereas

AddOneToTopThenStickOnBottom (T, _) => (_, T');


Since the type info states that T may not neccessarily be the same you have to write actual body of the function.

Likewise with dup, the type could completely describe the operation.

Another related thought is that type inference seems like it would be easy

I can't prove this rigorously, but I get the feeling the type could be determined using only the functions that have types equivalent to () => (T) (call it set a) and the first function in the chain that has a type equivalent to (T) => () (call it function b) and the last function.

You'd do something like pop the rhs of the first set of functions off the lhs of function b of functions. This would be the inferred lhs. The rhs would then be the rhs of the last function

If set a was interleaved throughout the function, you could decompose into multiple functions, infer those types and then use the result to infer the type of the final function. At least intuitively that's what it feels like.

### Implementation inference

Implementation inference from types appears possible on the surface, but it unfortunately isn't because a single type maps to multiple possible values.

On the other hand the type inference mechanism you propose does seem very feasable. It seems to me that this is essentially what they do in ML, but I'm not an expert in type inference systems.

### Parametricity

The issue is whether you view the 'T' as "parametrically polymorphic". As a common well-known example, the type (forall a.a→a) has only one (non-bottom) value (implementation). More relevant, the Haskell function,
dup :: (a, stk)→(a, (a, stk))
has only one implementation (ignoring bottoms again).

Of course as I've been implying this only holds for total and pure functions. Allowing side effects, essentially any side-effecting operations could be added without changing the type. If we view non-termination as a side-effect then this also covers the need for totality. That said, asking the implementation to generate the function from a type we can have it presume that you want the "obvious" pure total function, though, of course, even then there can easily not be a unique answer, e.g. swapOrId :: (a,a)→(a,a).

[Note: There is an edit I may make later; an addition.]

### I might be missing something important ...

So do the functions f(int x) = x + 1, g(int x) = x + 2 have the same type? I can buy into either answer, I just don't know what the mainstream answer is.

### Yes, they do...

But yes, you are missing something important... :)

Both of the functions you give have the same type, probably somthing like "int -> int" (depending on your interpretation of literals, addition, and so on). Note that this type is "monomorphic", in the sense that int is a specific, concrete type rather than a variable. In general, there may be an infinite number of functions with a monomorphic type like this one, depending on the operations defined on the type.

Things get more complicated (or is it simpler?) when you consider polymorphic types, like "α -> α" where α is a type variable rather than a concrete type. In a pure language with "parametric" polymorphism, there is only one function with this type. The word parametric in this context effectively means "type variables are black boxes": i.e., there's no way to say "if α = int, then..." or anything of that form. They're completely abstract. Once you see that, it's pretty easy to see that a type like α -> α can have only one implementation, or "inhabitant": since there is no conceivable way that the function can inspect its argument or construct a new value of the same (unknown) type, we can prove that any value with this type must be the identity function.

(Things might get slightly more complicated if you introduce primitive operators that are polymorphic in all types, but it won't change this example... For instance, if you have a primitive function typeName : α -> string, then it's possible for a function to inspect values of arbitrary type, but it's still not possible for a function to construct new values of arbitrary type.)

In any case, I'm not sure how clear this explanation is, but I hope it helps somewhat. It's in this sense that Logan and Derek have suggested that it ought to be possible to infer implementations from types in your language, and this is why Derek mentions the question of parametricity. For a very cool example of this in action, take a look at Djinn, which does this kind of thing for Haskell, and if you want to get quite technical, you'll have lots of fun here...

### Swap

Well, if you want swap to do the right thing you need to give it the type (a,b) -> (b,a). Or am I missing your point here?

### swap and parametricity

swap :: (a,a) -> (a,a) is a perfectly legitimate type for swap. You are correct that (a,b) -> (b,a) would force the function to be the swap function, but my point was simply that parametricity does not always force a unique choice. For example, every function, f, between natural numbers induces a parametrically polymorphic function rearrange f :: Stream a -> Stream a.

### Take a look at Factor

The Factor language is dynamically-typed, however it supports both stack effect and type inference. I haven't documented the particulars of the techniques used yet, but hope to do so soon.

### That looks quite cool, good

That looks quite cool, good job. It looks like we are operating in the same space.

### 500

Internal Server Error, even though it worked for me ten minutes ago. I guess somehow it saw me reading AvS's old arguments 'against' concatenative languages? :-)

He has some papers on type checking of stack-based languages.

Actually, Forth convention of commenting stack behaviour irght next to defined word is quite sufficient (and is used by Jaanus):

: wordbeingdefined ( stack before -- execution after stack )
.....
;

### Thinking Forth

This discussion reminded me of Leo Brodie's "Starting Forth" and "Thinking Forth". The latter is available at http://home.earthlink.net/~lbrodie/forth.html

### Prior work

Robin Popplestone designed a static type checker for Pop-11, here ("Specifying Types by Grammars" and "A Typed Operational Semantics" -- I don't think I've read these papers, I just remember a comp.lang.forth discussion). "This approach is valuable for any language or system in which stacking operations are explicit, including the Forth, POP-11 and PostScript..."

### Typing

swap (foo::bar::rest) = bar::foo::rest

etc.

(you probably want to change :: to some other stack "constructor")

### int and T*

After a procedure returning T*, such as "dupN" in the example, the type system will become useless. For static typed systems, the number of T's in the stack cannot be known, so the compiler cannot do type-checking or other usage from the types anymore. In the other hand, for dynamic typed systems (e.g. joy) and non-typed systems (e.g. forth), type notation is simple not necessary. The type information in such systems is only meaningful for human.

By the way, I have written two stack-like notation for Haskell(this and this). They are only modules therefore they use the powerful typing system in the Haskell language directly, i.e. static typed. I hope it can help you.