DTP 2013 Accepted Papers with Abstracts

Abstract: A new approach to correct-by-construction pretty-printing is
presented. The basic methodology is the one of classical (not
necessarily correct) pretty-printing: users convert values to
pretty-printer documents, and a general rendering algorithm turns
documents into strings. The main novelty is that dependent types are
used to ensure that, for each value, the constructed document is
correct with respect to the value and a given grammar. Other parts of
the development use well-established technology: the pretty-printer
document interface is basically that of Wadler (2003), but with more
precise types, and a single additional primitive combinator; and
Wadler's rendering algorithm is used.

It is proved that if a given value is pretty-printed, and the
resulting string parsed (with respect to the same, unambiguous
grammar), then the original value is obtained. No guarantees are made
about "prettiness".

Abstract: The definitional equality of an intensional type theory is its test
of type compatibility. Today's systems rely on ordinary evaluation
semantics to compare expressions in types, frustrating users with
type errors arising when evaluation fails to identify two `obviously'
equal terms. If only the machine could decide a richer theory! We
propose a way to decide theories which supplement evaluation with
`-rules', rearranging the neutral parts of normal forms, and report
a successful initial experiment.
We study a simple -calculus with primitive fold, map and ap-
pend operations on lists and develop in Agda a sound and complete
decision procedure for an equational theory enriched with monoid,
functor and fusion laws.

Abstract: Type systems are used to eliminate certain classes of
errors at compile time. One of the goals of type system research is to
allow more classes of errors (such as array subscript errors) to be
eliminated statically in this fashion. Dependent type systems have
played a key role in this effort, and much research has been done on
them. However, so far no widely-used practical programming language
with a dependent type system exists. In this paper, we describe a new
functional programming language based on two key ideas. First, it
makes no distinction between expressions, types, kinds, and
sorts - everything is a term. The same integer values are used to
compute with and to index types, such as specifying the length of an
array. Second, the term language has a multivalued semantics - a term
can evaluate to zero, one, more than one, even an infinite number of
values. Since types are characterised by their members, they are
equivalent to terms whose possible values are the members of the type,
and we exploit this to express type information in our language. In
order to type check such terms, we give up on decidability - it is
possible to make our type checker loop forever. We consider this a
good tradeoff to get an expressive language without the pain of many
other dependent type systems. These two ideas combine to provide a
compelling practical dependent type system. This paper describes the
core ideas of the language, gives an intuitive description of the
semantics in terms of set-theory, explains how to implement the
language by restricting what programs are considered valid, and
sketches the first-order case of the type system.

Abstract: Dependently typed programming is hard, because ideally dependently typed programs should share structure with their correctness proofs, but there are very few guidelines on how one can arrive at such programs. McBride's algebraic ornamentation provides a methodological advancement, by which the programmer can derive a datatype from a specification involving a fold, such that a program that constructs elements of that datatype would be correct by construction. It is thus an effective method that leads the programmer from a specification to a dependently typed program. We enhance the applicability of this method by generalising algebraic ornamentation to a relational setting and bringing in relational algebraic methods, resulting in a hybrid approach that makes essential use of both dependently typed programming and relational program derivation. A dependently typed solution to the minimum coin change problem is presented as a demonstration of this hybrid approach. We also give a theoretically interesting “completeness theorem” of relational algebraic ornaments, which sheds some light on the expressive power of ornaments and inductive families.

Abstract: Generic programming is about writing a single function that
does something different for each type. In most languages
one cannot case over the structure of types. So in such languages
generic programming is accomplished by defining a universe, a data structure
isomorphic to some subset of the types supported by the language,
and performing a case analysis over this datatype instead. Such functions
support a limitied level of genericity, limited to the subset
of types that the universe encodes. The key to full genericity is
defining a rich enough universe to encode all types in the language.

In this paper we show how to define a universe with a predicative
hierarchy of types,
encoding a finite set of base types (including dependent products
and sums), and an infinite set of user defined datatypes.
We demonstrate that such a system supports a much broader
notion of generic programming, along with a serendipitous extension
to the usefulness of user defined datatypes with existential arguments.