Type Systems for Declarative Programming Languages
Mário Florido
Departamento de Ciência de Computadores & LIACC
Faculdade de Ciências, Universidade do Porto
Rua do Campo Alegre, 823 4150 Porto, Portugal
January 1998
Abstract
The main goal of this work is to define formal semantic descriptions
of descriptive type systems for declarative programming languages.
We show that the syntactic relationships between terms and types come
from semantic relations stronger than soundness. Traditionally type systems
are defined first and then proved to be sound with respect to some
well chosen semantics. We argue that the definition of the systems
should come from their semantics and not the opposite.
The usual semantic criteria for relating terms and types is
soundness. Soundness has been studied for several systems, including
the Curry type system for the lambda-calculus, the type system of
the language ML, intersection type systems and type systems for logic programming.
Based on the semantic relationships between types and terms, we first
define, for any term, a set of constraints of its admissible types
which guarantee the types semantic validity.
Following the Curry view of types as descriptions of term properties,
we define necessary conditions for types to be descriptions of terms. We then
prove the soundness with respect to those conditions of the Curry and ML
type systems. We prove that soundness regarding those conditions is
not present on some intersection type systems and based on that result
we explain some pathological behaviours of those systems.
Finally, based on semantic properties of type systems for the
lambda-calculus, we classify the most used type languages for logic
programming. Our results suggest the use of deterministic regular
languages to denote types in this paradigm.
