Re: no names allowed, we serve types only

On Feb 17, 9:15 pm, Nilone <rea..._at_gmail.com> wrote:
> On Feb 17, 1:29 pm, David BL <davi..._at_iinet.net.au> wrote:
>
> > Operators can be formalised without a type system too. Simply
> > formalise an operator as a function defined on some domain, where a
> > domain is merely a set (not a "type").
>
> Thanks for the introduction, I haven't seen the typeless model
> before. I don't see how such a system would handle arithmetic
> operators (e.g. + and <) and string operators like concatenation and
> search - could you perhaps give an example?

In a typeless system a unary function could for example be formalised as a triple (D,C,G) where D is the domain, C is the co-domain and G is the graph of the function (a subset of DxC). This is typeless in the sense that a function value doesn't formally have any concept of a defined type. Rather the domain and co-domain are formally part of the function's value as a triple (D,C,G). For example two functions can have the same domain and graph but different co-domains. That makes them distinct. This is actually conventional, as when one determines whether a given function is surjective (i.e. its range equals its co-domain). It wouldn't make sense to ask whether a function is surjective if its co-domain isn't part of its value.

Alternatively a typeless system could instead formalise a unary function as a set of pairs (i.e. what we above called its graph). In that case the domain and range is determined from the graph using projection, but there is no concept of a co-domain.

Similarly a typeless system could formalise a relation in two different ways. One allows for attributes to have domains specified independently of the graph (or "body") of the relation, and these domains represent part of the relation's value. That means that two distinct relations can have exactly the same graph.

Alternatively a relation can be identified with its graph. In that case the domains are determined as the projection of each attribute.

In a typeless formalism one is very clear about what it means for two functions or two relations to be equal. It seems to require more effort to understand what equality means in a typed formalism.

In a D&D type system, a value has a MST, but this actually depends on the prevailing type system. E.g. two different databases could use different type systems. Putting it another way, the MST of a value depends on who you ask :-).

D&D want to ensure that equality of values is independent of declared types. That's why they say that a selector for an ellipse value that happens to specify equal width and height actually returns a value which has an MST of circle. It's like a "magic downcast". They point out that OO systems don't normally work that way. E.g. an OO constructor for ellipse never returns a circle.

I think D&D end up treating relations with the same body and attribute names as equal. i.e. in essence the declared attribute domains are not part of the relation's value. I think they define subtyping of relation types accordingly.

It seems to me that D&D spend a lot of effort discussing ideas that are either eliminated or trivialised in a typeless formalism of the RM. Received on Wed Feb 17 2010 - 19:14:38 CET