>
> On 06/17/2016 03:15 PM, Waldek Hebisch wrote:
> > Ralf Hemmecke wrote:
> >>
> >> First of all, I wouldn't ever have typed "List Type", because what
> >> exactly would that mean? As I understand "Type", it is a category, not a
> >> domain.
> >
> > Rember that types are values and categories are also types.
>
> OK, my sentence was not correctly formulated. Actually, I have nothing
> against creating a list consisting of BasicType and Integer (because
> both of them belong to Type (right?)). At least I would nothing have
> against a domain "List(with)" and "List(Category)" where the elements
> would be domains and categories, respectively.
I am not sure what "List(with)" is supposed to mean. Maybe you
want 'List(with())'? Anyway, unlike other types categories are
not first class in FriCAS, so "List(Category)" is suspect.
"with()" creates a category that does not usable alone.
>
> My actual criticism was about what die signature of "has" is in order to
> have no type conflict when instantiating (and thus executing) something
> like "BasicType has BasicType" in the creation of List(BasicType).
That is confusing thing. Logically "Field has Field" should give
false: there is no '+' on field, so clearly you can not apply
signatures from Field to types in the category of fields.
"BasicType has BasicType" is more subtle: in priciple we could
declare that all categories have BasicType: in practice operations
on types uses equality and this is only signature neccessary to
have BasicType (there is also '~=', but it has default implementation
in terms of '=').
Axiom implementation did different thing: when A was a category
it treated "A has B" as test if A is a subcategory of B.
I think that the following is most resonable description of
current state: FriCAS universe consists of ordinary (non-type)
values and types. Types divide into normal types, categories
and lone Category. Normal types and ordinary values are
first class: can be used in runtime computations. Categories
(and Category) can be used only in limited contexts, essentialy
only as constants. Normal types are logically disjoint, so
nomal value belongs to only one type. OTOH categories support
subtyping: given type belongs to many categories. In particular
Category is a subtype of Type: every category is a type.
So there is no contradiction in Category both being of
type Category and of type Type: Category is more precise
but Type is OK too. Given limitations on use of categories
their exact type does not matter very much. Of course
if you want to use "types as propositions" paradigm, then
"Type has Type" leads to contradiction, but it causes no
trouble for typechecking and there are tricks to cure it
at logical level.
--
Waldek Hebisch
--
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.
