Re: Values have types ??

From: Alfredo Novoa <alfredo_at_ncs.es>
Date: 9 Sep 2003 15:15:49 -0700
Message-ID: <e4330f45.0309091415.3b45c54b@posting.google.com>

Costin Cozianu <c_cozianu_at_hotmail.com> wrote in message news:<bjgnju$h2b9n$1_at_ID-152540.news.uni-berlin.de>...

> No, actually {2} is the set with a single element 2.

Then {2} is not a type in the D&D model.

The MST of a value must be choosed among the defined types.

> 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

Agreed, but both parts of the books are independent.

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

Yes, but you have to define the type in some way.

> 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
I don't think it is acording to the syntax of page 261. The CONSTRAINT token is missing, and WHERE is not a boolean operator.

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

The type hierarchy is illegal because it is not a lattice. See chapter 15.

> So bottom line you have 2 options :
> - either the type system is inconsistent opening the possibility of
> runtime type errors

IMO the correct option is a compile time error.

> 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

Thanks for the references.

Regards
Alfredo Received on Tue Sep 09 2003 - 17:15:49 CDT