|> I have been looking at some recent papers on 'types' in OO context, and
|> have been having some discussion on such, and these have led to realize
|> that some people (perhaps many...) have not clear the distinction not
|> only between 'type' and 'type constraint', but the related one between
|> 'type system' and 'type constraint system'.
|>
|> I'll try, for the record, without much hope, to illustrate it...

You made the difference perfectly clear, at least to me.
Based on your definition I conclude that Smalltalk has a type system
but not a type constraint system.

[..]
|>   * in ISO Pascal 'var x : record ... end' constrains 'x' to denote
|>     values of the ``anonymous'' type defined therein, and _only that
|>     type_. More explicitly: 'var x; require typeof value(x) == record
|>     ... end;'.
|>
|>   * in Pascal 'var x: cmplx' constrains 'x' to denote values of the type
|>     'cmplx' or *any type with the same structure*. More explicitly: 'var
                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
AFAIK Pascal (like C/C++, Eiffel, Ada) has nameequivalence
for (named) types, so the same structure woun't do;
Modula-2 is one that has structural equvialence.

|>     x; require typeof value(x) equiv cmplx'.

What's the difference between "==" and "equiv" ?

[..]
|> Since as a
|> rule type metaoperators define not only the storage structure of a new
|> type but also its constructors and accessor functions, a large part of
|> designing a type system is deciding how far one wants to have the
|> compiler go in synthetizing those;

Well, like distinguishing type-system from type-constraint-system
you could additionally distinguish the implementation of a type
(some call it class) from its interface (type without implem. is
an abstract type).
The type-interface-system usually is the reference for the
type-constraint-system and the type-implementation-system.

* A type-implemenation(-constraint ?) says:
        "class y   implements                 interface-x"
  or
        "ctor y    constrained-to-producing   values-conforming-interface-x"

* A type-constraint says:
        "var y     constrained-to-containing  values-conforming-interface-x"

Ulf Schuenemann

--------------------------------------------------------------------
 ,_.   Ulf Schnemann
#,  \  Fakult?t fr Informatik, Technische Universit?t Mnchen, Germany.

 v=-<  WWW:   http://www.*-*-*.com/ ~schuenem/

Yes, exactly. There are no type (or other, like lifetime) constraints in
Smalltalk-80; thus the compiler/interpreter must make worst-case
assumptions, which lead to runtime dispatching in all cases, and pointer
based semantics (because the size of objects held by a variable is not
known statically). There are ``Smalltalk'' versions that do otherwise
have more or less explicit or inferred constraints, e.g. Johnson's TS.

piercarl> * in Pascal 'var x: cmplx' constrains 'x' to denote values of
piercarl>   the type 'cmplx' or *any type with the same structure*. More
schuenem>                        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

schuenem> AFAIK Pascal (like C/C++, Eiffel, Ada) has nameequivalence
schuenem> for (named) types, so the same structure woun't do;
schuenem> Modula-2 is one that has structural equvialence.

Well, I was being very particular: *Pascal* got structural equivalence,
but *ISO Pascal* has name equivalence. The rule was changed a few years
ago when Pascal was officially standardized. I have often used the
distinction between Pascal and ISO Pascal to show how radically
different semantics can become when just a little change is made in the
definition of a language...

piercarl> x; require typeof value(x) equiv cmplx'.

schuenem> What's the difference between "==" and "equiv" ?

Structural vs. name equivalence, at least in my itent. I was making up
notation as I was going along... :-)

piercarl> Since as a rule type metaoperators define not only the storage
piercarl> structure of a new type but also its constructors and accessor
piercarl> functions, a large part of designing a type system is deciding
piercarl> how far one wants to have the compiler go in synthetizing
piercarl> those;

schuenem> Well, like distinguishing type-system from
schuenem> type-constraint-system you could additionally distinguish the
schuenem> implementation of a type (some call it class) from its
schuenem> interface

Ah yes, this is indeed possible and popular. I have been repeating for
years in comp.object that there should be independent reuse algebras for
the three aspects of a type, its interface, specification, and
implementation, so that one can assemble types based on any part of
another type (I like to use the deque example). Very few languages
implement anything like that; Modula-3 among some is notable. In
particular it seems that not many language designers find important to
add the ability to have multiple interfaces for the same implementation,
and even multiple implementations for the same interface are not very
much supported.

schuenem> (type without implem. is an abstract type).

I dislike this use of abstract type; I prefer to leave abastract type to
label the denotation of a type, and call type interface or shortly just
protocol the interface. If one wants to indicate both the type interface
and the type specification there should be a different term. However if
one was sure that the denotation of a type were always called "type
denotation", I think that using astract type for it would not be too
bad. I may seem to finicky with terminology, as usual, but it can be
very confusing...