Survey

TEL, an acronym for types, equations and logic, is a second generation logic programming language. It is the practical outcome of a research effort aimed at the integration of types and functions with logic programming à la Prolog. TEL was developed from 1986 to 1989 at the Universität Kaiserslautern and the DFKI by Werner Nutt, Ralf Scheidhauer, Georg Seul, and Gert Smolka.

Here are some highlights of TEL:

TEL is a functional language. Functions are defined with conditional equations and are executed by innermost rewriting.
TEL is a relational language. Relations are defined with Horn clauses and are executed by resolution and backtracking.
Relations are declared with fixed input and output arguments, the consistent use of which is checked automatically at compile time. These data flow declarations provide for a simple and clean operational interaction between functions and relations.
The data flow discipline can be weakened by declaring variables as open. Thus the full generality of logical variables in Prolog is available if needed.
TEL is a typed language. It is the first language supporting both subtypes (as in OBJ2) and polymorphic type constructors (as in ML). Every well-typed term has a unique least type depending functionally on the types of the variables occurring in the term.
TEL computes with types. Types are present at run-time through typed matching and unification: values are tested for membership in subtypes and open variables are constrained to subtypes.
TEL has a module facility supporting the incremental construction of large programs. After the interface structure of a system has been fixed, every module can be compiled separately.
TEL is a logic programming language. TEL's kernel language is based on a first-order, typed, definite clause logic with equality giving an initial algebra semantics to programs.
TEL is a practical language. It supports type-safe file handling and other extra-logical operations. Almost the entire TEL system is written in TEL.
TEL is an interactive language. The user enters queries, which are type checked, compiled, and executed. The results of a query are reported together with their least types.

Most of the theoretical and practical effort was devoted to the development of TEL's type system. TEL is a language integrating parametric polymorphism à la ML with subtypes à la OBJ2. This combination regains much of the flexibility of untyped languages such as Lisp and Prolog while providing the classical advantages of typed languages:

The data structures used by a program can be defined explicitly. This leads to clearer, much easier to understand programs. The explicit definition of data structures is particularly beneficial if they are complex, as it is typically the case in Artificial Intelligence.
Type checking detects many programming errors at compile time, a feature whose importance is proportional to the size of the program under development.

The presence of subtypes makes TEL's type system more than a syntactic discipline merely visible at compile time. TEL actually computes with types: at run time values are tested for membership in subtypes and variables are constrained to subtypes. Constraining variables to subtypes rather than binding them tentatively to particular elements (as in Prolog) avoids expensive backtracking.

The goal in designing TEL was to come up with a practical language that is a significant improvement over Prolog and can be implemented efficiently right now. The quest for practicability strongly constrained the design of TEL:

Functions are executed by innermost rewriting rather than by the more general narrowing. If there is a need to solve for variables, this still can be done with relations. One advantage of executing functions with rewriting is that the programmer doesn't need to worry about their control.
Relations must be declared with fixed input and output arguments. This ensures a clean operational interaction between functions and relations and is in accordance with common Prolog programming style. Having explicit data flow declarations and checking their consistent use at compile time contributes significantly to the clarity of programs. If the full generality of logical variables is needed, which is typically the case only at a few places in a large program, it can be obtained by bypassing the data flow discipline by declaring variables as open. While this approach is quite unsatisfactory from a theoretician's point of view, our programming experience in TEL suggests that it is very practical. One major use of logical variables is the implementation of open data structures, for instance, tables that are created incrementally at run time. In TEL open data structures can be implemented as abstract data types, thus making it possible to hide the use of open variables.
Logic alone does not suffice for a practical programming language. Hence TEL has several extra-logical features including modules, control structures, stream-based file handling and data bases. All of TEL's extra-logical features are type safe.