[Axiom-math] Re: [fricas-devel] Re: iterators and cartesian product.

[Martin Rubey]

"Bill Page" <address@hidden> writes:

> It seems somewhat artificially imposed by Axiom's type hierarchy that does
> not easily allow domains to be members of domains. (Domains belong to
> categories, not other domains.).

Aldor does not have this problem at all.  As far as I remember, even axiom's
interpreter understands such constructions, if they are implemented in Aldor.

I.e., in Aldor, you can have

define CombinatorialSpecies(L: LabelType): Category == with {
        <<exports: CombinatorialSpecies>>
    default {
        <<defaults: CombinatorialSpecies>>
    }
}

CS == (L: LabelType) -> CombinatorialSpecies L;
CombinatorialSpeciesAlgebra: with {
        1: %;
        X: %;
        +: (%, %) -> %;
        coerce: CS -> %;
        coerce: % -> CS;
} == add {
        Rep == CS;
        coerce(cs: CS): % == per cs;
        coerce(x: %): CS == rep x;
        1: % == per EmptySetSpecies;
        X: % == per SingletonSpecies;
        (x: %) + (y: %): % == per Plus(rep x, rep y);
}

> In order to introduce '1..9' as a domain it would be possible to introduce
> new domain constructor like
> 
>    )abbrev domain INTS IntegerSegment
>    IntegerSegment(S:Segment Integer): with Finite ...
> 
> that takes something of 'Segment Integer' as a parameter. Do we want
> 'IntegerSegment' to also be a subdomain of Integer?. In any case, then we
> could write:
> 
>   DirectProduct(4,IntegerSegment 1..9)
> 
> But somehow the distinction between '1..9' and 'IntegerSegment 1..9'
> and '[a,b,c]' and 'OrderedVariableList [a,b,c]' seems artificial.

I think it's OK.

> It occurs to me that one might like at least the Axiom interpreter to perform
> some kind of automatic coercion from 'x' in a domain like 'Segment Integer'
> into the *category* consisting of domains 'IntegerSegment(x)'.

You could do this with dependent types:

coerce: (s: Segment Integer) -> IntegerSegment s;

This problem pops up in many many many places: look at the series operations:

    series(sin x, x=0)

we really would like to have something like (I substitute values for parameters
of the package for clarity)

    series: (EXPR INT, eq: EQ EXPR INT) -> UPXS(EXPR INT, lhs eq, rhs eq)

instead we have 

    series: (EXPR INT, eq: EQ EXPR INT) -> Any

I'd also like to have a retraction from Matrix to RectangularMatrix:

   retractIfCan: (m: Matrix INT) -> Union("failed", SquareMatrix(INT, nrows m)

instead, this retraction seems to be built into the interpreter, and cannot be
used in SPAD code.



Martin