🚀 go-pugleaf

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