Am 31.10.2016 um 02:42 schrieb Bill Page: > On 30 October 2016 at 19:14, Waldek Hebisch <hebi...@math.uni.wroc.pl> wrote: >> ... >> OTOH: >> >> (2) -> typeOf(Integer) >> >> (2) Type >> Type: Category >> (3) -> typeOf(typeOf(Integer)) >> >> (3) Category >> Type: Type >> (4) -> typeOf(typeOf(typeOf(Integer))) >> >> (4) Category >> Type: Type >> (5) -> typeOf(typeOf(typeOf(typeOf(Integer)))) >> >> (5) Category >> Type: Type >> >> So type operations can handle 'Category'... >> > > OK I can understand that the interpreter might not know the name > 'Category' but this still looks strange to me. Result (2) displays the > value 'Type', i.e. the top element of the category lattice and of > course this is a Category, so to be consistent with (2) shouldn't the > rest of the results at least be: > > (3) -> typeOf(typeOf(Integer)) > > (3) Category > Type: Category > (4) -> typeOf(typeOf(typeOf(Integer))) > > (4) Category > Type: Category > (5) -> typeOf(typeOf(typeOf(typeOf(Integer)))) > > (5) Category > Type: Category > > Yet it is odd to say that Category is a Category. If it is a Category > where is it in the lattice? > > OpenAxiom implements a different solution though I am not convinced it > is any better: > > (12) -> typeOf(-1) > (12) Integer > Type: Domain > (13) -> typeOf(typeOf(-1)) > (13) Domain > Type: Type > (14) -> typeOf(typeOf(typeOf(-1))) > (14) Type() > Type: Category > (15) -> typeOf(typeOf(typeOf(typeOf(-1)))) > (15) Category > Type: Type > (16) -> typeOf(typeOf(typeOf(typeOf(typeOf(-1))))) > (16) Type() > > It keeps the name 'Domain' which was at least partially implemented in > Axiom and defines the type of both 'Domain' and 'Category' to be > 'Type' but then we still have that 'Type' is a Category. > > In both cases there seems to be some confusion over the notion of type > and the notion of satisfying a category. >
According to the book (0.2.3) there is some logic: ... The type of every category is the distinguished symbol Category. I do interpret this as: Category is a terminal, i.e. has no type at all. Consequently typeOf(typeOf Type) should not give 'Category' as result. It's then an almost conceivable fact that Category is a Symbol whereas Type is not, unless quoted. -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To unsubscribe from this group and stop receiving emails from it, send an email to fricas-devel+unsubscr...@googlegroups.com. To post to this group, send email to fricas-devel@googlegroups.com. Visit this group at https://groups.google.com/group/fricas-devel. For more options, visit https://groups.google.com/d/optout.
