Using Modes to Ensure Subject Reduction for Typed Logic Programs with Subtyping

TL;DR

This paper introduces a type system with modes for logic programs that guarantees subject reduction even with complex subtyping, ensuring type consistency throughout program execution.

Contribution

It provides syntactic conditions and a mode-based approach to maintain subject reduction in logic programs with subtyping, extending prior work without subtyping.

Findings

Syntactic conditions ensure subject reduction with subtyping

Modes help maintain type safety during execution

Applicable to logic programs with parametric polymorphism and subtyping

Abstract

We consider a general prescriptive type system with parametric polymorphism and subtyping for logic programs. The property of subject reduction expresses the consistency of the type system w.r.t. the execution model: if a program is "well-typed", then all derivations starting in a "well-typed" goal are again "well-typed". It is well-established that without subtyping, this property is readily obtained for logic programs w.r.t. their standard (untyped) execution model. Here we give syntactic conditions that ensure subject reduction also in the presence of general subtyping relations between type constructors. The idea is to consider logic programs with a fixed dataflow, given by modes.