RE: [Axiom-developer] Bootstrap documentation.

[Bill Page]

On May 8, 2007 10:48 AM Ralf Hemmecke wrote:
> 
> 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 called 'dependent types'"?
> 

Perhaps I should have said: "goes beyond what **I** would normally
call a dependent type". How other people classify this, I cannot
say. Now you might ask: How do I define dependent type? But I
prefer to punt (en Français "ponter") on that question for now.

> 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?

Yes, excellent. That is much better. Now L only appears explicity
in the body of the function. Is it equivalent to what Martin wrote?

> 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.ht
ml#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".
> 

Ok. Thanks.

Regards,
Bill Page.