## Concatenative Programming; The Free Monoid of Programming Languages

This post demonstrates a simple encoding of a (typed) concatenative language in Haskell.

Point-free style is one of the distinctive markers of functional programming languages. Want to sum a list? That’s as easy as:

`sum = foldr (+) 0`

Now I want to sum every number after adding one to it.

`= foldr (+) 0 . map ((+) 1) sumSuccs `

One more step to make this function truly abstract™ and general™: we’ll allow the user to supply their own number to add

`= foldr (+) 0 . map . (+) sumAdded `

And here the trouble begins. The above expression won’t actually type check. In fact, it’ll give a pretty terrible error message:

```
• Non type-variable argument in the constraint: Num [a]
(Use FlexibleContexts to permit this)
• When checking the inferred type
sumThoseThat :: forall a.
(Num [a], Foldable ((->) [a])) =>
a -> [a]
```

I remember as a beginner being confused by similar messages. What’s
`FlexibleContexts`

? I had thought that the “point-free style”
just meant removing the last variable from an expression if it’s also
the last argument:

```
sum xs = foldr (+) 0 xs
sum = foldr (+) 0
```

Why doesn’t it work here?

Well, it doesn’t work because the types don’t line up, but I’m going
to try and explain a slightly different perspective on the problem,
which is *associativity*.

To make it a little clearer, let’s see what happens when we point-fill the expression:

```
= (foldr(+) 0 . (map . (+))) n xs
sumAdded n xs => foldr(+) 0 ((map . (+)) n) xs
=> foldr(+) 0 (map ((+) n)) xs
```

Indeed, the problem is the placement of the parentheses. What we want at the end is:

`=> foldr(+) 0 (map ((+) n) xs) `

But, no matter. We have to jiggle the arguments around, or we could use something terrible like this:

```
infixr 9 .:
.:) = (.).(.)
(
= foldr (+) 0 .: map . (+) sumAdded
```

Is there something, though, that could do this automatically?

# Associativity

We run into a similar problem in Agda. We’re forever having to prove statements like:

```
(x + y) + z ≡ x + (y + z)
0 x ≡ x +
```

There are a couple of ways to get around the issue, and for monoids
there’s a rich theory of techniques. I’ll just show one for now, which
relies on the *endomorphism* monoid. This monoid is created by
partially applying the monoid’s binary operator:

```
: Set
Endo = ℕ → ℕ
Endo
_⇑⟧ : ℕ → Endo
⟦= n + m ⟦ n ⇑⟧ m
```

And you can get back to the underlying monoid by applying it to the neutral element:

```
_⇓⟧ : Endo → ℕ
⟦= n 0 ⟦ n ⇓⟧
```

Here’s the important parts: first, we can lift the underlying operation into the endomorphism:

```
_⊕_ : Endo → Endo → Endo
= λ x → xs (ys x)
xs ⊕ ys
: ∀ n m → ⟦ ⟦ n ⇑⟧ ⊕ ⟦ m ⇑⟧ ⇓⟧ ≡ n + m
⊕-homo = cong (n +_) (+-identityʳ m) ⊕-homo n m
```

And second, it’s *definitionally* associative.

```
: ∀ x y z → (x ⊕ y) ⊕ z ≡ x ⊕ (y ⊕ z)
⊕-assoc _ _ _ = refl ⊕-assoc
```

These are all clues as to how to solve the composition problem in the Haskell code above. We need definitional associativity, somehow. Maybe we can get it from the endomorphism monoid?

# State

You’re probably familiar with Haskell’s state monad:

`newtype State s a = State { runState :: s -> (a, s) }`

It can help a lot when you’re threading around fiddly accumulators and so on.

```
nub :: Ord a => [a] -> [a]
= go Set.empty
nub where
= []
go seen [] :xs)
go seen (x| x `Set.member` seen = go seen xs
| otherwise = x : go (Set.insert x seen) xs
```

```
nub :: Ord a => [a] -> [a]
= flip evalState Set.empty . go
nub where
= pure []
go [] :xs) = do
go (x<- gets (Set.member x)
seen if seen
then go xs
else do
modify (Set.insert x):) <$> go xs (x
```

Of course, these days state is a transformer:

`newtype StateT s m a = StateT { runStateT :: s -> m (a, s) }`

This lets us stack multiple effects on top of each other: error
handling, IO, randomness, even another state monad. In fact, if you
*do* stack another state monad on top, you might be surprised by
the efficiency of the code it generates:

```
type DoubleState s1 s2 a = StateT s1 (State s2) a
=> s1 -> State s2 (a, s1)
=> s1 -> s2 -> ((a, s1), s2)
```

It’s nothing earth shattering, but it inlines and optimises well. That output is effectively a left-nested list, also.

# Multi-State

If we can do one, and we can do two, why not more? Can we generalise the state pattern to an arbitrary number of variables? First we’ll need a generic tuple:

```
infixr 5 :-
data Stack (xs :: [Type]) :: Type where
Nil :: Stack '[]
(:-) :: x -> Stack xs -> Stack (x : xs)
```

Then, the state type.

`newtype State xs a = State { runState :: Stack xs -> (a, Stack xs) }`

We can actually clean the definition up a little: instead of a tuple at the other end, why not push it onto the stack.

`newtype State xs a = State { runState :: Stack xs -> Stack (a : xs) }`

In fact, let’s make this as polymorphic as possible. We should be able to change the state is we so desire.

```
infixr 0 :->
type (:->) xs ys = Stack xs -> Stack ys
```

