|
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
[Prev in Thread] | Current Thread | [Next in Thread] |