# Representation of the concatenation at the type level

I would like to learn more about concatenative programming through the creation of a small simple language, based on the stack and following the concatenative paradigm.

Unfortunately, I haven't found many resources concerning concatenative languages and their implementation, so excuse me in advance for my possible naivety.

I therefore defined my language as a simple sequence of concatenation of functions, represented in the AST as a list:

data Operation
= Concat [Operation]
| Quotation Operation
| Var String
| Lit Literal
| LitOp LiteralOperation

data Literal
= Int Int
| Float Float

data LiteralOperation
= Add | Sub | Mul | Div


The following program, 4 2 swap dup * + (corresponding to 2 * 2 + 4) once parsed, will give the following AST:

Concat [Lit (Int 4), Lit (Int 2), Var "swap", Var "dup", LitOp Mul, LitOp Add]


Now I have to infer and check the types.

I wrote this type system:

data Type
= TBasic BasicType   -- 'Int' or 'Float'
| TVar String        -- Variable type
| TQuoteE String     -- Empty stack, noted 'A'
| TQuote String Type -- Non empty stack, noted 'A t'
| TConc Type Type    -- A type for the concatenation
| TFun Type Type     -- The type of functions


That's where my question comes in, because I don't know what type to infer from that expression. The resulting type is obvious, it is Int, but I don't know how to actually entirely check this program at the type level.

At the beginning, as you can see above, I had thought of a TConc type that represents concatenation in the same way as the TFun type represents a function, because in the end the concatenation sequence forms an unique function.

Another option, which I have not yet explored, would be to apply the function composition inference rule to each element of this expression sequence. I don't know how it would work with the stack-based.

The question is so: how do we do it? Which algorithm to use, and which approach at the type level should be preferred?

A major idea of concatenative languages is that the syntax and semantic domain form monoids and the semantics is a monoid homomorphism. The syntax is the free monoid generated by the basic operations, better known as a list. It's operation is list concatenation, i.e. (++) in Haskell. In the untyped context, the semantic domain is just the monoid of endofunctions (on stacks) with composition as the operation. In other words, an interpreter should look like the following:

data Op = PushInt Int| Call Name | Quote Code | Add | ... -- etc.
type Code = [Op]

-- Run-time values
data Value = Q (Endo Stack) | I Int | ... -- etc.
type Stack = [Value]

-- You'd probably add an environment of type Map Name (Endo Stack)
interpretOp :: Op -> Endo Stack
interpretOp (PushInt n) = Endo (I n:)
interpretOp (Quote c) = Endo (Q (interpetCode c):)
interpretOp op = ... -- etc.

interpretCode :: Code -> Endo Stack
interpretCode = foldMap interpretOp

runCode :: Code -> Stack
runCode code = case interpretCode code of Endo f -> f []


Making a (very naive) compiler is just as simple. The only thing that changes is the target monoid which will now be a syntactic monoid built out of a fragment of the syntax of the target language thus interpretOp will become compileOp. This target monoid may be sequences of statements with the operation of sequential composition, i.e. ;. You can be quite a lot more sophisticated though.

Type systems for concatenative languages are not as obvious, and there are almost no typed concatenative languages. Cat is the most significant example I'm aware of. One way to start to approach it and experience some of the issues that come up is to embed a concatenative language in Haskell. You quickly discover that you don't want add :: (Int, Int) -> Int as this won't compose. Instead, you have add :: (Int, (Int, s)) -> (Int, s). This works extremely well for simple things. This is also relatively clearly poor man's row types. One of the first and most significant hurdles you'll hit is dealing with quotations. The problem is that [add] should correspond to something with a type like s -> ((forall s'. (Int, (Int, s')) -> (Int, s')), s) which requires higher-rank types and impredicative instantiation. Cat appears to have both. It certainly has higher ranked types, and it will substitute a polytype for a type variable. It may be doing things in a way that can be understood without impredicativity. Accomplishing this with an embedding in Haskell might be doable using type-level lists, (closed) type families, and local universal quantification. At this point though, making a custom type system likely makes more sense.

Operations with non-uniform stack effects are also likely to be problematic, but, in most cases, it makes sense to just omit them and provide alternative means of doing things that guarantee a consistent stack.