Abstract
Traditional static type systems in the Hindley-Milner style are a
useful means of guaranteeing type safety, in the form of type
preservation and progress theorems, and of broadly specifying
properties of functions (such as taking integers to lists of
integers). In order to allow programmers to express stronger
properties through static typing, I propose to develop and implement
a rich type system that combines and extends work on datasort
refinements, index refinements, intersection, and union types, and
to show that it can check many interesting properties of functional
programs that are difficult or impossible to check in conventional
static type systems. Due to the richness of the type system, full
type inference is undecidable, so a certain amount of annotation
will be necessary. I intend to focus on properties of algebraic
datatypes, such as list length or the set of keys mapped by a binary
search tree. The type system's soundness is maintained in the
presence of effects, but the properties are not about state.
However, many of the techniques developed may be applicable to
stateful properties as well.
|