[stack] typing higher-order concatenative languages with standard hindley-milner

Okasaki's paper "Techniques for Embedding Postfix Languages in  
Haskell" shows how to implement a crude Forth-like language in  
Haskell. I won't go over how it works here, but you should be able to  
gather what's happening just by looking at the examples below.

Unfortunately, the language discussed is a first-order language, not a  
higher-order language like Joy, Cat, Factor, etc. It turns out that  
extending the language is trivial. For example, here are quite a few  
common functions, some of which are higher order ('swap' and 'dup' are  
taken from the paper):

     swap :: ((s, a), b) -> ((s, b), a)
     swap ((s, a), b) = ((s, b), a)

     dup :: (s, a) -> ((s, a), a)
     dup (s, a) = ((s, a), a)

     quote :: (s, a) -> (s, s1 -> (s1, a))
     quote (s, a) = (s, \s1 -> (s1, a))

     i :: (s, s -> s1) -> s1
     i (s, f) = f s

     dip :: ((s, a), s -> s1) -> (s1, a)
     dip ((s, a), f) = (f s, a)

     keep :: ((s, a), (s, a) -> s1) -> (s1, a)
     keep ((s, a), f) = (f (s, a), a)

     compose :: ((s, a -> b), b -> c) -> (s, a -> c)
     compose ((s, f), g) = (s, g . f)

Additionally, we need a 'push' function that will let us put values  
(including quotations) on the stack directly:

     push :: a -> s -> (s, a)
     push a s = (s, a)

We can then use these functions via the composition operator (as  
expected perhaps). For example, we can write Cat and Factor's  
(unfortunately named?) 'curry' function as such:

     -- equivalent to '[quote] dip compose'
     curry :: ((s, a), (s1, a) -> b) -> (s, s1 -> b)
     curry = compose . dip . push quote

This all seems to work fairly well. What's interesting is that it  
breaks down in the same places that Fifth's current system breaks  
down. For example, here's our 'bi@' combinator once again:

     -- equivalent to Factor's '[dip] keep call'
     bi_at = i . keep . push dip

This gets the unfortunate type '(((s, a), a), (s, a) -> s) -> s'. This  
is equivalent to the Fifth type 'S a a (S a -> S) -> S'! It's the  
exact same problem. We can try my backwards 'bi@' combinator (which  
calls the quotation on the top element first, unlike Factor) as well:

     -- equivalent to 'dup dip dip'
     bi_at_backwards = dip . dip . dup

This gets the type '(s, s -> (s, a)) -> ((s, a), a)'. This is  
equivalent to the Fifth type 'S (S -> S a) -> S a a'! Again, the exact  
same problem.

What's very interesting to note here is that we're getting the same  
results as Fifth *without* the need for row variables. Perhaps row  
variables are not necessary?

What about fixed-arity combinators? We know that we need these in  
order to handle callbacks, infra, things like 'bi@', and so on. For  
example, here's a version of 'dip' that only works with quotations of  
arity 1->1:

     -- used to represent the bottom of the stack
     data Bot = Bot

     -- the type signature is *required* here otherwise we get this  
overly
     -- general type: (((s, a), b), (Bot, a) -> (c, d)) -> ((s, d), b)
     -- the type below is equivalent to 'S a b (a -> c) -> S c b'
     dip1_1 :: (((s, a), b), (Bot, a) -> (Bot, c)) -> ((s, c), b)
     dip1_1 (((s, a), b), f) = ((s, snd (f (Bot, a))), b)

We can then use this to write my backwards 'bi@' combinator such that  
you can actually use it properly:

     bi_at_backwards_yet_useful = dip1_1 . dip1_1 . dup

This gets the type '(((s, a), a), (Bot, a) -> (Bot, b)) -> ((s, b),  
b)'. This type is equivalent to the Fifth type 'S a a (a -> b) -> b  
b', and hence, this version of 'bi@' is useful!

There's something very important to note here: It is impossible to  
write 'dip1_1' simply by restricting the type of 'dip' as it is in  
Fifth. This is because Haskell is based on Hindley-Milner and has  
principal types. Since 'dip1_1 dip1_1 dup' and 'dip dip dup' yield  
types such that neither is more general than the other, it roughly  
follows that neither the type of 'dip1_1' or 'dip' is more general  
than the other, and hence restricting 'dip' to yield 'dip1_1' is not  
possible.

In short, it seems standard Hindley-Milner alone is enough to do  
everything we want! As a downside, we need several versions of fixed- 
arity higher order combinators like 'dip' and 'i'. This is not a  
problem as the general versions can be used in cases where there's no  
need for fixed arities (i.e. most of them). This gives us a  
concatenative language that's truly useful and never requires type  
annotations.

Down with row polymorphism! Well, maybe not quite yet. I still have a  
few more things to look into. This does, at least, seem to be very  
promising.

- John