🚀 go-pugleaf

In article <15343@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
|In article  <STEPHEN.92Apr14174618@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*.
|
|That is just another way of saying that types are static properties of
|programs, which is far from a universal view.  It also happens to be
|the case that sets make an excelent implementation of types.

Ha ha. First off, "type" is a technical term from mathematical logic,
and it has various approximate implementations in programming
languages, but that isn't going to change the idea; just as you're
never going to persuade me that floating point numbers really ARE the
Reals, just because that's the approximation some languages use (for
whatever excellent reasons they might have).

Secondly, sets aren't even very nice mathematical objects, let alone a
sound basis for computation. The whole idea of approaching computation
non-constructively is a little, er, bizarre, n'est ce pas? To
implement a set-based language semantics you have to implement the
universal equality relation on which set theory is founded. So tell
me, how do you compare functions?

So obviously we're at cross purposes here.

|]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).
|
|I can't imagine what you are trying to say here.  A language with
|finite first-class sets has first-class sets.  And there are many that
|do have them.  Furthermore, it is a simple matter to represent and
|compute with infinite sets.  For example the complement of a finite
|set X can be easily represented by a data structure that enumerates X.
|Set operations on infinite sets can keep representations of the
|argument sets, they don't have to do infinite operations.  First-class
|predicates can be used to define sets by extension.

But given an arbitrary object, how do you test for membership? You
can't. But that's one of the fundamental set operations - and it's
squarely in the set of operations that types DON'T have, which was my
point.

|I could implement all this in a few hundred lines of lisp, but no
|doubt it has already been done.  Of course if you allow full
|generality of these operations, you have some expressions that are not
|computable, but that is no different from any other sort of
|non-terminating computation.

Hm. Ok, score a maybe with that disclaimer. I've used a language with
an undecidable type system, of course, and it isn't so bad (in fact it
may be well worth it to get types like "list of primes"). But I'm
really unhappy about having nontermination while trying to check type
conformity *at runtime*, because I'm not sure this is predictable or
avoidable. Intuitively, it seems to me that in order to pass a
function as an argument under this scheme, I'd have to have listed all
the *particular* arguments that can be passed - like APL's reduction
in the Bad Old Days.
----------------------------------------------------------------------
stephen p spackman         Center for Information and Language Studies
stephen@estragon.uchicago.edu                    University of Chicago
----------------------------------------------------------------------