A.M. Dinikeev¹

¹Innopolis University (Innopolis, Russia)

¹a.dinikeev@innopolis.university

In concatenative stack-based programming languages programs are written as sequences of operators that manipulate a stack of values, rather than using named variables. While most well-known concatenative stack-based programming languages, such as Forth, Factor, and Joy, are dynamically typed, some statically typed concatenative stack-based languages also exist. Static typing in such languages allows for compile-time detection of type errors and makes it possible to view the types of values on the stack at any point in the program.
Supporting first-class functions in concatenative stack-based programming languages increases abstraction and code reuse, resulting in programs that are easier to write, understand, and maintain. However, adding support for first-class functions to a statically typed stack-based programming language presents a challenge of describing the type of operators for first-class functions execution and composition, these operators have different operator types depending on the first-class function they are applied on. An existing programming language Cat is an example of a statically typed concatenative stack-based programming language with support for firstclass functions. Its type system uses type variables that represent a list of types, which is necessary for operators that execute and compose first-class functions. However, this requires the type system to support rank-n polymorphism for type inference involving first-class functions, which greatly increases the complexity of the type checker implementation.
This paper describes IV, a statically typed concatenative stack-based programming language, along with a type system that supports first-class functions without the requiring rank-n polymorphism. This is achieved by requiring explicit type annotations for all operator definitions, using an operator type extension process that generalizes operator applicability across stacks with different element count, and introducing explicit parameters for operators that perform first-class functions execution and composition. These choices simplify the type system while still keeping the type system expressive enough to perform type checking on programs involving firstclass functions.

Dinikeev A.M. Type system for a statically typed concatenative programming language with first class function support. Informationmeasuring and Control Systems. 2025. V. 23. № 5. P. 15−25. DOI: https://doi.org/10.18127/j20700814-202505-02 (in Russian)

1. Moore C.H. FORTH: a new way to program a mini computer. Astronomy and Astrophysics Supplement. 1974. V. 15. P. 497.
2. Pestov S., Ehrenberg D., Groff J. Factor: a dynamic stack-based programming language. SIGPLAN Not. 2010. V. 45. № 12. P. 43−58. DOI: 10.1145/1899661.1869637.
3. Von Thun M., Thomas R.Joy: Forth's functional cousin. Proceedings of the 17th EuroForth Conference. 2001.
4. Diggins C. Type Inference for Polymorphic Types. https://github.com/cdiggins/type-inference.
5. Rather E.D., Colburn D.R., Moore C.H. The evolution of Forth. Association for Computing Machinery. New York. NY. USA. 1996. P. 625−670. DOI: 10.1145/234286.1057832.
6. Harris H.M. Forth as the basis for an integrated operations environment for a space shuttle scientific experiment. J. FORTH Appl. Res. 1986. V. 3. № 2. P. 23−36.
7. Lindholm T., Yellin F., Bracha G., Buckley A., The Java Virtual Machine Specification. https://docs.oracle.com/javase/specs/jvms/se8/html/.
8. Python Software Foundation. Disassembler for Python bytecode. https://docs.python.org/3/library/dis.html.
9. Milner R., Tofte M., Harper R., MacQueen D. The definition of standard ML: revised. MIT press. 1997.
10. WebAssembly Community Group. WebAssembly specification. https://webassembly.github.io/spec/core/.
11. Freeman T. Pfenning F. Refinement types for ML. Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation. 1991. P. 268−277.