🚀 go-pugleaf

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