First class categories

[Waldek Hebisch]

Peter Broadbery wrote:
>
> Not sure about the last two; the second argument of "has" should
> really be a category, as having any type on the right would allow
> things like "X has Float", which ought to be an error.
> Effectively in aldor, "has" is of type "(Type, Category) -> Boolean".
>
> This still allows things like "Ring has SetCategory", at least in theory.
>
> > So it seems that has should be defined for categories and
> > return appropiate values (corresponding to operations that
> > one can do on types), like
> >
> > Group has Group ---> false
> > Group has Category ---> true
> > Group has Type ---> true

IIUC both Category and Type are categories, so in principle are
OK for second argument to 'has'. Float definitely is not a
category...

BTW, hypoterical code:

my_has(A : Type, B : Type) : Boolean ==
B has Category => A has B
A is B

BTW2: If one wants to compute with categories than probably
beside 'has' one need another predicate, say
extends : (Category, Category) -> Boolean
which return true when first argument is an extention of
the second one. At first glance one may confuse it with
'has' but it works at different level.

--
Waldek Hebisch

[Peter Broadbery]

On 2 February 2017 at 20:13, Waldek Hebisch <heb...@math.uni.wroc.pl> wrote:

Peter Broadbery wrote:
>
> Not sure about the last two; the second argument of "has" should
> really be a category, as having any type on the right would allow
> things like "X has Float", which ought to be an error.
> Effectively in aldor, "has" is of type "(Type, Category) -> Boolean".
>
> This still allows things like "Ring has SetCategory", at least in theory.
>
> > So it seems that has should be defined for categories and
> > return appropiate values (corresponding to operations that
> > one can do on types), like
> >
> > Group has Group ---> false
> > Group has Category ---> true
> > Group has Type ---> true

IIUC both Category and Type are categories, so in principle are
OK for second argument to 'has'.  Float definitely is not a
category...

I guess this is a place where axiom & aldor differ; in aldor, type and category are not of type category. Instead, all types are subtypes of "Type".  categories are special subtypes whose instances are domains with specific exports & "Category" is the type of all of these.  (this might be slightly incorrect, as it's a long time since I've really looked in detail at this - the aldor user guide is clearer). 

 

BTW, hypoterical code:

my_has(A : Type, B : Type) : Boolean ==
    B has Category => A has B
    A is B

 

BTW2: If one wants to compute with categories than probably
beside 'has' one need another predicate, say
  extends : (Category, Category) -> Boolean
which return true when first argument is an extention of
the second one.  At first glance one may confuse it with
'has' but it works at different level.

Agreed it would make sense.. I guess the other operations would be "get: (D: with, name: String, T: Type) -> T" which would return the export "name: T" from D, and something to retrieve all exports.

 

--
                              Waldek Hebisch

--
You received this message because you are subscribed to the Google Groups "aldor-devel" group.
To unsubscribe from this group and stop receiving emails from it, send an email to aldor-devel+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.