Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!wuarchive!cs.utexas.edu!sun-barr!newstop!exodus!rbbb.Eng.Sun.COM!chased
From: chased@rbbb.Eng.Sun.COM
Newsgroups: comp.lang.misc
Subject: Data types are values, and contravariance
Message-ID: <10785@exodus.Eng.Sun.COM>
Date: 1 Apr 91 18:10:13 GMT
Sender: news@exodus.Eng.Sun.COM
Reply-To: chased@rbbb.Eng.Sun.COM ()
Organization: Sun Microsystems, Inc.  Mt. View, Ca.
Lines: 62

Sigh.  Nobody posting has too much of a clue.  If you view a "data
type" as an interpretation of an otherwise typeless sequence of bits
in a data domain D, then that means that a map from a finite set of
names to functions is equivalent to a data type.  But, functions from
D to D are also elements of the domain of "sequences of bits" (*), and
finite simple maps from D to D are also in D.  Thus, data types ARE
values.  You can make them up, pass them around, store them in global
variables, put them in data structures, whatever you please.

(*) Proof omitted because I have forgotten the details, and I believe
that the functions must be continuous in a topological sense within
the domain.

Such a construction leads to some hairy problems for type inference,
but I believe Russell gets around them with a practical hack (so some
type theorist told me once).  Note that Russell, though polymorphic,
is type-checked at compile-time (though if you choose to make
incredibly general use of types, you'd best be ready to help out the
type infer-er with some declarations).

----------------------------------------------------------------

Contravariance is easier.  If you take a set-oriented view of types (X
subtype of Y means every X is also a Y), then the function subtyping
rule is:

  the type of functions mapping from type to to type u (t -> u) is a
  subtype of the type of functions mapping from type v to type w
  (v -> w) if and only if

  (1) u is a subset of w
  (2) v is a subset of t  ( <-- contravariance)

that is,

  (t -> u) <: (v -> w) IFF t <: v AND w <: u.

Thus, a (t -> u) can always be passed in to a context expecting a
(v -> w) because (1) the result is guaranteed to be a subtype of the
expected result and (2) the actual parameter passed in is guaranteed
to be a subtype of the expected parameter.  If the contravariant part
of the rule is reversed, then you could get something like this:

  TYPE super = PROCEDURE (x: INTEGER) : INTEGER;
  TYPE bogus = PROCEDURE (x: POSITIVE) : POSITIVE;
  PROCEDURE expose_bug(f : super)
  BEGIN
  ... FOR I = 1 TO 10 DO sum = sum + f(I) + f(-I) END ...
  END

If a bogus were passed to expose_bug, it would be passed a negative
number, which is not correct.  This rule causes a minor problem in
some (statically-typed) object oriented languages, because the
parameters to methods are forced to remain at the supertype.

----------------------------------------------------------------

Anyone care to explain Tarski's Q-systems, and/or why they are
relevant to programming languages?

David Chase
Sun