The notions of type and of type constraint 
Author Message
 The notions of type and of type constraint

[Note:

  This is almost a complete quote of a paper in ECOOP91 (which I think
  is legal everywhere given the liberal copying policies of such
  proceedings). I am posting it here verbatim so that one might read it
  without prejudice. The purpose of this is to _document_ what according
  to the authors is the typical usage of some terminology and concepts
  in discussions on type by various OO authors. I have omitted names,
  because the critique that will follow is not about their report, but
  about _what_ they report, and they explicitly disclaim that it is
  _their_ opinion on the matter. Therefore who is the author of this
  report does not really matter -- what matters is that it documents
  what a "consensus" (or "dissensus") of opinions of some people other
  than the authors, who are just messengers, is as to concepts and
  terminology. As to these opinions I don't know whether they are
  typical, or are shared by the majority of researchers, or are
  normative; they are common enough, IMNHO.

  I do this because there have been several discussions on "types" both
  recently and in the past years (I can remember some as far as five
  years ago), and I think that a lot of these discussions are made less
  enjoyable, and for me at least often very frustrating, by some
  widespread use of the same words to denote different concepts and
  different words to denote the same concept, and the concepts
  themselves are often not that well communicated either.

  This long quote, and the discussion in the next article, is both to
  provide context, explain a bit of my frustration (that I know is
  shared by others), and a bit as penance for the impatience with which
  (at times :->) I express such frustration, and also as a Festivities
  present for those that have the patience to still read about such
  issues.

]

1 Introduction

This paper summarizes three discussions conducted at the ECOOP'91 W5
Workshop on "Types, Inheritance, and Assignments", Tuesday July 16, 1991
in Geneva, Switzerland, organized by the authors. [ ... ]

The three discussions were entitled "Classes versus types", "Static
versus dynamic typing", and "Type inference". All these topics were
assumed to be volatile and controversial; indeed a broad range of
diverging opinions were represented. However, much superficial
disagreement seemed to be rooted in confusions about terminology. When
such issues were resolved, there appeared to be a consensus about basic
definitions and the -- often incompatible -- choices that one is at
liberty to make. This clarification, which we hope to have described
below, was the most important achievement of the workshop.

In our summary we have attempted to organize the topics and arguments
into a succinct and readable format. In particular, we sometimes
emphasize points of agreement or divergence that were only implied  at
the workshop. We hope that this style will result in a coherent overview
of this research area within the available space. Similar apologies
apply to the absence of references and direct quotation.

This summary is not intended as an introductory survey, and it will
certainly not perform that task in a satisfactory manner. We direct
ourselves to the active researcher in the field. [ ... ]

2 Classes versus types

Initially, this topic seemed very controversial -- in particular when
specialized to subclassing versus subtyping. However definite progress
towards a consensus was made during the discussion.

2.1 The role of types

A common understanding of the role of types can be achieved by viewing
them as predicates on objects. An object 'x' has type 'T' whenever 'x'
satisfies the predicate corresponding to 'T'. This implies that, in
general, an object will have many (incomparable) types.

There is full agreement that an object is an encapsulated state, and that
classes describe objects with the same implementation. Furthermore, it
is clear that subclassing is a technique for reusing object descriptions
(classes). There is some disagreement about the exact semantics of
subclassing: which transformations on classes should be possible, and
how should they be specified? Inheritance is generally considered a
fundamental subclassing mechanism, but it has many, somewhat divergent,
definitions.

To fully appreciate the need for types, one must consider the reuse of
individual objects. The _use_ of an object consists of sending it
messages, such as 'x.m(y)'.

Here 's' is the object, 'm' is the message selector, and 'y' is the
argument, which is also an object. When the method corresponding to 'm'
was implemented, it is likely that the argument was intended to be an
instance of some specific class. The _reuse_ of an object is concerned
with supplying other -- perhaps unforeseen -- arguments.

If the language is untyped, then _any_ argument is legal; in short, we
have unlimited possibilities for reuse. We operate, however at our own
peril. Our expectations when implementing the method 'm' need not be
adhered to, and it is a common experience that unwanted behaviour may
result.

Types will be needed to _restrict_ the potential reuse of objects. We
only want _disciplined_ reuse of objects. As mentioned, the types will
be predicates on objects. Formal parameters to methods will have
associated types, and all actual parameters must satisfy the
corresponding predicates.

There is a wide spectrum of such predicates that have been
suggested. Some place emphasis on the implementation, others on the
specification. Informally, they can be arranged along the following
line; from left to right the predicates become _more expressive_, in the
sense that they consider more and more aspects of objects.

            class+strictly monotone subclasses

          behaviour

        class+monotone subclasses

      interfaces

    name compatibility

  class+arbitrary subclasses

