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

Can this work for things that use the data stack with a statically
unknown depth? For example if factorial is defined like

: factorial ( n -- n! )
    dup zero? [ drop 1 ] [ dup 1 - factorial * ] if ;

it seems like it should be impossible for Haskell to come up with a type for it.

Dan

On Sat, May 31, 2008 at 12:28 AM, John Nowak <[email protected]> wrote:
> 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
>
>