🚀 go-pugleaf

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