Some explanation is required. When classes are used as types, then the
predicate properly requires that the object is an instance of a
particular class +or_ any of its subclasses. Clearly, this definition
depends on the particular choice of subclassing mechanism.

By ``arbitrary'' subclasses we mean that methods may be added, deleted, or
redefined; this results in an almost trivial predicate, since any
collection of methods corresponds to some subclass. A step up, we can
require name compatibility, i.e., the existence of a particular set of
named methods. The next step is to interface types, which consider not
just the named methods required by the object, but also include the
types of the arguments of those methods (recursively). Going up we
encounter ``monotone'' subclasses, where we can only add methods or
redefine method bodies; clearly this will also preserve the
interface. Next, we encounter the idea of also imposing restrictions on
the ``behaviour'' of the required methods, typically by specifying pre-
and post-conditions; the more subtle ideas of behavior employed by
various process calculi could be an alternative. Finally, our diagram
shows ``strictly monotone'' subclasses, where methods can only be added;
here we even require that specified behaviour must have a particular
implementation.

Under close scrutiny, the indicated line would probably be discovered to
have a branching structure. There is, however, at least one
interpretation under which it is linear. If we partition the (imagined)
collection of all objects according to whether they have the same set of
types, then we observe strictly finer partitions as we move from left to
right.

2.2 Subtyping

Subtyping is a relation on types -- typically a partial order -- such
that if $T1$ is a subtype of $T2$ then object of type $T1$ is also an
object of type $T2$. This allows us to exploit the polymorphism of
objects.

The exact definition of subtyping depends on the definition of
type. However, there is a general soundness criterion that must be
obeyed. A method implementation is protected by the types of its formal
parameters. This protection is exploited by the language to guarantee
certain invariants about the dynamic behaviour of programs, e.g. the
absence of certain run-time errors. A sound notion of subtyping must
guarantee that sufficient protection is provided by the subtypes of the
formal parameters. The major notions of subtyping are listing in the
following table:

  When a type is:               Subtyping becomes:
  ===============               ==================

  class+subclass                subclassing
  name compatibility            more methods
  interface                     conformance
  behaviour                     weaker preconditions, stronger
  postconditions

With classes as types, it is hardly surprising that subtyping becomes
subclassing; after all, that choice is sound by definition. Note,
though, that there are other implementation types beside a class + its
subclasses. Finite sets of classes has also been suggested; in this
context, which arises when closed programs are considered, subtyping is
simply set inclusion. Even a single class can be a useful type because
it fixes both the behavior and the implementation; in this case
subtyping is trivial equality.

With specification types, subclassing and subtyping need not be related
at all; indeed there is no pressing reason even to have subclassing. For
name compatibility, the subtype must implement more methods. For
interfaces, the subtype must _conform_ to the supertype -- a recursive
generalization of the requirement for name compatibility that usually
involves the notion of _contravariance_. [ ... ]

2.3 Specification types versus implementation types

It is significant that the participants agreed on the described
conceptual common ground of the various notions of types and subtypes in
object-oriented languages. Beyond that, however, there are distinct
choices to be made. The fundamental question -- whether to separate
classes and types -- can now be rephrased as a question whether to use
specification types or implementation types. Neither alternative is
perfect, and it may be that both are needed ...

read more »



Thu, 11 Jun 1998 03:00:00 GMT  
 The notions of type and of type constraint

This is an analysis of a summary of a report that appears in the
preceding article. As such it reports what is supposed to be the
consensus (or not) of various researchers on concepts and terminology
in OO type system issues.

Let me make immediately say that because of big problem with the
terminology and concepts reported in it, it takes considerable effort to
extract some consistent meaning. For this reason, a large part of my
comments will consist of translations into an hopefully clearer
vocabulary of terminology and concepts.

This, IMNHO, (still) reflects indeed the state of the art as to the
concepts and terminology used in research on the subject.  It is no
surprise that many OO practitioners get confused impressions from a less
than alert reading of some of the literature.

I shall use as base for my terminology and concepts, among many others,
specifically the classics "On Data Types" by Hoare in "Structured
Programming", and "On Understanding Data Types" by Cardelli&Wegner in
"ACM Surveys".

Quote:
> The three discussions were entitled "Classes versus types", "Static
> versus dynamic typing", and "Type inference". All these topics were
> assumed to be volatile and controversial; indeed a broad range of
> diverging opinions were represented. However, much superficial
> disagreement seemed to be rooted in confusions about terminology.

