On 30 October 2016 at 19:14, Waldek Hebisch <[email protected]> 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.
--
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 [email protected].
To post to this group, send email to [email protected].
Visit this group at https://groups.google.com/group/fricas-devel.
For more options, visit https://groups.google.com/d/optout.
