Representation of the concatenation at the type level
-
05-11-2019 - |
Frage
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?
Keine korrekte Lösung