Indeed... :-)

Quote:
> 2 Classes versus types
> Initially, this topic seemed very controversial -- in particular when
> specialized to subclassing versus subtyping. However definite progress
> towards a consensus was made during the discussion.
> 2.1 The role of types
> A common understanding of the role of types can be achieved by viewing
> them as predicates on objects. An object 'x' has type 'T' whenever 'x'
> satisfies the predicate corresponding to 'T'. This implies that, in
> general, an object will have many (incomparable) types.

This paragraph is almost devoid of meaning, and confuses several
important notions.

First of all the common understanding of the role of a type as in Hoare
and Cardelli&Wegner is that a (concrete) type describes the properties
(representation, operations applicable to it) common to a set of
(concrete) objects. Therefore it cannot be a _predicate_, at most its
_domain_ can be _characterized by_ a predicate.

Second, objects don't _have_ types. Objects _belong_ to types, the
opposite relationship.

Third, an object can belong only to one type (or "none"), even if its
denotation may belong to several type denotations.

  For example the value named by '1' can be only an 'int', while its
  denotation, the number one, belongs to both the 'Natural' and
  'Positive' type denotations. An added complication that should not
  fool the reader is that in some language the same syntactic entity,
  say '1', can name values that belong to two different types, depending
  on context, bot those values belong to only one type. In some other
  languages this is not the case; for example in C '1' labels a value
  belonging to the 'int' type and '1U' labels a value belonging to the
  'unsigned' type.

The above paragraph confuses, as it will be clearer in the following
discussion, several concepts, among them:

  * type, which is a characteristic of an object.

  * type denotation, which is the mathematical entity represented by
    a type.

  * identifier declaration, which may involve a _constraint_ on the type
    of the objects the identifier may denote, which constraint _may_ be
    expressed as a predicate on the characteristics of the objects the
    identifier may denote, and such predicate _may_ involve aspects of the
    type of those objects (as well as their lifetimes, for example).

Please reread carefully the latter paragraph, because it is crucial.

There is an enormous difference between the type of an object and the
type constraint that annotates an identifier (or a term of an expression
for that matter).

Quote:
> There is full agreement that an object is an encapsulated state, and
> that classes describe objects with the same implementation. [ ... ]
> To fully appreciate the need for types, one must consider the reuse of
> individual objects. The _use_ of an object consists of sending it
> messages, such as 'x.m(y)'.
> Here 'x' is the object, 'm' is the message selector, and 'y' is the
> argument, which is also an object. When the method corresponding to 'm'
> was implemented, it is likely that the argument was intended to be an
> instance of some specific class. The _reuse_ of an object is concerned
> with supplying other -- perhaps unforeseen -- arguments.

This is nonsense: there is no such thing as use or reuse of objects in
the above paragraphs.

What's there is the reuse of a procedure, which depends on the type
constraints on its _parameters_, which are (named by) identifiers.

Speaking of the type of objects and presenting as an example a procedure
_call_ is totally misleading.

The meaning is clear though, and let me try to rephrase it:

  To fully appreciate the usefulness of identifier constraints, one must
  consider the reuse of procedures, whose definitions consist of an
  interface and a body (and, rarely expressed, also of a specification):

    proc m (x,y) begin ... end

  Here 'm' is the name by which the procedure can be invoked, and 'x'
  and 'y' are the identifiers for its parameters, and are bound to the
  objects passed as arguments when it is called, which typically is
  specified using one of the following equivalent syntactic forms:

    a.m(b)
    a m: b
    m(a,b)
    (m a b)
    b a m

  In general the body of 'm' will only be meaningful for some particular
  subset of all possible arguments, and this can expressed by annotating
  the definition of the _parameters_ of 'm' with some constraint. Such
  constraint can involve _any_ possible property of the arguments, such
  as their value, their type (for objects are usually typed), or
  properties of those types. This all depends on the specific type
  checking system as defined in the specific language.

  For example relatively few languages allow one to constrain parameter
  identifier to particular _values_, as in CLOS or SML:

      proc m (x eql 1, y) begin return y end;
      proc m (x, y eql 1) begin return x end;
      proc m (x eql 0, y) begin return 0 end;
      proc m (x, y eql 0) begin return 0 end;

  Some languages allow to constrain parameters as to their _structure_
  (a part of the notion of type) e.g. SML, or as to the interface of
  their type, and so on.

  The role of a a language implementation is to enforce, and exploit,
  those constraints. Enforcement can be done either at compiletime or
  runtime, and so can exploitation.

  As an example of exploitation, it common to have the ability to
  specify a constraint on the lifetime of the objects that an identifier
  can denote. If such constraint specify a lifetime equal to the scope
  of the identifier, then the implementation can exploit it by
  allocating space on a stack, for example, and should then enforce this
  by making sure that references to the objects denoted by such
  identifiers are not exported outside their scope.

  In a language that supports identifier constraints, the same procedure
  name can be used for several implementations (overloading), as long as
  the parameters for each implementation are annotated with a unique (in
  some sense) set of constraints (ambiguous constraints may well make
  sense if nondeterminism is considered useful).

  In most common object oriented languages only the constraint of the
  first argument is examined in the above process.

