RE: [Axiom-developer] Bootstrap documentation.

[Gabriel Dos Reis]

On Tue, 8 May 2007, Bill Page wrote:

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

I think this is a standard reference

  ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps

Look from page 82 onwards.

-- Gaby