|
|
last edited 16 years ago by Bill Page |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 | ||
Editor: hemmecke
Time: 2008/07/08 02:51:56 GMT-7 |
||
Note: |
changed: - A **category** is a type whose type is the language-defined constant Category. - - A **domain** is a type whose type is a category. - - A **type** is either a category, a domain or the language-defined constants Category and Type. - - Any **type** is of type Type. A **category** is an L-type whose type is the language-defined constant 'Category'. A **domain** is an L-type whose type is a category. An **L-type** is either a category, a domain or the language-defined constants 'Category' and 'Type'. Any L-type is of type 'Type'. I wrote **L-type** to mean *type in the language*, either Aldor or SPAD.
There seems to be different understandings of Type, domain, category, Category, etc. around. Here is an attempt to collect all these different opinions in order to make discussion about them clearer.
A category is an L-type whose type is the language-defined constant Category
.
A domain is an L-type whose type is a category.
An L-type is either a category, a domain or the language-defined constants Category
and Type
.
Any L-type is of type Type
.
I wrote L-type to mean type in the language, either Aldor or SPAD.