Re: Notions of Type

Excellent commentary here, Marshall - I was going to write a similar note about Bob's suggestion, but wouldn't have explored it as thoroughly as you did here.

Marshall wrote:
> Bob Badour wrote:
> > Marshall wrote:
> >
> > > Consider PROJECT:
> > >
> > > PROJECT: Relation, Set-of-attributes -> Relation
> > >
> > > So for PROJECT of an x,y point over x, we pass it two
> > > things:
> > >
> > > 1) A relation defined over attributes x and y
> > > 2) ???
> > > and it returns
> > > 3) A relation defined over attribute x (aka "profit")
> > >
> > > Whoops! Doesn't fit the template. The second argument isn't
> > > a relation. So, strictly speaking, this is not an algebraic operator,
> > > because it isn't closed over the type Relation. Exercise for the
> > > reader: what *is* the type of the other argument? This should
> > > make your head hurt a least a little bit.
> >
> > It is a relation of degree 1 and cardinality N representing a set of N
> > attribute names.
>
> Yes and no.
>
> In its most minimal form, it is a set of attributes. A set of
> attributes is not a relation. However, because of the
> awesome representational power of relations, it is easy
> enough to construct a relation that, as you say, represents
> a set of attributes. In other words, the fact that you were
> able to construct an answer in the form of a relation says
> more about the tremendous flexibility of relations than it
> does about the type of the parameter to PROJECT.
>
> Also, note that this solution can fail in so many ways.
> The second argument is hardly any general relation; it
> has to be specifically a relation of degree 1. And the
> lone attribute of this relation: what type is it? String?
> That doesn't quite work; it is drawn from the domain
> of attribute names, and not just any attribute names,
> but specifically the ones from the other parameter!

In itself, I don't think that's a problem, as that's the entire basis of parameterized types (or perhaps dependent types), which essentially imposes a constraint on the relationship between parameter types of a function.

> It gets worse: the two relations are not of the same
> order. The first relation is of the base order and
> the second relation is of a higher order, since it is
> a relation over type components. And it is here that
> we have to start being *very* *careful* because we're
> wandering into paradox territory.
>
> (It is exactly the area of considering types as values
> that is a current area of study for me, largely motivated
> by the desire to understand and avoid these paradoxes.)
>
> Two side notes:
>
> 1) I observe that TTM is extremely conservative in
> avoiding getting anywhere near the territory
> of thinking of types as values.
>
> 2) The Tropashko algebra doesn't have any of the
> above limitations. Specifically note that its two operators
> work completely generally with any two relations, never
> requiring one of them to be structured a particular way,
> nor does it require us ever to address the issue of types
> as values. In fact, those operators can fail in only one
> respect (the same as for natural join,) namely the
> unification of the attribute typespaces. Specifically, the
> one way to get a failure is to have an attribute with
> the same name in both relations, but a different type
> in each.

Alloy also side-steps this sort of failure by basically ignoring the areas of disjunction. In other words, the second parameter in your PROJECT operator could have whatever attribute names you like; the result would have only the attributes in the intersection. (Intersection of WHAT is a different issue - as Marshall indicated, if the attribute names are values in tuples of the second parameter, then there's the need for a "bridge" betwen the values domain and types domain, of the first parameter. Hence higher-order relations, which I think are extremely useful for such things as database standards, system catalog, and some other applications.)

(In any event, this is much more useful in Alloy for treating object "attributes" as relations and using joins rather than navigation. There are no pesky typespace issues of this type, since the joins cheerfully ignore attributes outside the intersection.)  

> Marshall
Received on Fri Aug 18 2006 - 13:20:23 CEST