(thank you François!) Dear Gordon,
> > I am a Ph.D. student of Dr. Carette at McMaster University and I am working > > on the use of combinatorial species in type theory. I am not entirely sure what exactly you are up to. However, I'd be extremely happy to see somebody from the outside casting a look at our project. Our goal is to follow the theory as described in the book by Bergeron, Labelle & Leroux as closely as possible, while keeping things usable. And I must say that I'm quite astonished how far we got with relatively little code. As programming language we are using Aldor, in which types are first class objects, that is, a function can take a type as parameter, and can also return a type as value. For example, there actually is a function that (roughly) has the signature Fraction: IntegralDomain -> Field For example, Fraction(Integer) returns rational numbers while Fraction(Polynomial(Integer)) returns rational functions. Aldor also allows dependent types in great generality: f: (n: Integer) -> PrimeField n is a perfectly legal signature. Note that Aldor can be used as extension language of Axiom (I use the FriCAS fork, [EMAIL PROTECTED], axiom-wiki.newsynthesis.org), which makes our project available to a larger community. What concerns species, we decided to approach them as follows: a species is actually a function that takes a type of labels L, and returns a type which allows the operations and constants below. The "%" refers to the type itself, i.e., the species, and Generator is an Aldor type that provides iteration. Thus, in essence, we view a species as a function that can return a collection of structures given a set of labels. structures: SetSpecies L -> Generator % isomorphismTypes: SetSpecies L -> Generator % generatingSeries isomorphismTypeGeneratingSeries cycleIndexSeries So far we have implemented the most important constructions described by Bergeron, Labelle & Leroux: RestrictedSpecies, Plus, Times, Compose and FunctorialCompose, and some of the most important basic species, like CharacteristicSpecies, SetSpecies, Subset and Partition. (Of course, for functorial composition we cannot produce the isomorphism types - there is no known algorithm.) Currently we are working on the multisort extension. I have an algorithm to generate the isotypes of multisort compose, but I have not managed to implement it yet. (In the exposition above I cheat a tiny bit what concerns isotypes, but explaining it properly will take some time...) If you have any questions, do not hesitate to ask! Of course, now I'm curious what you are after...! Martin PS: to obtain the code, use svn co svn://svn.risc.uni-linz.ac.at/hemmecke/combinat/ combinat to read the documentation of the main development line, go to http://www.risc.uni-linz.ac.at/people/hemmecke/AldorCombinat/ ------------------------------------------------------------------------- This SF.net email is sponsored by: Microsoft Defy all challenges. Microsoft(R) Visual Studio 2008. http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/ _______________________________________________ Aldor-combinat-devel mailing list Aldor-combinat-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/aldor-combinat-devel