Quote:
> If the language is untyped, then _any_ argument is legal;

This confuses two very important concepts again:

  * If a language is untyped, then effectively there is only one type,
    and there is no way to encapsulate a representation. A typed
    language is one in which objects objects are partitioned in classes
    based on their _distinct_ representations, according to some
    distinctness gauge (if the representations have different names
    vs. whether they have different structures, typically).

  * If a language is not _explicitly typed_ then while objects may be
    typed, identifiers are not constrained as to which kinds of objects
    they might denote, and therefore each procedure applies to all
    possible N-tuples of arguments (where N is the number of its
    parameters).

Note that the latter case is relatively rare. For example in languages
like Smalltalk-80 the first (distinguished) parameter is _always_
constrained.

Quote:
> in short, we have unlimited possibilities for reuse. We operate,
> however at our own peril. Our expectations when implementing the
> method 'm' need not be adhered to, and it is a common experience that
> unwanted behaviour may result.

The problem with no constraints on parameters is that procedures are not
(usually) restricted to implement total functions.

Quote:
> Types will be needed to _restrict_ the potential reuse of objects. We
> only want _disciplined_ reuse of objects.

And here the veil falls, and the absurdity of the terminology reported
as being in common use is apparent. Let's rephrase this as:

  Parameter annotations will be needed to constrain the potential
  applicability of procedures, for they only usually implement partial
  functions. We only want to apply procedures to arguments which satisfy
  at least in part the procedure's guard.

Again, note the absurdity of speaking of 'type' when 'constraint on the
parameter (which may involve the type of the argument)' is meant and of
reuse of 'object' when what is being reused is the _procedure_.

  Note that 'object' _might_ make sense if we were talking of actor
  systems, in which actors are in fact procedure activations, but we
  should not assume that the domain of our discussion is actor systems
  by default, for they imply a completely different computational model.

Quote:
> As mentioned, the types will be predicates on

...

read more »



Thu, 11 Jun 1998 03:00:00 GMT  
 The notions of type and of type constraint
There is a reply by Bertrand Meyer in comp.object to this thread.  I
wanted to point this out so that anyone who follows this group, but not
comp.object, wouldn't miss it.

This has been a public service announcement.



Fri, 12 Jun 1998 03:00:00 GMT  
 The notions of type and of type constraint

Quote:

>>> Grandi) said:

