Applied Type System: An Approach to Practical Programming with Theorem-Proving

TL;DR

This paper introduces the Applied Type System (ATS), a practical framework for designing type systems with advanced features like dependent types, supporting theorem-proving and separating type reasoning from program execution.

Contribution

It presents ATS as a novel type system framework that accommodates practical programming features and theorem-proving, overcoming limitations of Pure Type System (PTS).

Findings

ATS can incorporate dependent types and recursive features.

Supports programming with theorem-proving (PwTP) paradigm.

Formal development and practical examples demonstrate ATS's effectiveness.

Abstract

The framework Pure Type System (PTS) offers a simple and general approach to designing and formalizing type systems. However, in the presence of dependent types, there often exist certain acute problems that make it difficult for PTS to directly accommodate many common realistic programming features such as general recursion, recursive types, effects (e.g., exceptions, references, input/output), etc. In this paper, Applied Type System (ATS) is presented as a framework for designing and formalizing type systems in support of practical programming with advanced types (including dependent types). In particular, it is demonstrated that ATS can readily accommodate a paradigm referred to as programming with theorem-proving (PwTP) in which programs and proofs are constructed in a syntactically intertwined manner, yielding a practical approach to internalizing constraint-solving needed during type-checking. The key salient feature of ATS lies in a complete separation between statics, where types are formed and reasoned about, and dynamics, where programs are constructed and evaluated. With this separation, it is no longer possible for a program to occur in a type as is otherwise allowed in PTS. The paper contains not only a formal development of ATS but also some examples taken from ats-lang.org, a programming language with a type system rooted in ATS, in support of employing ATS as a framework to formulate advanced type systems for practical programming.