High-level language languages are often implemented by transforming them to a stack-based intermediate language. To ensure correctness of the implementation, it is desirable to have a type-system for the stack-based code that ensures that the required arguments are available on the stack. This is quite challenging since the stack contains values of mixed types. Moreover, a single stack is shared by all basic stack instructions and the functions implemented with those instructions. Just like basic instructions, function calls are expected to replace their arguments by the result and to leave the rest of the stack untouched.

This paper shows a Domain-Specific Language, DSL, for stack-based computations embedded in strongly typed functional programming language. We use heterogeneous lists in the DSL to ensure that the top of the stack contains the required elements for instructions and functions. Type correctness of the composition of instructions and functions is ensured by requiring that the remainder of the stack is unchanged. However, standard typing restrictions impose that all function applications have identically typed arguments and hence an identical stack layout. We present a simple solution based on data types with universally quantified type variables. The resulting DSL supports multiple views and handles mutually recursive functions of arbitrary arities.