Re: [Axiom-developer] RE: [Aldor-l] Type: Type

[Gabriel Dos Reis]

"Page, Bill" <address@hidden> writes:

| On Tuesday, August 29, 2006 6:03 AM Gabriel Dos Reis wrote:
| >>> At the logical level, as I have observed some time ago, there
| >>> is an inconsistency problem with Type:Type.  I'm wondering how
| >>> Aldor gets away with that.  Many languages (mostly functional)
| >>> use stratified types.
| 
| On Tue, Aug 29, 2006 at 12:42:04PM +0200, Ralf Hemmecke wrote:
| >> Can you construct a paradox that demonstrates the problem in
| >> terms of Aldor code? To me it looks like the class (not set)
| >> of all classes. Would there be a problem in class theory?
| 
| On Tuesday, August 29, 2006 8:52 AM Stephen Watt wrote:
| > 
| > You are correct that there is a potential inconsistency.
| > 
| > We avoid Russel's paradox by limiting the operations for
| > constructing and testing membership in type categories.
| > ...
| 
| I think the fact that Aldor defines the type of Type as Type
| is very interesting from a theoretical point of view and that
| it is not correct to suggest that it implies any inconsistency
| or even necessarily any fundamental limitation.

I believe I need more explanations than the vague allusion to
co-inductive formalism.  Epigram, for example, faces the same issue, and
I don't think it is just mirage:

   http://www.mail-archive.com/address@hidden/msg00038.html

-- Gaby