General Semantic Construction of Dependent Refinement Type Systems, Categorically

TL;DR

This paper introduces a general semantic framework for dependent refinement type systems, enabling the lifting of structures like dependent products and recursion from underlying type systems to refinement systems, with demonstrated soundness.

Contribution

It provides a novel categorical construction for dependent refinement types based on comprehension categories and fibrations, extending the semantics of refinement types.

Findings

Semantic construction for dependent refinement types

Conditions for lifting dependent structures and effects

Soundness proof for the constructed refinement type system

Abstract

Refinement types are types equipped with predicates that specify preconditions and postconditions of underlying functional languages. We propose a general semantic construction of dependent refinement type systems from underlying type systems and predicate logic, that is, a construction of liftings of closed comprehension categories from given (underlying) closed comprehension categories and posetal fibrations for predicate logic. We give sufficient conditions to lift structures such as dependent products, dependent sums, computational effects, and recursion from the underlying type systems to refinement type systems. We demonstrate the usage of our construction by giving semantics to a refinement type system and proving soundness.