Re: [Axiom-developer] Bootstrap documentation.

[Gabriel Dos Reis]

"Bill Page" <address@hidden> 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