Polymorphic Directional Types for Logic Programming

In this paper we present a new type system for logic programs. Our system combines ideas of the classical polymorphic, but not very precise, system due to Mycroft and O'Keefe [16], and the complementary system of directional types that has been proposed by Aiken and Lakshman [1]. Our main technical inventions are a new method of deriving more specic types from a given type, which we call pruning, and the notion of the main type from which, using a combination of substitution, subtyping and pruning all types of a predicate can be obtained. We describe a type checking algorithm, and a type reconstruction algorithm which for a given program and a predicate nds its main type. A complexity analysis of these algorithms is provided. In spite of large theoretical complexity bounds these algorithms work quite fast in practice.

• Type: Conference
• Year: 2001
• Where: PPDP
• Authors: Pawel Rychlikowski, Tomasz Truderung
• Keywords: Main Type, PPDP 2001, Programming Languages, Type Checking Algorithm, Type Reconstruction Algorithm