Gödel (programming language): Difference between revisions

Revision as of 23:59, 26 February 2014

Revision as of 22:16, 19 May 2014

Line 55:

The main reason for introducing types in logic programming languages is for knowledge representation. Intended interpretations in most logic programming applications are typed and hence using a typed language is the most direct way of capturing the relevant knowledge in the application. Also, the information given by the language declarations of a type system can be used by a compiler to produce more efficient code. Type declarations can help to catch programming errors. In a typed program, typographical errors often lead to syntax errors which can be caught by the compiler.

There are two kinds of type systemsystems in logic. The first one is suitable for higher order logics, for example, λ-calculus. The second kind of type system studied in logic is many-sorted (first-order) logic. It is many-sorted logic which provides the foundation for type facilities in first-order logic programming languages and it is an extension of this logic that is used by Gödel. However, a many-sorted logic alone is not sufficiently flexible for a type system in a logic programming language. For this reason, Gödel allows a form of polymorphism, called parametric polymorphism, familiar from functional programming languages. Parametric polymorphism necessitates the introduction of type variables, which range over all types.

[[Parametric polymorphism]] is the second most important aspect of the type system. It is common for programmer to want to write a definition of a predicate for which the arguments of the predicate vary in used types. For example, the Append predicate is normally written so that it can append lists of any type. A symbol is polymorphic if its declaration contains a parameter; otherwise it is monomorphic. A polymorphic symbol can be understood as representing a collection of (monomorphic) symbols.