Re: Values have types ??

Alfredo Novoa wrote:
> Costin Cozianu <c_cozianu_at_hotmail.com> wrote in message news:<bjbbdu$hf0jo$1@ID-152540.news.uni-berlin.de>...
>
>

>>In the D&D proposal a value is guaranteed to have a most specific type 
>>(MST), which is largely undefined in the book that a few people around 
>>here have come to recite like the bible.
>>
>>In the above case I'd propose that the MST is, well, {2}.
>>
>>2 then has the "type" {2}

No, actually {2} is the set with a single element 2. A name for the type is superfluous, actually D&D are totally inconsistent when they require that types have names ("types are named sets") since relation types and tuple types obviously don't have user-defined names, and at best should be system generated as such, there's no reason for the system not to generate a name for the type {2}.

In any case, allowing specialization by constraint, and then declaring that all values have a MST they opened (unknowingly) the Pandora's box.

Imagine that a user defines 2 types (in Tutorial D clumsy syntax, if you don;t believe this syntax go to page 259):         

	TYPE PRIME IS INTEGER WHERE IS_PRIME(INTEGER)
	TYPE EVEN IS INTEGER WHERE INTEGER%2 == 0

Now what's the MST(2) ???

So bottom line you have 2 options :

• either the type system is inconsistent opening the possibility of runtime type errors, or undefined and surprising results following from unexpected decision with regards to MST and late binding of methods
• or the type system is trivial and all value x have the type {x}. The type system has to allow anonymous or at least automatically named type anyways. The reason for that is that given 2 subtypes defined by 2 constraints C_A and C_B the system has to "automagically" generate the constraint and the subtype < C_A && C_B >, and furthermore given 2 other constraints C_X and C_Y the system has to automagically generate <C_X && C_Y> and to resolve the question whether C_X && C_Y is or is not the same with C_X && C_Y, and imagine this for all the subtypes in question.

Given a user defined ADT algebra this is also known under the general term as "implication is undecidable, given an abstract algebra you cannot devise an algorithm that will decide whether a particular equation follows from another. So the only safe solution is to allow for each element to have the MST(x) = {x}

And with all these jazz about unresolved lattices of specialization by constraint subtypes, what do we buy ? Petty nothing.

This whole enchillada solves the "difficult" proble of "late binding" known l,ong before D&D as predicate based dispatch, i.e. substituting a very simple if then else or case with non-sensical type declaration:

I.E substitute

	if (is_circle (x)) then
		do_the_circle_thing (x)
	else
		do_the_general_thing_for_ellipses(X)

With the respective type declartions for specialization by constraint (I won;t repeat here the clumsy syntax, which is far worse than the above from all points of view).

This is an entirely puerile construction, broken by design, a definite trap for unsuspectign users, because D&D decided that the whole discussion of OO is about subsets (i.e. circle is a ellipse). So a whole philosophical discussion buys us nothing when it comes to real software, and that because D&D never took their exercise seriously. They never build a whole formal system they just waved their hands at the problems (that is if they figured out at all there are problems), they never analyzed the full implication of their decision and they didn't even built a pet example. Just look at page 259 where

        TYPE PLANE_FIGURE .... ;
and

	TYPE ELLIPSE
		IS PLANE_FIGURE POSSREP {
			A LENGTH,
			B LENGTH,
			CTR POINT
			CONSTRAINT  A>= B  ??? blunder
		}
	TYPE CIRCLE IS ELLIPSE
		CONSTRAINT THE_A {ELLIPSE } = THE_B {ELLIPSE}
		POSSREP { R= THE_A (ELLIPSE) ,
			  CTR= THE_CTR (ELLIPSE) };

Now if they figured out what to put in the dots for PLANE_FIGURE and had built even this toy example fully and make it actually be useful for some toy computation, they'd had realized the utterly unnecessary and painful exercise that the user of such a system is submitted to, and what unnecessary techinical difficulties will happen to system implementors.

In real mathematics and CS, type theory is not about values at runtime, but about *terms* and *evaluations* in a formal system of logic. Unfortunately Date's knowledge of the domain is limited to half a semester introductory course, since I can't imagine even a bachelor degree in Mathematics nowadays being unaware of Tarski's work in logic for example.

Google for Robert Constable Naive Type Theory, and you'll find the minimal introduction in type theory. I'll add a most useful book:

Paul Taylor : Practical Foundations of Mathematics

that is a delightful and very cultured and subtle introduction into the avatars of building consistent and useful formal systems in the spirit of modern mahtematics, especially when applied to computer science.

Specialization by constraint and the whole D&D typing system (with POSSREP see the ellipses on page 259) should be discarded as broken, dangerous and most of all useless (oferring absolutely no real benefits in building system).

>
> Regards
> Alfredo

Best,
Costin Received on Mon Sep 08 2003 - 03:58:38 CEST