Relational Type Theory (All Proofs)

TL;DR

This paper presents Relational Type Theory (RelTT), a novel type theory incorporating relational semantics and constructs like composition and converse, enabling traditional type constructions and paving the way for implementation.

Contribution

It introduces RelTT with relational semantics, extending System F, and demonstrates how key type-theoretic constructions are achievable within this new framework.

Findings

RelTT supports eta-laws for basic types

It enables inductive and recursive types with induction principles

A type system for RelTT is developed for potential implementation

Abstract

This paper introduces Relational Type Theory (RelTT), a new approach to type theory with extensionality principles, based on a relational semantics for types. The type constructs of the theory are those of System F plus relational composition, converse, and promotion of application of a term to a relation. A concise realizability semantics is presented for these types. The paper shows how a number of constructions of traditional interest in type theory are possible in RelTT, including eta-laws for basic types, inductive types with their induction principles, and positive-recursive types. A crucial role is played by a lemma called Identity Inclusion, which refines the Identity Extension property familiar from the semantics of parametric polymorphism. The paper concludes with a type system for RelTT, paving the way for implementation.