"Bill Page" <[EMAIL PROTECTED]> writes:
| On May 8, 2007 2:15 AM Martin Rubey wrote:
| >
| > Bill Page writes:
| >
| > > Gaby wrote:
| > > > Many of the categories and friends dragged in by Integer
| > > > do not seem to be of necessity at the lowest level. So,
| > > > you could start with just the simple data structure Integer
| > > > with few operations and extend it as you go.
| > >
| > > But for this to be sucessful for the entire Axiom library
| > > wouldn't that require that there be no essential mutual
| > > recursion between source modules? I do not see how extend
| > > helps in this case. Sure it is possible even to have
| > > mutual recursion between extensions, not?
| >
| > At least in Aldor you can have more or less arbitrary mutual
| > dependencies.
|
| So far as I understand it, Aldor can solve mutual dependencies
| only when they occur within the same source module.
For the majority of the cases where I need mutual recursion between
domains, that is sufficient.
| Some types
| of mutual dependencies between source modules (the trivial ones)
| can be handled by extend.
I'm not sure I would qualify those of "trivial".
[...]
| > 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'"?
-- Gaby
_______________________________________________
Axiom-developer mailing list
[email protected]
http://lists.nongnu.org/mailman/listinfo/axiom-developer
