🚀 go-pugleaf

Can anyone provide any references to programming languages that
treat types as first-class values?

The sense of "type" that I mean is "a partial specification of behaviour".

If a type is meant to represent some distinguished set of "values",
that is, some subset of the universe of discourse (whether this be
data, ADTs, objects, functions, processes, etc.), then a type expression
can be viewed as a specification (predicate) that values may or may not
satisfy.  The kind of properties types distinguish should be (just) enough
to determine that values be used in a "type-safe" way [i.e., (partial)
functions are only applied to appropriate values; objects are never sent
messages that they will not understand ...].

So, for a type to be first-class:

1. you must be able to bind it to a variable, pass it around, etc.,
2. test whether a value satisfies it (and, if it does, be able to use that
   value in a type-safe way within the scope of the test),
3. produce new types from old at run-time by means of type-operators.

Any pointers would be appreciated.  I am especially interested in
functional and object-oriented languages that treat types as first-class.

NB: There is a theory of types as values -- or special kinds of functions,
called "retracts" -- introduced by Scott, but I do not think this has ever
been used as the basis of a programming language.

Oscar Nierstrasz

-------------------------------------------------------------------
Dr. O.M. Nierstrasz                 | Tel:    41 (22) 787.65.80
University of Geneva                | Fax:            735.39.05
Centre Universitaire d'Informatique | Home:           733.95.68
12 rue du Lac, CH-1207 Geneva       | E-mail: oscar@cui.unige.ch
SWITZERLAND                         |         oscar@cgeuge51.bitnet
-------------------------------------------------------------------