A Complete Finitary Refinement Type System for Scott-Open Properties

TL;DR

This paper introduces a finitary refinement type system that is both sound and complete for Scott-open properties in the context of infinite data handling, based on domain theory and logical polarities.

Contribution

It develops a novel type system that precisely characterizes Scott-open properties for recursive data types using logical polarities and domain theory.

Findings

The type system is sound and complete for Scott-open properties.

It models input-output properties of functions handling infinite data.

Uses logical polarities to distinguish between least and greatest fixpoints.

Abstract

We are interested in proving input-output properties of functions that handle infinite data such as streams or non-wellfounded trees. We provide a finitary refinement type system which is (sound and) complete for Scott-open properties defined in a fixpoint-like logic. Working on top of Abramsky's Domain Theory in Logical Form, we build from the well-known fact that the Scott domains interpreting recursive types are spectral spaces. The usual symmetry between Scott-open and compact-saturated sets is reflected in logical polarities: positive formulae allow for least fixpoints and define Scott-open sets, while negative formulae allow for greatest fixpoints and define compact-saturated sets. A realizability implication with the expected (contra)variance on polarities allows for non-trivial input-output properties to be formulated as positive formulae on function types.