Lambda the Ultimate

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.

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 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.

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.]

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.

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...

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 :: (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.

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

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? :-)

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