axiom-developer
[Top][All Lists]
Advanced

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

Re: [Axiom-developer] Bootstrap documentation.


From: Ralf Hemmecke
Subject: Re: [Axiom-developer] Bootstrap documentation.
Date: Tue, 08 May 2007 16:47:56 +0200
User-agent: Thunderbird 2.0.0.0 (X11/20070326)

On 05/08/2007 03:49 PM, Gabriel Dos Reis wrote:
"Bill Page" <address@hidden> 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




reply via email to

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