# typing higher-order concatenative languages with standard hindley-milner

## John Nowak — 2008-05-31 05:28:50

    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 — 2008-05-31 05:36:24

    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 — 2008-05-31 05:47:14

    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

## Daniel Ehrenberg — 2008-05-31 06:41:20

    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 — 2008-05-31 07:14:53

    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 — 2008-05-31 07:25:32

    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 — 2008-05-31 07:48:04

    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 — 2008-05-31 07:55:20

    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