blog

Concatenative languages lend themselves to rewriting because they do not bind variables and thus do not incur any confusion with renaming/scope (compositional rather than applicative).

Manfred von Thun has already written on this: there are algebraic laws for concatenative programming like the algebraic laws one has for e.g. groups (\(a \cdot 1 = a\)).

Some simple ones that do not need quotation:

• dip(f) dip(g) = dip(f g)
• dip(+) + = + + (holds because \(+\) is associative; works on all other associative operations)
• 0 drop = id and so on for constants
• swap swap = id
• dup and = id
• dup or = id
• dup xor = False
• swap * = * (holds because \( \cdot \) is commutative; works on all other commutative operations)
• swap > = < (and so on for other operations that have reflect, such as \( > \)).
• > not = <= (and so on)

I implemented the above lints in my own Kempe compiler. A linting pass is easily implemented with pattern matching one has in ML-style functional languages:

lintAtoms :: [Atom b b] -> Maybe (Warning b)
lintAtoms []                                    = Nothing
lintAtoms (a@(Dip l _):a'@Dip{}:_)              = Just (DoubleDip l a a')
lintAtoms (a@(IntLit l _):(AtBuiltin _ Drop):_) = Just (PushDrop l a)
...