[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 11:25:11 -0400 |
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.
- [Axiom-developer] Bootstrap documentation., Waldek Hebisch, 2007/05/07
- Re: [Axiom-developer] Bootstrap documentation., Martin Rubey, 2007/05/07
- RE: [Axiom-developer] Bootstrap documentation., Bill Page, 2007/05/07
- Re: [Axiom-developer] Bootstrap documentation., Gabriel Dos Reis, 2007/05/07
- RE: [Axiom-developer] Bootstrap documentation., Bill Page, 2007/05/07
- Re: [Axiom-developer] Bootstrap documentation., Martin Rubey, 2007/05/08
- RE: [Axiom-developer] Bootstrap documentation., Bill Page, 2007/05/08
- Re: [Axiom-developer] Bootstrap documentation., Gabriel Dos Reis, 2007/05/08
- Re: [Axiom-developer] Bootstrap documentation., Ralf Hemmecke, 2007/05/08
- Re: [Axiom-developer] Bootstrap documentation., Gabriel Dos Reis, 2007/05/08
- RE: [Axiom-developer] Bootstrap documentation.,
Bill Page <=
- Re: [Axiom-developer] Bootstrap documentation., Ralf Hemmecke, 2007/05/08
- RE: [Axiom-developer] Bootstrap documentation., Gabriel Dos Reis, 2007/05/08
- Re: [Axiom-developer] Bootstrap documentation., Gabriel Dos Reis, 2007/05/08
- Re: [Axiom-developer] Bootstrap documentation., Ralf Hemmecke, 2007/05/08
- Re: [Axiom-developer] Bootstrap documentation., Gabriel Dos Reis, 2007/05/08
- Re: [Axiom-developer] Bootstrap documentation., Ralf Hemmecke, 2007/05/08
- Re: [Axiom-developer] Bootstrap documentation., Gabriel Dos Reis, 2007/05/08