Re: Distributed foreign keys (was Re: Category Types)

From: Costin Cozianu <c_cozianu_at_hotmail.com>
Date: Sat, 05 Jul 2003 23:40:08 -0700
Message-ID: <be8g3t$2atlh$1_at_ID-152540.news.dfncis.de>


Marshall Spight wrote:
> "Costin Cozianu" <c_cozianu_at_hotmail.com> wrote in message news:be7p79$25miq$1@ID-152540.news.dfncis.de...
>

>>Types are not sets nor are they
>>predicates. For sets and predicates we already have, well, sets and
>>predicates.

>
>
> Can you expand somewhat on what you mean by "types are not sets?"
> It seems like I've read enough times that the integers, Z, are a set, and
> it certainly seems like integer is a type. In fact, the Cardelli paper you
> cite below defines "type" in the glossary as "a collection of values"
> which sounds a lot like a set to me. (I'll try to finish the paper tomorrow;
> it looks good.)
>

What it specifically means is that a type system where any set (of values) can define a type is counter-productive (it will have bad engineering properties like undecidability).

Basically, any type is associated with a set of values. But the reverse is not true. And in any case with a few exceptions (mostly basic types) it makes little sense to reason about the specific set of values.

A type is a characterization of an expression in a formal language (like programming language but not only, the languages of formal proofs may also have types). As such the set of values will correspond to the potential set of values that such a term can be evaluated to during the computation.

When you assign a type to an expression you basically prove that the expression is legal within the language.

For the engineering problems to be resolved such a set of values typically is associated with an algebraic structure of some kind, it might have an inner structure that is observable (record types), in other words it is something that the programmer will *construct* starting from primitive types and using the expression composition (and consequently type composition) rules defined in the type system specific to that language.

> I'm *hoping* what you mean is that a type is a specific kind of set
> with specific properties, but I'm afraid you mean something else
> entirely.
>
>

Well a type can definitely be a set if you define some semantics within some set theory for that particular language, otherwise a tyoe can be for example a categorical object in a particular category. Type theory holds that the SET category is not very well suited for constructing the semantics of a programming language.

>

>>In order to avoid this trap you have to ask yourself what is the purpose
>>for which you want to construct a type system.

>
>
> Good point.
>
>
>
>>It seems to me you are trying to do it the other way around, meaning to
>>approach from the platonistic ideals that there are some eternal truths
>>about mathematics that you'll want to discover. So you risk ending up in
>>the eternal all circles are ellipses problems.

>
>
> You don't like TTM's answer to this question, I take it.
>
>

No, it is not the relevant, representative, important question to ask or problem to resolve, in order to construct a useful type system. Questions like whether a particular ellipse has become a circle need not be addressed within the type system.

If you want to address it within the type system, the logical consequence is that your type system will suffer from very bad properties.

For example:

        undecidability - the programmer has described patrulaters, rhombus and rectangles, and now he defines squares as rectangles with orthogonal diagonals. Can the system decide that square is subtype of rhombus ?

        undefidedness - see above except the programmer doesn't define square as a type. But he defines a polymorphic function f for patrulaters let's say by the expression E1, he overrides f for the particular case of rhombus let's say expression E2 and overrides it again for rectangles, expression E3. Now at runtime f is invoked on a square object. What expression should be used to evaluate f for squares ?

So the bottom line is such issues are not expressible within a type system and you can't have the "perfect" type system to take care of them because of undecidability issues, halting problem and so on.

The right formalism for circle and ellipse can be as simple as

function (x: Ellipse)=

	if (x.a = x.b) then
		compute_the_Circle_Case (x)
	else
		compute_the_NonCircle_Case(x)

In trying to solve such unsolvable problems, D&D left lots of other important things unsolved.

>

>>You have to look the
>>other way around: you can construct any formal system you want as long
>>as it have the properties needed for you to solve problems. Types as you
>>defined them above (or even as Date defines them in TTM) are not
>>particularly useful, since they don't have certain desirable properties
>>while they have certain undesirable properties.

>
>
> Could you expand on what the desirable and undesirable properties are?
> I do intend to read the references you provided (although my previous
> experience with the "Naive type theory" paper was unsatisfactory.)
> But I'd also like to have the conversation here.
>
>

Well, the most important thing is to have a sound type system. The language should have well defined semantics and any expression that is type checked should have a clear evaluation mechanism, and the evaluation should not result in a type error at runtime.

That would be the basics.

Other than that the language and the type systems should help the programmers with the economy of expression at code write time and the economy of execution.(should allow extracting common patterns in higher order functions to avoid duplication, should allow for optimizations and efficient execution).

A very down to earth introduction to such things is "Bad enegineering properties of Object Oriented Languages" by Cardelli.

Oh, also economy of resoning is very important. If I have to scratch my head too hard to figure out the type of an expression, something might be fishy in there :)

>

>>The ultimate judgement on any formalism is how effective it is in
>>solving a particular problem or a class of problems. As such, trying to
>>attack the theory of types without having a problem in mind is not going
>>to bear fruits. So again, rather than thinking on "what types are " you
>>should be thinking on "what [my unspecified] types could be useful for".

>
>
> As an aside, what do you think of Haskell and type classes?
>
>

Haskell is a good example of a sophisticated type system. So is OCAML. They are also good examples of engineering trade-offs of balancing a delicate formalism to be effective, implementable and so on.

Still for most programmers in the industry any of these languages would be too hard to swallow.

>

>>You might also give it a try with introductory papers such as "type
>>systems" by Cardelli or Naive Type theory by Constable and of course the
>>wonderful book Types and Programming Languages.

>
>
> I'll read that first paper asap. Maybe buy the book, too, but it's $60-plus.
> Maybe I can get work to buy it.
>

Type theory is a very tough subject. Pierce's book is probably the best introduction. It's also very comprehensive and with plenty of hands-on code. Absolutely the best.

>
> Marshall
>
>
>

Costin Received on Sun Jul 06 2003 - 08:40:08 CEST

Original text of this message