🚀 go-pugleaf

In article <7597@cui.unige.ch>, oscar@cui.unige.ch (Oscar Nierstrasz) writes:
|> 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.
|> 

Here is the situation in Hermes:

Hermes has a built in *program* data type.  Programs contain
*declaration*s; declarations contain *typename*s

A value of type *typename* is a first-class type.

It meets criterion 1.  Variables can be declared
to be of type *typename*; values of type *typename*
can be stored in these variables, passed around, etc.
Typename literals generate static values of type *typename*.

Now in Hermes there are two kinds of typing:  static, and dynamic.
Static type is the usual case: variables are just declared
to have that type.  Dynamically typed variables are declared
to have the static type *polymorph*.  The *type of* operator
applied to a polymorph produces a value of type *typeof_value*,
which contains a *typename* and the set of definitions in terms
of which the typename was defined.  Applying *type of* and
then comparing the typename component to the value of a typename
variable performs the test of criterion 2.  To use the
dynamically typed value in a type-safe way as a value of
its proper type, you must cast the polymorph into a value
of the appropriate type using an *unwrap* statement.  An exception
is raised if the polymorph has the wrong type for the target of
the unwrap statement.  Statically typed values don't need
a run-time operator to check their type.  You can check
whether a typename value has a particular static literal value
by comparing the typename variable to a typename literal.

To produce new types from old as required by criterion 3, you
must build a value of type *type_definition*.  These type
definitions can be used to build new objects of type *program*
which use these new types.

-- 
Rob Strom, strom@watson.ibm.com, (914) 784-7641
IBM Research, 30 Saw Mill River Road, P.O. Box 704, Yorktown Heights, NY  10598