An approach to practical programming with theorem-proving
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 (of minimalist style) but also some examples taken from
ATS, 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.
An approach to practical programming with dependent types
Abstract:
The paper presents an approach to enriching the type system of ML
with a restricted form of dependent types, where type index terms are
required to be drawn from a given type index language L that is completely
separate from run-time programs, leading to the DML(L) language
schema. This enrichment allows for specification and inference of
significantly more precise type information, facilitating program error
detection and compiler optimization. The primary contribution of the paper
lies in a novel language design, which can effectively support the use of
dependent types in practical programming. In particular, this design makes
it both natural and straightforward to accommodate dependent types in the
presence of effects such as references and exceptions.
Abstract:
The paper introduces a notion of guarded recursive (g.r.)
datatype constructors, generalizing the notion of recursive datatypes in
functional programming languages such as ML and Haskell. Both theoretical
and practical issues resulted from this generalization are addressed. On
one hand, a type system is designed to formalize the notion of
g.r. datatype constructors and its soundness is proven. On the other hand,
some significant applications (e.g., implementing objects, implementing
staged computation, etc.) of g.r. datatype constructors are given,
indicating that g.r. datatype constructors can have far-reaching
consequences in programming. The main contribution of the paper lies in the
recognition and then the formalization of a programming notion that is of
both theoretical interest and practical use.
Abstract:
This paper enriches imperative programming with a form of dependent
types. It starts with some motivations for the enrichment as well as some
major obstacles that need to be overcome. The design of a source-level
dependently typed imperative programming language of the name
Xanadu is presented, together with a formalization of both static and
dynamic semantics for Xanadu. In addition, the type soundness for Xanadu is
established and various realistic programming examples in support of the
practicality of Xanadu are given. It is claimed that the language design of
Xanadu is novel and it can serve as an informative example to demonstrate a
means for combining imperative programming with dependent types.
Abstract:
Applied Type System (ATS) is recently proposed as a framework for
designing and formalizing (advanced) type systems in support of practical
programming. In ATS, the definition of type equality involves a constraint
relation, which may or may not be algorithmically decidable. To support
practical programming, we adopted a design in the past that imposes certain
restrictions on the syntactic form of constraints so that some effective
means can be found for solving constraints automatically. Evidently, this
is a rather ad hoc design in its nature. In this paper, we rectify the
situation by presenting a fundamentally different design, which we claim to
be both novel and practical. Instead of imposing syntactical restrictions
on constraints, we provide a means for the programmer to construct proofs
that attest to the validity of constraints. In particular, we are to
accommodate a programming paradigm that enables the programmer to combine
programming with theorem proving. Also we present some concrete examples in
support of the practicality of this design.
Abstract:
The need for direct memory manipulation through pointers is
essential in many applications. However, it is also commonly understood
that the use (or probably misuse) of pointers is often a rich source of
program errors. Therefore, approaches that can effectively enforce safe use
of pointers in programming are highly sought after. ATS is a programming
language with a type system rooted in a recently developed framework
Applied Type System, and a novel and desirable feature in ATS lies in its
support for safe programming with pointers through a novel notion of
stateful views. In particular, even pointer arithmetic is allowed in ATS
and guaranteed to be safe by the type system of ATS. In this paper, we give
an overview of this feature in ATS, presenting some interesting examples
based on a prototype implementation of ATS to demonstrate the practicality
of safe programming with pointer through stateful views.
Abstract:
We present a type system capable of guaranteeing the memory safety of
programs that may involve (sophisticated) pointer manipulation such as
pointer arithmetic. With its root in a recently developed framework
Applied Type System (ATS), the type system imposes a level of
abstraction on program states through a novel notion of recursive stateful
views and then relies on a form of linear logic to reason about such
stateful views. We consider the design and then the formalization of the
type system to constitute the primary contribution of the paper. In
addition, we also mention a running implementation of the type system and
then give some examples in support of the practicality of programming with
recursive stateful views.
Dependent ML (DML) extends ML conservatively with a restrictive
form of dependent types. In DML, program values are not allowed
in the formation of types. However, types dependent on certain
program values (such as integers) can still be constructed due to
the availability of singleton types for classifying such values.
Dependent ML was developed and prototyped during the second half
of 1997 and through the year of 1998 as the primary contribution
of Hongwei Xi's doctoral thesis, which was supervised by Prof.
Frank Pfenning and completed and defended in December, 1998.
The prototype implementation of DML consisted primarily of a
typechecker written in Standard ML (SML).
Further developement of DML continued at Oregon Graduate Institute (OGI) of
Science and Technology, where Hongwei Xi worked as a post-doctoral
researcher until the end of August, 1999. During this period, a programming
language system of the name deCaml was implemented as an extension
of Caml-light (the predecessor of OCaml) with DML-style dependent types.
Programs in deCaml can be first typechecked and then passed to Caml-light
for further compilation. Various demos of deCaml were given but the system
itself has never been documented for public release.
How can DML-style dependent types be made available to support imperative
programming? An experimental programming language of the name Xanadu
was designed and implemented mostly during the second half of 1999 in an
attempt to answer this question. While many concepts developed in Xanadu
would eventually find their way into ATS, Xanadu as a programming language
did not provide a satisfactory answer to imperative programming with
dependent types. In particular, the manner in which dependent types are
supported in Xanadu is very limited, and it is clear that this manner
cannot accommodate many common programming features in the C programming
language. Various demos of Xanadu were given based on a prototype
implementation consisting primarily of a typechecker and an interpreter.
A guarded recursive datatype (GRDT) is also referred to as a generalized
algebraic datatype (GADT). This notion can be seen as a natural adaptation
of DML-style dependent types in a setting where types replace integers as
type indexes. While GRDTs are fundamentally different from DML-style
dependent types semantically, the former and the latter are treated
similarly at the level of syntax. In particular, typechecking for the
former can be readily adapted from typechecking for the latter. The concept
of ATS was conceived around the end of 2002 (immediately after the
development of GRDTs) as an attempt to form a unifying framework for both
DML-style dependent types and GRDTs.
Implementation for ATS started around the beginning of 2003, when the
theory for ATS was being developed and formalized as well. By Summer 2003,
a functioning typechecker for ATS could be tested on a variety of simple
examples. By the beginning of 2004, an interpreter for programs in ATS
started to be functioning. However, it was still unclear by then how common
imperative programming features can or should be supported in ATS. The
breakthrough came at the beginning of Summer 2004, when it was finally
realized that a form of theorem-proving based on linear logic can be
incorporated into ATS as the basis for supporting imperative
programming. The moment of this realization can probably be claimed as the
single most crucial moment in the development of ATS. By the middle of July
2004, the implementation for ATS (extended with linear types) reached a
point where the typechecker and the interpreter were able to handle a
variety of imperative programs.
The following list consists of the major implementations of ATS
that were publicly released in the past:
ATS0/Proto (written in OCaml)
ATS1/Geizella (written in OCaml)
ATS1/Anairiats (written in ATS1)
ATS2/Postiats (written in ATS1)
The current release of ATS is ATS2/Postiats. The compiler inside
ATS2/Postiats alone consists of more than 181K lines of code written in
ATS1, which can be compiled into C code (conforming to the C99 standard) by
either ATS1/Geizella or ATS1/Anairiats. A little bit of history on the
released implementations of ATS can be found on-line.
[thePageRFooterSep]
This page is created by
Hongwei Xi
with tools including ATS/weboxy, atscc2js and atscc2php.
