Re: POSSREPs as union types

Marshall,

In Date and Darwen's The Third Manifesto a type is a named set of values. A possrep (possible representation) maps a subset of a cartesian product (namely those that satisfy the possrep constraint) to values of the type. Two cartesian tuples can map to the same value. A selector invocation (a possrep name with arguments) maps its arguments as a cartesian tuple to the corresponding value.

On Aug 29, 11:07 pm, Marshall <marshall.spi..._at_gmail.com> wrote:

> It occurred to me that possreps have a lot in common with union
> types.

In Plain Ol' Data, the different constituent types of a union type are
disjoint. That's not like possreps, where each possrep of a type runs the gamut of values of that type.

Also, in typical recursive type definitions all the values of each specified form are distinct. Not like possreps. And often they're all legal. Not like possreps. And most importantly values with different tags are distinct. Not like possreps.

> type tree = leaf int | branch tree tree;

Is there a particular language where this is considered a union type definiton?

Classical union type definitions reference other existing types and only introduce the union type. Classical recursive type definitions introduce distinct values with tags (ie leaf & branch), but only a single type (ie tree). But a language could interpret this recursive definition of tree as also introducing types leaf and branch. So I can
see how it could be considered to include a union type definition in the classical sense.

Note that in this definition leaf values are distinct from branch values.

> type point = polar r:real theta:real | rectangular x:real y:real;

If this is a double possrep definition, the two sets of values, polar and rectangular, are by definition the same set. Namely the set of point values. This is not like your previous example (or classical union types). This does not define distinct polar and rectangular value sets.

> Is it necessary that there always be a bijection
> between multiple possreps for a type?

If you mean between their cartesian products, no, because a possrep can involve only some of the cartesian tuples.

If you mean between legal selector invocations, no, because two cartesian tuples can map to the same value.

But if all of a type's possreps' legal selector invocations are in bijection with its values then there is a bijection between legal selector
invocations for different possreps, because you can map between two selector invocations via their value.

> If not, how does
> one convert between them?

One defines each selector and equality in terms of the actual representation and/or other possreps.

I don't know what the "them" are that you want to convert between. Selector invocations denote values of their return type. The alternatives do not define different value sets, they denote the same value set.

> This makes possreps and union types look quite similar
> to me.

Your tree example is interpreted differently than your point example, since the alternate value sets are disjoint in the former but equal in
the latter. Presumably syntax would distinguish them. But even if the rest of the syntax were similar the semantics would still be different.

> It also gives a clear idea of how to differentiate
> between "member functions" that ought to belong
> ("directly" if you will) to the type, and those that are
> less immediately associated: whether or not they
> are constructor arguments.

The only association of operators and types in TTM is via signatures (parameter and return types) with subtyping (of parameter types) (other than those further implied by an operator being a selector or equality). Operators do not "belong to" types. Unless you consider an operator to "belong to" all the distinct declared types of its parameters (and return type?). But such a statement of belonging is just peculiar wording for giving some essentially useless information:
that (per that definition) a given operator has given distinct declared
types.

philip Received on Thu Sep 03 2009 - 22:22:16 CEST