Correct-by-Construction Pretty-Printing

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".

New Equations for Neutral Terms: A Sound and Complete Decision Procedure, Formalized.

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.

A Multivalued Language with a Dependent Type System

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.

Relational Algebraic Ornaments

Leveling Up Dependent Types - Generic programming over a predicative hierarchy of universes.

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.