Ralf Hemmecke <[EMAIL PROTECTED]> 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. _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer
