On 05/08/2007 03:49 PM, Gabriel Dos Reis wrote:
"Bill Page" <[EMAIL PROTECTED]> writes:
| > In any case, "extend" would make life a lot easier, although
| > my top priority still is to make types first class objects
| > and to allow domain constructors like
| >
| > SPECIES ==> (L: LabelType) -> CombinatorialSpecies L;
| >
| > Plus(
| > F: SPECIES,
| > G: SPECIES
| > )(L: LabelType): CombinatorialSpecies(L) == add {
| > Rep == Union(left: F L, right: G L);
| > import from Rep;
| > <<implementation: Plus>>
| > }
| >
|
| I don't understand this construction. What is the signature
| of the function 'Plus'? I think this goes beyond what would
| normally call "dependent types"
Huh? What is "normally calle 'dependent types'"?
Bill, yes, the L looks like being a parameter. Let me try another
definition.
Plus1(
F: SPECIES,
G: SPECIES
): SPECIES == (L: LabelType): CombinatorialSpecies(L) +-> add {
Rep == Union(left: F L, right: G L);
import from Rep;
<<implementation: Plus>>
}
So
Plus: (SPECIES, SPECIES) -> SPECIES
as an addition of species.
Does that look simpler? Of course you can go on and define something like
Plus2: (F: SPECIES, G: SPECIES) -> ... ==
(F: SPECIES, G: SPECIES): ... +-> ((L: LabelType): ... +-> ...)
But that is probably not what you meant.
Yes, CombinatorialSpecies is itself a function.
http://www.risc.uni-linz.ac.at/people/hemmecke/AldorCombinat/combinatsu16.html#dt:CombinatorialSpecies
CombinatorialSpecies: (L: LabelType) -> Category
The following does (of course) not work.
Plus3(
F: SPECIES,
G: SPECIES
): CombinatorialSpecies ==
(L: LabelType): CombinatorialSpecies(L) +-> add {
Rep == Union(left: F L, right: G L);
import from Rep;
<<implementation: Plus>>
}
And I somehow need the L, because it is used inside the "add".
Ralf
_______________________________________________
Axiom-developer mailing list
[email protected]
http://lists.nongnu.org/mailman/listinfo/axiom-developer
