[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] RE: [Aldor-l] Type: Type
From: |
Gabriel Dos Reis |
Subject: |
Re: [Axiom-developer] RE: [Aldor-l] Type: Type |
Date: |
30 Aug 2006 05:15:57 -0500 |
"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
[Axiom-developer] Re: Dimensions as types..., C Y, 2006/08/29
Re: [Axiom-developer] Re: Dimensions as types..., Martin Rubey, 2006/08/29