🚀 go-pugleaf

Oscar Nierstrasz writes:
>Can anyone provide any references to programming languages that
>treat types as first-class values?
 
Try SETL for starters.
 
Set theory defines the algebra of types you want.
 
The real problem for data abstraction languages is to define 
representation mappings between concrete sets representing the
same abstract set, which are implicitly applied when needed.
 
Combine set theory with representation mapping and you have 
accomplished most of the objectives of object oriented programming.

--                    
INTERNET:  jim@netlink.cts.com (Jim Bowery)
UUCP:   ...!nosc!ryptyde!netlink!jim
NetLink Online Communications * Public Access in San Diego, CA (619) 435-6181

I'm a little confused by the notion of type you are looking for: the
fact that you specify that you want a membership TEST suggests that
you're thinking of a set theory rather than a type theory at all -
types are properties of the expressions, not the values, *even when
the types are values themselves*.

Languages that provide first-class types include Russell and (the
spectacularly non-trivial) NuPRL (which doesn't think it's a
programming language, but is. We had a language called Brouwer that
used the same logic as the source language for a compiler. I;d point
you at that but I don't thnk there's a running implementation
anymore, or much in the way of literature).

Languages that provide first-class sets? I can't think of any; in
fact, I'm not sure how you could do that. Unless you restricted
yourself to small finite sets a la SETL, most of your primitives would
be too expensive (the advantage of the type-theoretic approach is that
while compilation may fail to terminate unexpectedly, a successfully
compiled programme won't misbehave in that way).
----------------------------------------------------------------------
stephen p spackman         Center for Information and Language Studies
stephen@estragon.uchicago.edu                    University of Chicago
----------------------------------------------------------------------

Oscar Nierstrasz writes:
>Can anyone provide any references to programming languages that
>treat types as first-class values?
> 
(Jim Bowery) writes:
>Try SETL for starters.
> 
>Set theory defines the algebra of types you want.

I would have thought that any algebaraic system that allows you to
define algebaraic structures at run-time is treating types as first
class objects. For example defining a permutation group by specifying
generators at run-time is in essence creating a type that defines the
bahaviour of all elements of the group. In addition if you can then
compute properties of the group (eg: its order) than are you not
computing the properties of a type (since the group is a type)?

graham
--
Graham Matthews                 And it's true we are immune
Pure Math, Uni.Sydney, Oz       When fact is fiction and T.V. is reality
graham@maths.su.oz.au

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

In article <STEPHEN.92Apr14174618@estragon.uchicago.edu> stephen@estragon.uchicago.edu (Stephen P Spackman) writes:
>	I'm a little confused by the notion of type you are looking for:
>	the fact that you specify that you want a membership TEST suggests
>	that you're thinking of a set theory rather than a type theory at all
>	- types are properties of the expressions, not the values,
>	*even when the types are values themselves*.

I don't understand the significance of this distinction.
The extensional definition of a predicate is the subset
of the universe/domain over which the predicate is true.
So what does it matter whether we speak of an object having
a property, or whether we speak of an object being a member
of the set which defines the property?

>	Languages that provide first-class sets?  I'm not sure
>	how you could do that, unless you restricted yourself
>	to small finite sets a la SETL.

I added first-class sets to a higher-order lazy functional language.
Sets may be infinite, and may contain functions or even other sets.
However, I had to greatly restrict the _operations_ over sets.
(Essentially, I had to assume that my sets are recursively enumerable,
not decidable, and hence there isn't even a set membership test!
The functionality of these sets is, however, adequate to express
any 1st-order Horn logic program.  It may be published soon
in the Journal of Functional Programming -- I recently returned
my corrections to the proofs).  The language does _not_, however,
offer types as objects. 

------------------------------------------
Frank Silbermann	fs@cs.tulane.edu
Tulane University	New Orleans, Louisiana  USA

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?

My memory is quite fuzzy here, but there is an interesting paper entitled "Data
Types are Values", by Donahue (?) et. al., published around five years ago in
ACM TOPLAS.  They talk about a programming language, Russell, that illustrates
their ideas.  I believe a free, real working Russell implementation is
available somewhere.  I can get the full reference, if you like.


bv

--
Brian Victor                 Tivoli Systems                 victor@tivoli.com
                   ...!cs.utexas.edu!tivoli!victor

In article <1992Apr15.150059.8354@cs.tulane.edu> fs@cs.tulane.edu (Frank Silbermann) writes:
|In article <STEPHEN.92Apr14174618@estragon.uchicago.edu> stephen@estragon.uchicago.edu (Stephen P Spackman) writes:
|>	I'm a little confused by the notion of type you are looking for:
|>	the fact that you specify that you want a membership TEST suggests
|>	that you're thinking of a set theory rather than a type theory at all
|>	- types are properties of the expressions, not the values,
|>	*even when the types are values themselves*.
|
|I don't understand the significance of this distinction.
|The extensional definition of a predicate is the subset
|of the universe/domain over which the predicate is true.
|So what does it matter whether we speak of an object having
|a property, or whether we speak of an object being a member
|of the set which defines the property?

Ok. So the problem is that there's an extra layer of modelling going
on with a progamming language. The extension of an implementation of a
type is a set of bitpatterns, the relationships between the _ of which
(you can't say this in English, can you? Try again), which
bitapppterns aren't necessarily in any particular relationship between
different types. So extensional equality at implementation level is
uninteresting (and not checkable, either: determining if a given
bitpattern might be a function in int -> int, eg, is not something you
want to have to do).

Extensional equality at the formal language definition level is
different, but I'm not sure it's significantly different; if I happen
to write my language spec so that both integer zero and te empty list
map map to the empty set, well, who cares? It isn't going to be
detectable within the language, because all the PROVIDED comparison
operators and so forth are going to be described. The formal
semantics, in short, is going to be far from unique.

I just don't think that we're discussing set theory at all, because
the thing about programmes is how they're constructed and where they
can get to in finite time: values have their static properties by
construction and only by construction.

Am I being unnecessarily confused?

|>	Languages that provide first-class sets?  I'm not sure
|>	how you could do that, unless you restricted yourself
|>	to small finite sets a la SETL.
|
|I added first-class sets to a higher-order lazy functional language.
|Sets may be infinite, and may contain functions or even other sets.
|However, I had to greatly restrict the _operations_ over sets.
|(Essentially, I had to assume that my sets are recursively enumerable,
|not decidable, and hence there isn't even a set membership test!
|The functionality of these sets is, however, adequate to express
|any 1st-order Horn logic program.  It may be published soon
|in the Journal of Functional Programming -- I recently returned
|my corrections to the proofs).  The language does _not_, however,
|offer types as objects. 

If there's no membership test, then I don't think it qualifies as a
set. Still a useful object, though, I agree.
----------------------------------------------------------------------
stephen p spackman         Center for Information and Language Studies
stephen@estragon.uchicago.edu                    University of Chicago
----------------------------------------------------------------------

oscar@cui.unige.ch (Oscar Nierstrasz) wrote:
> Can anyone provide any references to programming languages that
> treat types as first-class values?

David Harland's language Poly does this.  It's described in:

	AUTHOR: Harland D. M David M.
	TITLE: Polymorphic programming languages
	IMPRINT: Chichester Horwood 1984
	SERIES: Ellis Horwood series in computers and their applications 25

From what I've seen of it, it looks like a hacker's dream and a
theoretician's nightmare.  It's been implemented on special-purpose
hardware - the Linn Rekursiv, also designed by Harland.


-- 
--  Jack Campin    room G092, Computing Science Department, Glasgow University,
17 Lilybank Gardens, Glasgow G12 8RZ, Scotland   TEL: 041 339 8855 x6854 (work)
INTERNET: jack@dcs.glasgow.ac.uk or via nsfnet-relay.ac.uk    FAX: 041 330 4913
BANG!net: via mcsun and uknet     BITNET: via UKACRL    UUCP: jack@glasgow.uucp

oscar@cui.unige.ch (Oscar Nierstrasz) writes:

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

>....

In BETA a pattern is a first-class value in the sense that a variable
may be assigned a pattern. Such pattern values may be passed around as 
parameters and returned as the result from functions. 

Consider patterns

	T: (# ... #)

with subpatterns

	T1: T (# ... #);
	T2: T (# ... #)

The following is a declaration of two pattern variables

	F1,F2: ## T

F1 and F2 may be assigned pattern T or subpatterns of T.

Ex.

	T1## -> F1##;  { F1 is assigned the pattern T1}
	&F1[] -> R1[]; { a new instance of F1 is created; since the value
			 of F1 is the pattern T1, an instance of  T1 is created}

	T2## -> F2##;
        F2## -> F1##   
	&F1[] -> R1[]; {an instance of T2 is created}

Since a pattern may be used as e.g. a class or a procedure, classes and
procedures may be passed around as arguments and results of functions.

By using pattern variables instead of virtual patterns (procedures)
it is possible to change the methods of an object after it has been created.

Pattern variables are relatively inexpensive in BETA and used for many
purposes. They are of course NOT like Smalltalk metaclasses.

>So, for a type to be first-class:

>1. you must be able to bind it to a variable, pass it around, etc.,

I think this is satisfied.

>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),

	At run-time it is possible to test the value of af pattern variable

	F## = T1	true if F## denotes T1

	F## < T1	true if F## denotes a subpattern of T1

	etc.

>3. produce new types from old at run-time by means of type-operators.

	The only type-operators for combining pattern variables into
	new patterns are pattern declarations where pattern variables
	may be used as attributes. This is perhaps not what you want?

I will be happy to supply more information.

Ole Lehrmann Madsen
Computer Science Department
Aarhus University
Ny Munkegade
DK-8000 Aarhus C, DENMARK
Tel.: +45 86 12 71 88 Fax.: +45 86 13 57 25
E-mail: olmadsen@daimi.aau.dk

I am posting this for a friend of mine who does not have access to the net. 
If anyone has suggestions, please mail me. 

We can represent each node in a binary tree by
 

          type node
                =record
                 value=integer;
                 link =^node;
                 Rlink=^node;
                 end;

My friend wants procedures 

1. to create a binary tree from a file which contains an inorder and 
post order sequences of a tree T

2. list all the leaf nodes of the tree T.

3. to delete a node S from a binary tree T.

4. list the data files of the nodes of the binary tree T by level.  

Thanks.