[Axiom-developer] RE: FW: data structure vs. mathematical structure

[Page, Bill]

Ralf Hemmecke <address@hidden> writes:
> 
> [...]
> 
> | ++ A set over a domain D models the usual mathematical notion of
> | ++ a finite set of elements from D.
> | 
> | Although
> | 
> | i: Integer
> | 
> | and
> | 
> | s: FinitePowerSet T
> | 
> | would be in perfect analogy if one read ":" as "element of", then
> | to go on "l: List T" would mean "List" is the container of all
> | finite sequences (with some information about their representation
> | (linked list)).

On Tuesday, November 14, 2006 8:30 PM Gaby wrote:
>  
> And that would match the usual definition of List as the least fixed
> point of the functor
> 
>      X |-> 1 + X
> 
> in CPO.

In case anyone is wondering what Gaby is talking about, I think the
following paper by Dos Reis and Jarvi:

  What is Generic Programming?
  Library-Centric Software Design LCSD'05

http://lcsd05.cs.tamu.edu/papers/dos_reis_et_al.pdf

provides a good introduction. It defines a List as the least fixed
point of

      X |-> 1 + T x X

Hopefully a future paper will deal more specifically with Axiom. :-)

In Axiom List could be defined something like this

  List(T:Type):ListAggregate == add
    Rep == Union(nil,Record(first:T,rest:%))
    ...

(perhaps it is in Aldor?) but in fact the actual definition refers
directly to the underlying Lisp architecture.

There is also a recent paper by Pablo Nogueira
http://www.cs.nott.ac.uk/~pni

  When is an Abstract Data Type a Functor? (31 Oct 06)
  7th Symposium on Trends in Functional Programming (TFP'06)

http://www.cs.nott.ac.uk/~pni/Papers/adt-functors.pdf

It contains a lot of references to Haskell and some category theory
but most of what it says about ADTs can also be applied to Axiom.

See also

http://www.cs.nott.ac.uk/~pni/Papers/index.html

> 
> However, the existence of 1.. in Axiom would suggest that actually
> some people think of List as the greatest fixed point.
> 

I don't think so.

In Axiom 1.. is called a UniversalSegment or a "Segment which may
be half open". Open segments can be expanded as Streams.

(1) -> expand(1..)

   (1)  [1,2,3,4,5,6,7,8,9,10,...]
                                             Type: Stream Integer

Formally Streams are defined as the greatest fixed point of the
functor

   X |-> T x X

Streams are like Lists but can be infinite. Axiom has both lists and
streams. E.g.

(2) -> generate(x+->nextItem(x),0)$Stream(INT)

   (2)  [0,1,- 1,2,- 2,3,- 3,4,- 4,5,...]
                                             Type: Stream Integer

Regards,
Bill Page.