TyS (Typechecking System) is an object-oriented type checker framework that has been developed at the Computational Reflection research group of the Oviedo University (Spain). TyS supports the automatic task of building object-oriented type checkers, to be used in language processors such as compilers (static type systems) or interpreters (dynamic type systems). It covers the existing lack of automatic implementation of (part of the) semantic analyzers in programming languages processors.
In the language processors implementation field, there exists a common lack of the automatic generation of semantic analyzers. Typechecking is commonly the main part of a semantic analyzer. The rest of its elements must be developed depending on the specific language features we are going to process.
There are different formal methods to specify the contextual constraints of a programming language. These methods are used to demonstrate that several correctness properties of a type system are achieved. However, they are not commonly used in a practical sense to develop a language processor --there are few tools capable of generating code.
There are many characteristics that are shared in almost every type checker. We identify this generic features as being potentially gathered in a tool capable of generating reusable code. Object-oriented design patterns could be applied to refactor this common behavior and structure.
Our approach is giving the compiler designer a framework to develop a type checker, following a common set of principles that may exist in almost every type checker. Instead of employing formal methods, we follow object-oriented design criteria independent of the programming language selected. The type checkers generated by these tool guides the programmer, in a correct and straightforward way, to develop type checking.
The TyS (Typechecking System) is an object-oriented framework that offers an automatic way to generate object-oriented type checkers. Starting from a type checker specification a specific implementation framework is generated. This is the system architecture:
A simple file is used to specify type rules --its description could be inspected in the user's manual. It has to be defined the programming language types, as well as its valid operations (omission implies not correctness): those operations that can be applied to the type variables.
This file is the input of the TyCC application (following section). Its correctness is checked and, if so, the type specification would be translated into a specific type checker implementation.
This is probably the main piece of our system. It takes the type specification file and makes language processing. Taking different parameters at its execution, if the file is syntactically and semantically correct, a type checker implementation is generated to be employed in a translator (static) or interpreter (dynamic).
Different kind of implementations could be generated depending on
the parameters passed to TyCC such as exception handler or a
particular programming languages. As an example, if we are
going to implement our language processor with
ANTLR, we can inheritance the exceptions we
ParserException. This way, our
semantic analyzer may recover to errors.
Depending on the type specification and the options passed to TyCC, alternative type-checker implementations are obtained. Every resulting type checker:
The type checker that has been generated leans on an API that offers those facilities generic to every type checker, independently of the programming language to be processed. It is separated, therefore, the specific functionality of a type checker (TyCC input file) from the general framework (API).
The other essential part of the system is the API that offers the type checker the interfaces of the general operation. The calls made from the type checker to the API, introduces the former into the TyS framework.
This subsystem needs a language for treating types: type expressions. By default, a Type Expression Language (TEL) is offered. Depending on the structure of every type, any type would have a TEL type expression that would represent it. The user could specify detailed type expression languages and type representations.
The API will validate type expression syntax, making sure that they are correct with the types specified. Therefore, this functionality may be employed either in static type checking or in a dynamic one.
The system will represent each type by an object, existing a unique object per type. The system ensures that no duplicated instances of a type may occur, reducing memory consumption.
Specific routines will always be necessary in a compiler construction. Different compiler modules (syntactic analyzed, symbol table, code generator) may access both the specific type checker generated and the generic API.
An example is the symbol table, responsible for storing the identifiers
of the programs analyzed. Every symbol has a type associated, whose
functionality is managed by TyS. The symbol table may retrieve types
by means of its type expression obtaining a
Once the type checker, compiler source code and input to other compiler tools are written, it is needed to compile the altogether generating the final language processor.
In many occasions a scanner, parser and tree walk tool is used (LEX, YACC, ANTLR and JAVACC). Our system has been designed taking this into account, offering the integration with this kind of tools. This integration in occasions is direct and, in others, need to be configured with specific parameters passed to TyCC --see TyS user's guide.
Once every module has been processed and compiled successfully, the application generated is the language processor. The static or dynamic type checking is performed by TyC, being necessary the API because of the support offered to TyC.
This work was partially funded by the Department of Science and Innovation (Spain) under the National Program for Research, Development and Innovation: project TIN2011-25978, entitled Obtaining Adaptable, Robust and Efficient Software by Including Structural Reflection in Statically Typed Programming Languages.