[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

RE: [Axiom-developer] Bootstrap documentation.

From: Bill Page
Subject: RE: [Axiom-developer] Bootstrap documentation.
Date: Tue, 8 May 2007 09:31:59 -0400

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. Some types
of mutual dependencies between source modules (the trivial ones)
can be handled by extend.

> We use that (heavily) in the species project ("aldor-combinat").

Could you give an example?
> However, I don't think that the current Axiom algebra uses 
> it.

??? You don't think the Axiom algebra uses mutual recursion?
I would like to be shown that I am wrong, but I think that
it does, in fact that it is used extensively.

> 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" since L would appear to be
a free parameter of some kind. Isn't there a way to write
this that does not use such an exotic definition?

Bill Page.

reply via email to

[Prev in Thread] Current Thread [Next in Thread]