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

"Costin Cozianu" <c_cozianu_at_hotmail.com> wrote in message news:be7p79$25miq$1_at_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.)

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.

> 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.

> 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.

> 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?

> 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.

Marshall Received on Sun Jul 06 2003 - 07:23:32 CEST