Re: [Axiom-developer] operations working in general, but not in special cases -- help needed

[Ralf Hemmecke]

Dear William,

I like most of what you have written, but I must oppose against a few 
things.

> > Example 1, Matroids
> >
> > A "matroid" is a mathematical structure with one very, very important
> > operation, namely "dualizing" which transforms a given matroid into
> > another. Thus, one is tempted to have a category "MatroidCat", which exports an
> > operation "dual: % -> %".
>
> I assume you want MatroidCat to be the category of all matroids, in which case,
> the dual operation is actually a domain constructor.  That is, the above
> signature cannot do what you are aiming for:
>
>     MatroidCat():Category == ... with
>       dual: % -> %
>
> because the % refers to a particular implementation of a domain which is a
> matroid, not the category itself.

Sorry, I have not yet read about Matroids, but in simple terms it is that
       dual: % -> %
transforms a concrete matroid M=(E, I) to M^D=(E, I^D) but doing this by 
assuming I^D = I (and thus M=M^D) which need of course not be the case).

So clearly that signiture is wrong.

> The argument to dual is an element of a
> matroid. A plausible signature is:
>
>       dual:() -> MatroidCat()
>
> which associates a matroid to the current matroid.

That sounds promising but here I must oppose. The reason is that the 
resulting dual domain will probably be not very useful.

[snip]

But let's analyse this...

>     MatroidCat(): Category == Finite with
>       underlyingSet: () -> Finite
>       underlyingFamily: () -> Set %
>       span: Set % -> Set %
>       defining?: % -> Boolean  -- true if set is in underlyingFamily()
>       independent?:  Set % -> Boolean
>       circuit?: Set % -> Boolean
>       ...
>       dualSet: () -> Set %  -- constructs I^D
>       dual: () -> MatroidCat() 
>       dual()==Matroid(underlyingSet(), dualSet())
>       ...

Clearly, that category is very much involved and cannot be compiled 
without knowing about the constructor Matroid(E, I). But it's not that 
what I find problematic. It is the appearance of MatroidCat within the 
"with" expression. What comes after the == depends on what comes before.
I cannot say, that I like this very much. Would you do something like 
that in (mathematical) category theory? The "with" expression alone is 
not a value until MatroidCat is known.

What else is bad is that the dual is always constructed by the domain 
constructor Matroid. You don't allow other implementations (other 
constructors).

> Alternatively, instead of using functions dual(), you can have a domain
> constructor:
>
>     DualSet(M:MatroidCat): Set Set underlyingSet M == ...
>       
>     Dual(M:MatroidCat):MatroidCat == 
>       E:= underlyingSet(M)
>       I:=underlyingFamily(M)
>       J:=DualSet(M)
>       Matroid(E, J)

Well, that demonstrates what I mean by "the resulting dual domain will 
probably be not very useful" above.

Suppose you create a very special matroid M which inherits from 
MatroidCat but additionally from many other categories. If you now say

N == Dual(M)

you will get something that is constructed by the constructor Matroid 
(which might actually not be that what you want -- remember there are 
also several implementations of polynomials and they are all good for 
something).

So the next idea would be something like

  Dual(M: MatroidCat, MAT: ??? -> MatroidCat): MatroidCat ==
    MAT(underlyingSet M, DualSet M);

Well, what can you do if you now say

N == Dual(M, MyMatroid)

? Actually not much, since that N is of type MatroidCat and nothing 
more. No additional features are available even if MyMatroid would 
return something of category MyMatroidCat that is much richer than 
MatroidCat itself.

With the above Dual constructor, you explicitly restrict the exports to 
MatroidCat. And I would have no other idea to add features than to use 
"pretend". Brrrrrhhh.

> A more practical implementation may have this outline:
>
>    MatroidCat(E:Finite, I:Set Set E): Category == Finite with
>      span: Set % -> Set %
>      independent?:  Set % -> Boolean
>      circuit?: Set % -> Boolean
>      ...
>
>
>    Matroid(E: SetCategory, I:Set Set E):MatroidCat(E,I) == ... with
>
>    DualSet(E:SetCategory, I:Set Set E):List List E == 
>
>    Dual(E:SetCategory, I:Set Set E):MatroidCat(E, DualSet(E,I)) == ...

I like that somehow much better, but the same "restriction process" as 
above takes place. Things are not so easy with a dual functor.

> If you do NOT want to implement dual as a domain constructor, then you may try
> implementing Matroid as the DOMAIN of all matroids. However, Axiom does not
> allow dependent types at the code level (only at the declaration level for
> constructors).
>
>    Matroid(): SetCategory == ...
>
>      Rep:= Record(E:SetCategory, I:Set Set E)
>
> probably won't work in Axiom, but Aldor may.

Did you really mean SetCategory? So to create a new element you would 
write a function.

  matroid(A: SetCategory, B: Set Set A): % == per [A, B];

and call it with

  matroid(Integer, [[1,2], [3,4,5]]);

That sounds to me as follows: If E' \supset E and I \subseteq Power(E) 
then the matroids (E, I) and (E', I) are the same. I cannot believe that.

Ralf