Re: The Practical Benefits of the Relational Model

Costin Cozianu <c_cozianu_at_hotmail.com> wrote in message news:<3D99EEDD.40203_at_hotmail.com>...

> I believe your web site talks about a data access engine and some data
> access components. Which one is it ?

Dataphor Data Access Engine (or DAE).

> Types may have different precise definition in different type systems,
> but they do have a certain common functionality, that you have to
> provide. This is described briefly in "Type Systems".
>
> Stating that "my definition is different than yours" is not very
> helpful.

Thus far this conversation has yielded very little agreement, and I hope it is not because we are trying to out-argue each other. The cause, I think, is that we have differing assumptions. I have taken a kind of mental step back and I think I see where you are coming from.

> I'm open to all definitions that come with a formal system or
> even a slightly informal one, as long as we can understand the logical
> implications, we can compare advantages and disadvantages.

Here is part of my realization, all arguments and thinking I have given to this point assume we are working within 1st order predicate logic. In other words, the system (in my mind) was already in place. I assumed this because any "type model" to be used within a relational system must surely be based on the same logic system as the relational model. I am no logician, but my understanding is that 1st order predicate logic defines types very clearly as sets of possible values.  With this perspective, you can see that any other definition of type does not correspond with the one by the same name in the relational model.

To clarify an earlier statement: The specific domains of possible values are orthogonal to the relational model. Alternative "type systems" and other alternative logic systems are explicitly excluded.

> > I certainly don't consider a implementation contract (interface) a
> > type, and the implementation is (operators are) also orthogonal to
> > type.
>
> Either you confuse types with implementation, or you accuse me of
> confusing the two.

I am accusing you of this because you stated that an "Interface" (as exists in Java) is a type. Again, now that I understand where you are coming from, these arguments are irrelevant. Certainly I can make no rational argument against new logic systems that define type as whatever.

[other responses snipped for the same reason]

> Let's see an example ("real world" :) ). I have a cryptographic
> algorithm that works over finite fields. Let's rather say informally:
> P(private_key)= public_key.
>
> Now I have the mathematical algoithm for P. Obviously, I don't want to
> write that code again and again, for different finite fields, therefore
> I'd say that the algorithm should be written *once* and for all for the
> most generic type FINITE FIELD.
>
> Now do you accept that FINITE FIELD is a type ?
> If you construct for me a set of elements, can I verify that they indeed
> form a finite field, in other words, can you really separate the set
> from the structure defined over it ?
>
> By the way, how would you declare such a program in D4 ?

> > Mixing them in the way you describe has led to massive
> > confusion on the subject.
>
> Kind of patronizing, don't you think ?

What can I say... I did not mean to offend, merely to state my opinion frankly.

> I think the subject is not confused at all, unless you are confused
> about the subject, or you select the wrong references to prove your
> point. If you take time to study the _scientific_ work in the field
> you'll see that there's a rather large consensus.

Let's be fair, the domain (pun excused) of our product is that of the relational model of data which is a logic system based on 1st order predicate logic. Within the RM, we have not encountered any general logical or practical problems. To the contrary, we actually gravitated to the RM as a _solution_ to many practical problems before encountered. We are particularly happy with the simple but capable definition of type within the RM.

> No, we dont need to agree what _exactly_ a type is, unless you want to
> impose on me the view of Mr. Date.

I would say that it is pretty important that we agree on what a type is in the RM.

> You'd have to have some darn good
> arguments, because, you know, there's an established discipline at the
> confluence of Logic, Algebra and Computer Science that has come up with
> an established theory and lots of *practical* result, and it doesn't
> operate by Mr. Date's definition.

I am certainly not qualified to speak for them, but I think their position is that there is no need for another logic system. The RM has everything that is sufficient and necessary, so why come up with another "model." I think (hope) there is consensus on what a type is in the RM. Within that definition, what Date and Darwen have done is to spell out how to do type inheritance.

> In the meantime TTM has come up with a
> partial theory and no practical results. Where by result I mean a
> practical implementation of the system that is able to prove its
> usefulness.

We have seen _many_ practical benefits from our implementation of TTM.

> Ideally, as in the case of ML, the actual type systems
> should be _provable_ safe and sound.

It is not provable in general that a loop will ever terminate, but we don't argue the usefulness of them.

> A precise definition of type will be different in different systems,
> each with its own benefits.

As pointed out by the original posting the RM yields many benefits, so my vote is for a type system that works within the grounds of the RM.

> But we have to agree what are the essential
> roles and benefits of having a type system. And you can evaluate how Mr.
> Date's proposal compare with other type systems.

I suppose the "essential roles and benefits of having a type system" are best illustrated by the classic problems with propositional calculus.

> So far you have avoided to acknowlegde even the most obvious limitations
> of Mr. Date's proposal, like subtyping is undecidable.

I have not avoided acknowledging them, there simply is nothing more to say about them then "yes, the system cannot enforce that I define my types correctly. Yes, this means the type developer can break things.  I am okay with that." As touched on above in my loop example, many language elements are the same way.

> > Type and value are inextricably linked. You can't talk about one
> > without the other.
>
> "Inextricably linked" sounds very informal to me. You can't say in
> Mathematics that 2 definitions (type and value) are "inextricably
> linked". Whenever you have a recursive definition or a system of
> recursive definitions, you have to actually show the way out of recursion.

It was meant to be informal. If you would like a formal treatment, consult references on 1st order predicate logic. The best I can offer is perhaps a more precise informal description: The concept of "value" is introduced as part of "domain" (type).

> If you know French, I'd strongly recommend an article: Giuseppe Longo:
> Cercles vicieux, Mathématiques et formalisations logiques. It's rather
> short and very dense and related to type systems. Maybe it can change
> your view on "inextricably linked".

A pearl of wisdom I will have to forgo, as I do not speak French.

> Do you actually verify the subtyping relation A <: B ?
> Can you identify when 2 distinctly declared types are equal?
> Do you provide automatic inference of the type lattice ?

No No and No. (see above)

> More to the point: do you really have a choice about those issues within
> the framework of TTM "type inheritance model" ?

A choice? Yes I suppose there are many choices an implementer can make in this regard, so long as conceptual integrity is maintained. For example, were the implementation to restrict user defined types such that they could only be subtypes of "system" types, than I imagine that the system could go much further (if not all the way) in ensuring and inferring the "lattice".

> Or to say it more bluntly, is it implementable ?

So far, so good. :-)

Regards,

--
Nathan Allan