typing higher-order concatenative languages with standard hindley-milner

[John Nowak]

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

[Christopher Diggins]

It can't infer much, and as Okasaki points out the whole system
doesn't work in practice for even tiny non-trivial programs.

On Sat, May 31, 2008 at 1:28 AM, John Nowak <john@...> 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
>
>

[John Nowak]

On May 31, 2008, at 1:36 AM, Christopher Diggins wrote:

> It can't infer much,

The system, as I am using it below, seems to do very well. Keep in  
mind that he's using it for an imperative forth-like language. We're  
using it for a functional Cat-like language. If you have an example of  
something Cat can infer using a combination of the functions below  
that the Haskell version cannot (ignoring self types), please put it  
forward. Otherwise, I'll have to waste my time finding the problems  
myself. :)

> and as Okasaki points out the whole system
> doesn't work in practice for even tiny non-trivial programs.

The efficiency issues, as far as I can tell, are only due to  
'begindef' and friends which are necessary to allow the postfix  
syntax. If you had a built-in postfix syntax, that becomes non-issue.  
The huge size of the types is, again, a purely syntactic issue.  
There's no reason they can't be rendered exactly the same as Cat's  
types, albeit without the need for rows. You just need to use the  
space as a left-associative pairing operator.

- John

[LittleDan]

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

[John Nowak]

On May 31, 2008, at 2:41 AM, Daniel Ehrenberg wrote:

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

You'd be right it seems!

     (#) = flip (.)
     push a s = (s, a)

     ...

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

     zerop :: Num a => (s, a) -> (s, Bool)
     zerop (s, a) = (s, a == 0)

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

     mul :: Num a => ((s, a), a) -> (s, a)
     mul ((s, a), b) = (s, a * b)

     sub :: Num a => ((s, a), a) -> (s, a)
     sub ((s, a), b) = (s, a - b)

     ifte :: (((s, Bool), s -> s1), s -> s1) -> s1
     ifte (((s, True),  f), _) = f s
     ifte (((s, False), _), g) = g s

     ...

     factorial = dup # zerop # (push (pop # push 1)) #
       (push (dup # push 1 # sub # factorial # mul)) # ifte

     Occurs check: cannot construct the infinite type: s = (s, a)
       Expected type: ((s, a), a) -> ((s, a1), a1)
       Inferred type: (s, a) -> (s, a1)

I should note that Cat cannot handle the definition of 'fact' either,  
incorrectly giving it the type 'A any -> A any'. Recursive definitions  
in a concatenative language are tricky. Fifth can however, so it  
doesn't appear to be anything fundamentally problematic. It may,  
however, be an example of where row variables are needed.

- John

[John Nowak]

On May 31, 2008, at 1:28 AM, John Nowak wrote:

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

Well, as we're seeing already, perhaps not. In particular, row  
variables may be required to handle recursive definitions properly.  
(Okasaki's paper does give a solution to this problem, but it's  
nothing you want to use. Perhaps there's a nice way of hiding it.)

In either case, there's a trivial restriction to allow a language with  
row variables and non-row polymorphic functions to have principal  
types. You simply disallow the unification of a row variable with a  
vector greater than length zero that is not also row polymorphic. In  
other words, you could restrict the type of (A -> B) to ( -> ), but  
not (a -> b c) or (b -> ). As such, the principal types property of HM  
is nothing to be excited about here. (I apologize for, on occasion,  
being easily excitable.) It is rather interesting though how close we  
can get in Haskell.

- John

[Christopher Diggins]

The type of factorial in Cat is correct.
Most mathematical operators return "any", because they are not bound
to specific types.
For example "mul" has type "(any any -> any)" whereas "mul_int" has
type "(int int -> int)".


On Sat, May 31, 2008 at 3:14 AM, John Nowak <john@...> wrote:

>
> On May 31, 2008, at 2:41 AM, Daniel Ehrenberg wrote:
>
>> 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.
>
> You'd be right it seems!
>
> (#) = flip (.)
> push a s = (s, a)
>
> ...
>
> dup :: (s, a) -> ((s, a), a)
> dup (s, a) = ((s, a), a)
>
> zerop :: Num a => (s, a) -> (s, Bool)
> zerop (s, a) = (s, a == 0)
>
> pop :: (s, a) -> s
> pop (s, a) = s
>
> mul :: Num a => ((s, a), a) -> (s, a)
> mul ((s, a), b) = (s, a * b)
>
> sub :: Num a => ((s, a), a) -> (s, a)
> sub ((s, a), b) = (s, a - b)
>
> ifte :: (((s, Bool), s -> s1), s -> s1) -> s1
> ifte (((s, True), f), _) = f s
> ifte (((s, False), _), g) = g s
>
> ...
>
> factorial = dup # zerop # (push (pop # push 1)) #
> (push (dup # push 1 # sub # factorial # mul)) # ifte
>
> Occurs check: cannot construct the infinite type: s = (s, a)
> Expected type: ((s, a), a) -> ((s, a1), a1)
> Inferred type: (s, a) -> (s, a1)
>
> I should note that Cat cannot handle the definition of 'fact' either,
> incorrectly giving it the type 'A any -> A any'. Recursive definitions
> in a concatenative language are tricky. Fifth can however, so it
> doesn't appear to be anything fundamentally problematic. It may,
> however, be an example of where row variables are needed.
>
> - John
>
>

[John Nowak]

On May 31, 2008, at 3:48 AM, Christopher Diggins wrote:

> The type of factorial in Cat is correct.
> Most mathematical operators return "any", because they are not bound
> to specific types.
> For example "mul" has type "(any any -> any)" whereas "mul_int" has
> type "(int int -> int)".

Ah, very embarrassing. My mistake. Cat does indeed give the expected  
type when 'sub_int' and 'mul_int' are used.

Thanks for the correction.

- John