From: objsys@netcom.com (Bob Hathaway)
Newsgroups: comp.object,comp.lang.misc,comp.lang.functional
Subject: Re: Types as first-class values?
Date: 16 Apr 92 02:32:08 GMT
Article-I.D.: netcom.plzjq!b.objsys
Organization: Object Systems

In article <STEPHEN.92Apr15015720@estragon.uchicago.edu> stephen@estragon.uchicago.edu (Stephen P Spackman) writes:
>In article <nmyjmaf.objsys@netcom.com> objsys@netcom.com (Bob Hathaway) writes:
>|In article <STEPHEN.92Apr14174618@estragon.uchicago.edu> stephen@estragon.uchicago.edu (Stephen P Spackman) writes:
>|>In article <7597@cui.unige.ch> oscar@cui.unige.ch (Oscar Nierstrasz) writes:
>|>>  2. test whether a value satisfies it (and, if it does, be able to use that
>|>>     value in a type-safe way within the scope of the test),
>|>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*.
>|
>|If by value he means object in the OO paradigm, this makes perfect sense as
>|in Modula-3's typecase statement.  So, a construct should be able to
>|determine if an object is a member or instance of some class, and if so,
>|perhaps interact with that object in a statically typed (safe and efficient)
>|way.

  [I forgot to mention that typecasing should be used with caution, since
   one of the goals of OO is to avoid distributing the knowledge of types
   throughout a program (something OO neatly avoids), which the typecase
   construct seems to do.  I believe that messaging is the typical solution.]

>But those aren't types in the technical sense. Nor are they sets.
>Types lack dynamic membership test (or rather, it can in principle be
>resolved statically), and sets permit something to belong to multiple
>sets arbitrarily.

Why do you claim that types lack a dynamic membership test, are you
distinguishing between types and classes?  I was using the terms
synonymously.  Also, static types can be resolved statically and
dynamic types dynamically, I'm not sure if I follow you.

>|>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).
>|
>|Since set operations are quite small (add, delete, includes, ...), I don't
>|see what is so difficult, almost any representation seems to suffice and
>|if you need a set, you'll have to incur the expense anyway.  But I do agree
>|that small simple sets (if not all sets) should be implemented as
>|efficiently as possible whether provided by a programming language (Pascal,
>|Modula) or library (Smalltalk).
>
>But one of the required operations is membership test! What algorithm
>do you propose to check if some function is in some set? That's why
>you need types in the type theory sense: they don't barf on functions
>considered as objects.

I think the set "includes" operation above covers the membership test.
Since functions are objects with a class (or meta-class), they can certainly
have an equality operation, its just their signature in the simplist case.

bob
objsys@netcom.com
Newsgroups: comp.object