Re: [Axiom-developer] Bootstrap documentation.

[Gabriel Dos Reis]

On Tue, 8 May 2007, 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 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".

I'm not aware of a definition of "dependent types" that would
disallow the use of "L" above in the definition of Plus.

One of the reason I asked my question is that, I wanted to arrive at
the most "natural" way of expressing simple concepts (found in many
different programming languages today), that very simply written, and very
simply stated.  This is both necessary for teaching (I was writing up 
something about programming with Spad) and basis for improvement.

I'm looking for ways to express simple and elegantly simple notions.

-- Gaby