And suddenly, our endomorphism type from above shows up again.

We can, of course, get back our original types.

`newtype State xs a = State { runState :: xs :-> a : xs }`

And it comes with all of the instances you might expect:

```
instance Functor (State xs) where
fmap f xs = State (\s -> case runState xs s of
:- ys) -> f x :- ys)
(x
instance Applicative (State xs) where
pure x = State (x :-)
<*> xs = State (\s -> case runState fs s of
fs :- s') -> case runState xs s' of
(f :- s'') -> f x :- s'')
(x
instance Monad (State xs) where
>>= f = State (\s -> case runState xs s of
xs :- ys -> runState (f y) ys) y
```

# Polymorphism

But what’s the point? So far we’ve basically just encoded an unnecessarily complicated state transformer. Think back to the stacking of states. Written in the mtl style, the main advantage of stacking monads like that is you can write code like the following:

```
pop :: (MonadState [a] m, MonadError String m) => m a
= get >>= \case
pop -> throwError "pop: empty list"
[] :xs -> do
x
put xs pure x
```

In other words, we don’t care about the rest of `m`

, we
just care that it has, somewhere, state for an `[a]`

.

This logic should apply to our stack transformer, as well. If it only cares about the top two variables, it shouldn’t care what the rest of the list is. In types:

```
infixr 0 :->
type (:->) xs ys = forall zs. Stack (xs ++ zs) -> Stack (ys ++ zs)
```

And straight away we can write some of the standard combinators:

```
dup :: '[a] :-> '[a,a]
:- xs) = (x :- x :- xs)
dup (x
swap :: '[x,y] :-> '[y,x]
:- y :- xs) = y :- x :- xs
swap (x
drop :: '[x,y] :-> '[y]
drop (_ :- xs) = xs
infixl 9 !
! g) x = g (f x) (f
```

You’ll immediately run into trouble if you try to work with some of the more involved combinators, though. Quote should have the following type, for instance:

`quote :: (xs :-> ys) -> '[] :-> '[ xs :-> ys ]`

But GHC complains again:

```
• Illegal polymorphic type: xs :-> ys
GHC doesn't yet support impredicative polymorphism
• In the type signature:
quote :: (xs :-> ys) -> '[] :-> '[xs :-> ys]
```

I won’t go into the detail of this particular error: if you’ve been
around the block with Haskell you know that it means “wrap it in a
newtype”. If we do *that*, though, we get yet more errors:

`newtype (:~>) xs ys = Q { d :: xs :-> ys }`

```
• Couldn't match type ‘ys ++ zs0’ with ‘ys ++ zs’
Expected type: Stack (xs ++ zs) -> Stack (ys ++ zs)
Actual type: Stack (xs ++ zs0) -> Stack (ys ++ zs0)
NB: ‘++’ is a type function, and may not be injective
```

This injectivity error comes up often. It means that GHC needs to prove that the input to two functions is equal, but it only knows that their outputs are. This is a doubly serious problem for us, as we can’t do type family injectivity on two type variables (in current Haskell). To solve the problem, we need to rely on a weird mishmash of type families and functional dependencies:

```
type family (++) xs ys where
++ ys = ys
'[] : xs) ++ ys = x : (xs ++ ys)
(x
class (xs ++ ys ~ zs) => Conc xs ys zs | xs zs -> ys where
conc :: Stack xs -> Stack ys -> Stack zs
instance Conc '[] ys ys where
= ys
conc _ ys
instance Conc xs ys zs => Conc (x : xs) ys (x : zs) where
:- xs) ys = x :- conc xs ys
conc (x
infixr 0 :->
type (:->) xs ys = forall zs yszs. Conc ys zs yszs => Stack (xs ++ zs) -> Stack yszs
```

And it does indeed work:

```
pure :: a -> '[] :-> '[a]
pure = (:-)
newtype (:~>) xs ys = Q { d :: xs :-> ys }
quote :: (xs :-> ys) -> '[] :-> '[ xs :~> ys ]
= pure (Q x)
quote x
dot :: forall xs ys. ((xs :~> ys) : xs) :-> ys
:- xs) = d x xs
dot (x
true :: (xs :~> ys) : (xs :~> ys) : xs :-> ys
= swap ! drop ! dot
true
false :: (xs :~> ys) : (xs :~> ys) : xs :-> ys
= drop ! dot
false
test :: '[] :-> '[ '[a] :~> '[a,a] ]
= quote dup test
```

Interestingly, these combinators represent the monadic operations on
state (`dot`

= `join`

, `pure`

=
`pure`

, etc.)

And can we get the nicer composition of the function from the intro? Kind of:

`= quote add ! curry ! dot ! map ! sum sumAdded `

Here are some references for concatenative languages: Okasaki (2002), Purdy (2012), Kerby (2007), Okasaki (2003).

*Proceedings of the ACM SIGPLAN workshop on Haskell - Haskell ’02*, 105–113. Pittsburgh, Pennsylvania: ACM Press. doi:10.1145/581690.581699. http://portal.acm.org/citation.cfm?doid=581690.581699.

*Journal of Functional Programming*13 (4) (July): 815–822. doi:10.1017/S0956796802004483. https://www.cambridge.org/core/journals/journal-of-functional-programming/article/theoretical-pearls/3E99993FE5464986AD94D292FF5EA275.

*The Big Mud Puddle*. https://evincarofautumn.blogspot.com/2012/02/why-concatenative-programming-matters.html.