Partial type specifications and their ordering

[Eric Hughes <eric.eh9@gmail.com>]

My comment earlier today got my mind in a buzz on the topic of partial
types, so as a form of personal exorcism I wrote a skeleton draft.  I
first came upon this idea which thinking about types from a program
correctness point of view, so I've included all that as well; it's
even relevant, though not immediately obvious.

I'm not sure I got quite all of the details right; corrections
welcome.

A partial type is a collection of zero or more of each the following:
  A. Generic formal parameters
    1. formal objects, specified as satisfying some partial type.
    2. formal partial types
    3. formal partial subprograms
    4. formal partial packages
  B. Partial discriminants, that is, a discriminant specified with
partial types
  C. Partial subprograms, that is, subprograms specified with partial
types
  D. Partial record components, objects specified with partial types

For two partial types T1 and T2, we say that T1 < T2 if all the
following hold.  If so, then we also say that T1 satisfies T2.
Colloquially T1 is a subtype of T2 and T2 is a supertype of T1.
I. Language relationships
  A. The generic parameters of T2 are a subset of those of T1.
  B. The discriminants of T2 are a subset of those of T1.
  C. The subprogram names of T2 are a subset of those of T1.
  D. For each subprogram name F in T2
    1. the number of parameters of F in T1 and T2 are equal, and
    2. the names of parameters of F in T1 and T2 are pairwise equal,
and
    3. the partial type of a parameter in T2 is a supertype of the
corresponding parameter in T1, and
    4. the return value of T2 is a subtype of the return value of T1
  E. For each component name C in T2
    1. there is a component named C in T1, and
    2. the partial type of T1.C is a subtype of T2.C
II. Predicate relationships
  A. The instantiation conditions on the generic parameters of T1
imply those of T2.
  B. The instantiation conditions on the discriminants of T1 imply
those of T2.
  C. For each subprogram name F in T2
    1. the preconditions of T1.F imply those of T2.F, and
    2. the postconditions of T2.F imply those of T1.F
  D. The invariants of T1 imply those of T2.

Each ordinary type has a canonical partial type associated with it.
For a tagged type U, the canonical partial type of a subtype of U
satisfies the canonical partial type of U.  The canonical partial type
of limited view of a type U satisfies the canonical partial type of U.

The reason the predicate relationships are in there is to be able to
reason about limited types.  Limited types can be seen as having
required postconditions of the form "in C = out C", that is, no
component is modified by a subprogram.

Some theorems: "<" on partial types is a partial ordering.  The set of
partial types with "<" is a lattice.  The lattice is upper-bounded by
the nil type.

Whew.  Enough for now.

Eric