piercarl> [Note:
piercarl>   This is almost a complete quote of a paper in ECOOP91 (which
piercarl>   I think is legal everywhere given the liberal copying
piercarl>   policies of such proceedings). I am posting it here verbatim
piercarl>   so that one might read it without prejudice. The purpose of
piercarl>   this is to _document_ what according to the authors is the
piercarl>   typical usage of some terminology and concepts in
piercarl>   discussions on type by various OO authors. I have omitted
piercarl>   names, because the critique that will follow is not about
piercarl>   their report, but about _what_ they report, and they
piercarl>   explicitly disclaim that it is _their_ opinion on the
piercarl>   matter. [ ... ]

[Note:
  I have also decided, to clear some doubts, to type in here some parts
  of one of the positions papers summarized in the report (I would have
  typed in the whole paper, but I am not sure that it would be Ok as to
  copyright, as it is it arguably defensible). The paper is "Subclassing
  and subtyping", by J. Palsberg and M. I. Schwartzbach and appears in
  the collection edited by the same authors "Types, Inheritance and
  Assignment", PB-357, CS dept of Aarhus University, July 1991.

  I substantially agree with this paper, except for its use of "type" as
  shorthand for "type constraint", and "subtype" for "stronger type
  constraint" and "typed" for "statically/manifestly typed" even if it
  is crystal clear from their words that they mean the latter, and even
  if there are a few minor slips induced by such terminology.
]

                *Subclassing and subtyping*

We have studied an idealized subset of Smalltalk in order to get a
better understanding of subclassing and subtyping [53, 56, 54,55]. The
project is nearing completion, and in the following we survey its
results and limitations.

*Why Types?*

There are three reasons for introducing types. All are motivated by
deficiencies of untyped languages: they can be (1) unreadable, (2)
unreliable, and (3) inefficient. Types can remedy this by providing (1)
type annotations, (2) a safety guarantee, and (3) information for
optimization. We have the pragmatic attitude that anything meeting these
requirements deserves to be called a ``type''.

For object-oriented languages, a suitable definition of type is ``set of
classes''. Let 'S' be such a set and 'x:S' a type annotation. The
information it carries is that 'x' can only evaluate to either 'nil' or
some instance of a class in 'S'. The safety guarantee that be obtained
by verifying for every message send 'x.m(...)' that all classes in 'S'
implement a method 'm'. The optimization is primarily concerned with
inlining the call of 'm' whenever all classes in 'S' have the _same_
implementation of 'm'.

Our idealized language uses _finite_ sets of classes as types. We
restrict ourselves to consider entire programs, and then finite sets of
classes is an almost universal notion of type; after all, in a
particular program any predicate on classes can be expanded to yield a
finite set. Note that also interface and more general specifications
correspond to predicates.

*What is Subtyping?*

Subtyping is object-oriented languages allows a more flexible typing of
assignment and parameter passing compared to Pascal-like languages. With
types being sets of classes, it is natural to allow an object to have
any type containing its class. It follows that subtyping is simply set
inclusion; for an assingment 'x:=y' the type of 'y' must be contained in
that of 'x' (and similarly for parameter passing). Any sound notion of
subtyping must respect inclusion of the associated sets.

*What is Subclassing?*

Subtyping and subclassing are conceptually unrelated. A language may
have one of them or both. We view subclassing as being primarily
concerned with code reuse. The well-known concept of inheritance can be
seens as a textual short-hand, which is particularly useful since the
compiled code can be reused, due to dynamic method lookup. In typed
languages, it is also important if code is reused in a type-correct
manner.

With this simple view, there are no problems with updates or type-loss.

[ ... ]

*Type Inference*

It might be considered desirable to obtain a safety guarantee and
possiblities for optimizations without requiring the programmer to think
about types. This leads to the problem of ``type inference'', for which
we have suggested a solution for our idealized language[54].

We have designed an algorithm that given an untyped program can compute
a sound approximation of type of every expression, i.e. a superset of
the classes to instances of which it can evaluate. The algorithm employs
a so-called trace graph and generates a finite set of conditional set
inclusions, which is solved by a simple fixed-point computation.

Unlike some previous algorithms, ours can type-check most common
programs. it is currently being implemented in a prototype version,
which shows hopeful promises about its efficiency and reliability.

*Separate compilation*

Our approach seems incompatible with separate compilation, in the sense
of introducing new classes in a compiled program. We can, of course,
allow separate compilation of method bodies.

When new classes may be introduced, then finite sets are no longer
sufficient; after all, one cannot predict the potential future
classes. The solution is to use more general predicates such as 'x:<=C',
which expands to the infinite set of 'C' and all its subclasses.

Unfortunately, most of our results break down for such (finitely
represented) infinite sets. This is probably not coincidental, since
languages supporting both inheritance and types such as '<=C' invariably
resort to some degree of dynamic type checking (or accept unsound type
systems).



Sat, 13 Jun 1998 03:00:00 GMT  
 The notions of type and of type constraint
What is the subscription address for comp-object, please ?

Thanks

Dinesh
 ----------
From: owner-info-cls
To: Multiple recipients of list INFO-CLS
Subject: Re: The notions of type and of type constraint
Date: 25 December 1995 22:25

There is a reply by Bertrand Meyer in comp.object to this thread.  I
wanted to point this out so that anyone who follows this group, but not
comp.object, wouldn't miss it.

This has been a public service announcement.



Sun, 14 Jun 1998 03:00:00 GMT  
 
 [ 5 post ] 

 Relevant Pages 

1. The notions of type and of type constraint

2. Difference between a type system and a type constraint system

3. type classes and type constraints

4. Difference between a type system and a type constraint system

5. Library for solving set constraints in type analysis?

6. Haskell type classes, adding extra constraints

7. constraint error with tagged type

8. Hi all - new to smalltalk [type services and type-safety]

9. statically Typed vs dinamically typed

10. Strongly Typed and Weakly Typed Languages

11. Types, types: static vs. dynamic -- classification

12. Types, types: static vs. dynamic --

 

 
Powered by phpBB® Forum Software