Darwin species calculator

[Martin Rubey]

(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, fricas-***@googlegroups.com,
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/

[Jacques Carette]

To follow-up on what Gordon mentioned, our aim is to thoroughly examine
the benefits one gets when replacing "inductive datatypes" as the
foundation for basic type constructors in functional languages with
Species instead.

The point being that Set and Cycle, as atomic species qua type
constructors, are not all that different from X. And while you already
have + and * over inductive types, other species operations are just as
valid, and again do not really 'complicate' things too much. All sorts
of operations for generic/polytypic programming keep working just as
before. Some of this has been done before (read: reinvented) under the
name of 'Containers' in the functional programming community. But their
Containers are really defined in a dual form of species, which I don't
happen to like as much, even though many similar results hold.

In other words, we are not so much interested as implementing Species as
with replacing inductive datatypes (ie polynomial Functors and their
least-first-points) with Species as the basic language.

One question: do you plan to implement operations akin to Maple's
combstruct, in particular random generation? That would be extremely
helpful for automated testing of program over combinatorial structures.

Jacques

PS: thanks for the subversion address, that will be very handy.

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

[Martin Rubey]

In other words, we are not so much interested as implementing Species as with
replacing inductive datatypes (ie polynomial Functors and their
least-first-points) with Species as the basic language.

I must admit that I do not know what an inductive datatype is...

One question: do you plan to implement operations akin to Maple's combstruct,
in particular random generation?

Although I would very much like to have that, I do not really know yet how to
go about it. Note that for ordinary species, i.e., functors from finite sets
to finite sets, you do not have any order on the "input set", nor on the
"output set", i.e., the set of structures. On the other hand, at least as far
as I know, random generation usually works via ranking and unranking
algorithms, which assume that at least the output set is ordered.

I'm not saying that it's impossible to fit this nicely into the species
framework, but I do not know how to do it yet. Input would be greatly
appreciated, of course.

To make things clearer: combstruct and MuPAD-Combinat really had "usability" as
primary goal. As one consequence, they do not implement species, but rather
"combinatorial classes", that is, collections of objects with a size function.

The main drawback of that method is that you cannot treat labelled and
unlabelled objects uniformly, there is no such concept as an isomorphism type,
which, in my opinion, is the main strength of (ordinary) species. In that
sense, combinatorial classes are very close to linear species. As a
consequence, their implementation of "unlabelled composition" does not give
what somebody used to species would expect. (WARNING: Compose in
aldor-combinat/trunk is also broken with respect to isomorphismtypes! You'd
have to use the iso-experiment branch instead...)

Martin


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

[Gordon J. Uszkay]

Thank you Martin, that is very interesting. I will need to spend some more
time reading your documentation and perhaps learn more about Aldor to really
understand what you're working on, but I think it sounds very interesting.
We are also interested in generating structures using species as type
constructors, and also what you called generators, but were more in the
Haskell mindset, looking at generalized folds for R-enriched trees, and then
even more generally constructing computations over species of structures
(extending the idea of a fold to a crush (over a set), a loop (over a
cycle), etc.

I will read a bit more, and get back to you, I'm sure we'll have a lot to
talk about!

Thanks,

Gordon

P.S.
Thank you Francois, this will be very helpful!

----- Original Message -----
From: "Martin Rubey" <***@univie.ac.at>
To: "Gordon J. Uszkay" <***@mcmaster.ca>; "aldor-combinat-devel"
<aldor-combinat-***@lists.sourceforge.net>
Cc: <***@uqam.ca>
Sent: Tuesday, February 05, 2008 4:52 PM
Subject: Re: Darwin species calculator


(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, fricas-***@googlegroups.com,
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/