Re: Any and Every... (was Re: Eval)

[address@hidden]

"Peter H. Froehlich" <pfroehli@ics.uci.edu> writes:

> Hi!
> 
> Maybe I am not using my terms correctly, so let me try again (someone
> please hit me if I should take this offline).
>
> Maybe my problem is the exact definition of "union type" and
> "intersection type"?

I will be yelled at by the `static typing' camp.  I accept this.  In
any case, I'll try to answer your question in a way that will make
both camps happy.

A `union' type is what you get when you combine types in an
`either-or' manner.  For instance if something could be either a
scalar number or a string, you might want to declare a union type of
`scalar-number-or-string' so that your type system will complain if
you try to use a matrix.

If you don't know the type of an object when you are writing the code,
you need to be able to say `anything at all', which is the union of
all types.

An `intersection' type is what you get when you combine things in an
`and' manner.  For instance, if something must be a positive integer
less than 100 and divisible by two, you might want to declare an
intersection type of `integer', `> 0', `even', and `< 100'.
(Provided, of course, that your type system can express this.)

The `intersection' of all types would include all objects for which
*every* type predicate correcly answers `true'.  (The `union' of all
types would include all objects for which *any* type predicate
correctly answers `true'.)

The `intersection' of all types ought not to contain any elements.  If
it does contain an element, then your type system is either
inconsistent or too feeble to be useful.  But let me put in a caveat
here to avoid flamage.  Some languages have a `void' or `null' object
that may be assigned to any variable (like in Java).  I think it is
best to think of this in this way:  every type you declare has an
implicit union with `null'.

> I think Eiffel has a "not really existing type" (almost wrote "virtual
> type" but that might be confusing) called "ALL" which defined as the
> subclass of all other classes in a system.
> 
> Therefore it has all the methods of all the classes and "closes" the
> inheritance hierarchy at the bottom. Would you even call that an
> "intersection of all class types" or rather a "hodgepodge type"? 

Well, it would be an intersetion of all types, but can you instantiate
one?  Remember, it would (correctly) answer `true' to *every* type
predicate, and presumably would be a legitimate argument for *any*
method in the system.  Would it be equal to itself?  Is it `constant'?
Since it is `consp' (by definition), can you call RPLACA on it?

> For "ALL" my characterization seems to apply, i.e. "in theory" you can
> assign a value of type "ALL" to every variable, but you can never
> assign any value of another type to a variable of type "ALL".

Suppose you had an `intersection' of all types, and this type was
called `all', and you had an instance of an object of this type.
Then, since this instance satisfies *all* type predicates, it could be
(correctly) assigned to any variable.  Now if your type calculus is
sufficiently rich, you will have inconsistencies.  Suppose variable X
is declared a `positive integer' and variable Y is declared a
`negative integer'.  Can you prove that X will never equal Y?  Not if
they could both be the `void' object.

> BTW, I've been carrying around this "question" or "confusion" for at
> least three years now, always promising myself to sit down someday and
> work it out. Today it just struck me as a good idea to post it here
> instead. :-)

Definitely worthwhile to bypass this particular confusion.  Too many
people confuse `intersection' types with `union' types.