[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Axiom-developer] Axiom-Combinat / non-extending category
From: |
Martin Rubey |
Subject: |
[Axiom-developer] Axiom-Combinat / non-extending category |
Date: |
23 Oct 2006 17:55:38 +0200 |
User-agent: |
Gnus/5.09 (Gnus v5.9.0) Emacs/21.4 |
Dear Ralf, *
I now merged the modified signatures as outlined below with the axiom-port. The
result is quite promising.
I can use generatingSeries of all constructors, including Plus and Times.
I cannot use structures, of course, since this uses a dependent type now:
structures: (L: LabelType, List L) -> Generator %
The generator is not a problem, there is an easy workaround. However, the
dependent type is a show stopper, I'm afraid.
I'm willing to pay 200$ from my own pocket if somebody makes Axiom understand
signatures like that.
Furthermore, I tried to define a domain
)abb dom TEST Test
A: CombinatorialSpecies == Plus(CharacteristicSpecies(1),
CharacteristicSpecies(1))
in various forms, but all I get is the error message
non extending category
Well, I guess that's not so interesting anyway. We can use the aldor compiler,
after all.
I rather like the new signature.
Martin
Martin Rubey <address@hidden> writes:
> A short report:
>
> I modified species.as.nw, replacing CombinatorialSpecies L by
> CombinatorialSpecies, adding the LabelType in the representation of
> CharacteristicSpecies.
>
> (I didn't bother to modify the other basic species yet)
>
> The operation elements$LabelType is not needed in this approach, and in fact,
> I
> wouldn't know how to implement it.
>
> Extending Set is not possible, for reasons discussed recently on this list. We
> would need to create a new domain SetSpecies.
>
> Plus and Times stay nearly the same, only the signature changes to
>
> Plus(F: CombinatorialSpecies,G: CombinatorialSpecies): CombinatorialSpecies
>
> and F L has to be replaced by F everywhere, structures(List L) changes to
> structures(L: LabelType, List L), etc.
>
> Note that the Rep of Plus, Times, etc. won't change.
>
> Things seem to work. I'll have a look whether Axiom likes this version better.
>
>
>
> Martin
- [Axiom-developer] Axiom-Combinat / non-extending category,
Martin Rubey <=