Difference between a type system and a type constraint system

Difference between a type system and a type constraint system

Post by Ulf Schuenema » Fri, 26 Jan 1996 04:00:00



|> 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://hphalle2.informatik.tu-muenchen.de/~schuenem/

 
 
 

Difference between a type system and a type constraint system

Post by Piercarlo Gran » Sat, 27 Jan 1996 04:00:00



>>> Schuenemann) said:

schuenem> Based on your definition I conclude that Smalltalk has a type
schuenem> system but not a type constraint system.

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

 
 
 

1. Paper on constraint-based polymorphic type system in Cecil

The following paper is now available:

                Constraint-Based Polymorphism in Cecil
                 Vassily Litvinov and Craig Chambers

                       University of Washington
                  Technical Report UW-CSE-98-01-01

PoscScript: ftp://ftp.cs.washington.edu/pub/chambers/sbp-tr.ps.gz

We are developing a static type system for object-oriented languages
that strives to guarantee statically and completely the absence of
certain large classes of run-time errors, to enable polymorphic
abstractions to be written and typechecked once separately from any
current or future instantiations, and to avoid forcing code to be
written unnaturally due to static type system limitations. The type
system supports bounded parametric polymorphism, where the bounds on
type variables can be expressed using a mixture of recursive subtype
and signature constraints; this kind of bounding supports F-bounded
polymorphism, Theta-style where clauses, and covariant and
contravariant type parameters as special cases. The type system
coexists with many advanced language features, including
multi-methods, independent inheritance and subtyping, mutable and
immutable state, first-class lexically-scoped functions, and mixed
statically and dynamically typed code. We have implemented this type
system in the Cecil language, and we have used it to successfully
typecheck a 100,000-line Cecil program, the Vortex optimizing compiler.

This is work in progress.  The TR presents nondeterministic
typechecking rules; we have implemented a prototype typechecker as
part of the Vortex compiler.  We are working on the proof of soundness
and a formal deterministic typechecking algorithm.

Vassily Litvinov      http://www.cs.washington.edu/homes/vass/
Cecil/Vortex Project   http://www.cs.washington.edu/research/projects/cecil/

2. Data island logical or strange behavior?

3. Strongly Typed OO Type System

4. Cannot mail directly to files

5. Typed Smalltalk type system

6. Whats the better model for utilising COM/.NET objects with sites?

7. The notions of type and of type constraint

8. Goodbye Wordperfect

9. static_cast<type>(var) vs. (type)var vs type(var)

10. Enumerating system wide hooks, type and processid

11. Determining File System Type

12. which modem type are you using when developing modem_based IVR system

13. file system type