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

[Stephen Watt]

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.

Note that many programming languages have the problem of
allowing types with no elements, which can lead to the type
theory equivalent of a division by zero error.

Aldor is no exception in this regard:  It is possible to construct
a domain with no effective way to make elements.  

These kinds of errors have to be seen as  bugs in programs, just as 
division by zero is a programming error and not an invalidation of
integer arithmetic.

-- Stephen
    

On Tue, Aug 29, 2006 at 12:42:04PM +0200, Ralf Hemmecke 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.
> 
> That question should be asked at aldor-l.
> 
> 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?
> 
> Ralf
> _______________________________________________
> Aldor-l mailing list
> address@hidden
> http://www.aldor.org/mailman/listinfo/aldor-l