Evaluation and implementation of an optional, pluggable type system for Forth

Abstract

Typically, a type system influences the semantics of the programming language such that type checking is a mandatory process. In contrast, optional, pluggable typing introduces the possibility of running checkers for diverse semantic analyses and can be considered as an alternative to today's prevalent mandatory typing. This thesis aims at exploring the design of a Haskell prototype of optional, pluggable typing for the stack-based language Forth. This thesis addresses the question of how optional checkers, supporting varying degrees of static type consistency, can be designed and implemented for practical use in Forth considering the trade-offs of a potential loss of expressiveness and the need of necessary type annotations. A stack effect calculus is derived from a literature review on static analysis of Forth programs as a theoretical basis for type checking. Subsequently, language features as subtyping, control structures, reference types, assertions and casts are added to the implementation. It is the added value of this thesis to incorporate the above features together with a statically type consistent treatment of multiple stack effects, compile-time programming, object-oriented and higher-order programming into the same type checking algorithm. The prototype can deal with the majority of the words of the Core wordset and features a type checking algorithm of configurable static rigorousness, ranging from stack underflow checking to static type consistency. The checkers are evaluated using the example of a functionally correct Forth program. The evaluation shows that those checkers of varying static type safety aid the gradual evolution of the input program towards a static stack discipline. This benefit comes at the expense of only minimal type annotations. Type annotations of words defined in the program can often be omitted but they are always needed in supporting higher-order programming.

Typically, programming languages provide one type system which associates types to a program-s expressions and checks their consistent use either at compile-time or at run-time. In any case, the type system influences the semantics of the language such that type checking is a mandatory process. In contrast, optional, pluggable typing introduces the possibility of running different checkers for diverse semantic analyses and can be considered as an alternative to today-s prevalent mandatory typing and the tight coupling of a programming language and its type system. This thesis aims at exploring the design of a Haskell prototype implementation of optional, pluggable typing that provides checkers enforcing increasing static type safety for the stack-based language Forth. Alongside a literature research on various approaches bridging between static and dynamic typing, the prototype design and implementation serve to shed light on the benefits as well as the inevitable trade-offs and practical limitations of such a type system. In particular, this thesis addresses the question of how optional checkers, supporting varying degrees of static type consistency, can be designed and implemented for practical use in Forth considering the trade-offs of a potential loss of expressiveness and the need of necessary type annotations. To this end, a stack effect calculus is derived from a literature review on static analysis of Forth programs as a theoretical basis for type checking and subsequently, language features as subtyping, control structures, reference types, assertions and casts are added to the implementation. It is the added value of this thesis to incorporate the above features together with a statically type consistent treatment of multiple stack effects, compile-time programming, object-oriented programming and higher-order programming into the same core type checking algorithm. The resulting prototype can deal with the vast majority of the words of Forth-s Core wordset and features a type checking algorithm of configurable static rigorousness, ranging from bare stack underflow and overflow checking to full-fledged static type consistency. The checkers are practically evaluated using the example of a small, functionally correct Forth program. The evaluation shows that those checkers of varying static type safety aid the gradual evolution of the input program towards a static stack discipline. This benefit comes at the expense of only minimal type annotations. Type annotations of words defined in the program can often be omitted but they are always needed in supporting higher-order programming.