Partial type specifications and their ordering

Partial type specifications and their ordering

[Eric Hughes]

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

Re: Partial type specifications and their ordering

[Eric Hughes]

P.S.

To implement this, I'd use two new keywords:
-- "partial", to annotate any non-complete declaration
-- "satisfies", to require that an ordering relationship be present

To forestall some easy questions:
-- All inheritance gives rise to satisfaction relationships.
-- Not all satisfaction relationships are expressible as inheritance.

Eric

Re: Partial type specifications and their ordering

[Dmitry A. Kazakov]

On Mon, 17 Mar 2008 16:14:42 -0700 (PDT), Eric Hughes wrote:

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

[...]

Your draft does not explain why certain sets of types (called partial here)
cannot form a proper class.

My guess is that any set of types can be associated with a class. The
procedure is a follows. You construct the intersection of the interfaces of
the types from the set. (The set is countable infinite, so it should be
possible to do) The result is the interface of the root. The relation "S
derived from T" is obviously preserved on the class.

Consequently, generic types (not Ada term, but the meaning is obvious) are
fully equivalent to classes. The only difference is that the former do not
have T'Class and thus lack corresponding polymorphic values (class-wides).
IMO the difference is not in the semantics.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Partial type specifications and their ordering

[Eric Hughes]

On Mar 18, 2:40 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> Your draft does not explain why certain sets of types (called partial here)
> cannot form a proper class.

No code.  No subprogram definitions.  Nothing to execute.  The name
"partial type" can be taken as an abbreviation for "partial
specification of a type".  Pretty much every definition of types that
I've seen, starting with Godel's 1957 _Dialectica_ paper, uses some
kind of algorithm expression to define types.  A partial type strips
out algorithm expressions and focuses only on assumptions and results
of operations and on invariants about data.

> My guess is that any set of types can be associated with a class.

Any set of partial types can be associated with a least common
superclass.  That's what a lattice is.  See http://en.wikipedia.org/wiki/Lattice_%28order%29.

> Consequently, generic types (not Ada term, but the meaning is obvious) are
> fully equivalent to classes.

Please go find out what Alonzo Church meant by a lambda constructor
(which became Lisp, but is far broader than Lisp).  Barring
degeneracies, a generic type has a higher minimal lambda recursion
level than an ordinary type.  If you'd rather use a programming
language that treats type recursion as basic, try a functional
language such as Haskell.

Partial types specification are a notion orthogonal to generics.

Eric