Refining refinement types



It was observed by Burstall that it is natural to consider programs paired
with their proof of correctness. During program development, the proof can
be constructed together with the program. Specifications there are taken to 
be types plus some predicate, in a context. This notion of "deliverable" was 
studied by McKinna in his thesis, where it was pointed out that in practice 
it is existence of a proof which matters, and moreover that it would be better
to incorporate extensional equality into the theory since specifications only 
determine programs up to extensional equality.

Pfenning introduced "refinement types" in order to add an extra level of
expressiveness over the type theories of ML and LF. Rather than
replace the existing theories with more expressive ones, he considered 
a class of refinement types, each of which is essentially a base type plus
a predicate.

We give a calculus which can be seen as extending the deliverables idea, by 
providing an account of refinement types as a type-theoretic formalisation
of specifications, where our view of a specification is that it is given 
by some logical refinement of a type, and should be thought of as a per (in 
context) over the type, thus accounting for equality.

We build a theory of refinement types on top of the simply-typed lambda
calculus and allow dependency, in the form of dependent sums and products,
at the level of refinement types. This allows more expressive specifications
without a complicated underlying type theory. Equality on terms is stratified 
at refinement types, and a subtyping relation (or 'refinement') is given on 
the refinement types.

We give a simple concrete semantics using `Henkin pers', and deduce
consistency from soundness. We also prove a completeness result, though
we see that the calculus does not match the per intuition entirely.

For future work, we are currently combining the calculus with another
system, of 'refinement terms', consisting of programs with indeterminates.
This is intended to give a fully formalised refinement calculus based on this 
view of specifications.