🚀 go-pugleaf

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.

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

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.
-- 
					David Gudeman
gudeman@cs.arizona.edu
noao!arizona!gudeman