Ok, thanks. On Fri, Aug 19, 2011 at 6:08 PM, Gabriel Dos Reis <g...@cs.tamu.edu> wrote: > | > > | > )abbrev category MYAGG MyAggegate > | > MyAggegate(): Category == Type with > | > elementType: Ring -- to be defined by each domain > | > toList: % -> List elementType -- idem > | > sumAll: % -> elementType -- this one has a default implementation > | > add > | > sumAll x == reduce(_+,toList x,0$elementType) > | > > | > > | > This is just one simple example of (indirect) dependency. > | > Type dependency requires an advanced decision procedure of type equality > | > that goes beyond syntactic equally (which is the theoretical > | > underpinning of most of current Spad, ML, and Haskell98 type system.) > | > > | > Bill Page <bill.p...@newsynthesis.org> writes: > | If the associated type is "defined on case by case basis by each > | domain" we can make the dependency more explicit. Presumably we still > | want types to be static. Is there any situation where the following > | would not be adequate? > > The issue is not whether an associated type can be *encoded*. > > what you have done is to turn an implicit parameter (existentially > quantified) into an explicit parameter (universally quantified), and > ask each user to pass that around all the time, blurring the distinction > between what is essential parameter from what is derivable (associated > types). It becomes unbearable when the number of associated type > grows or there are redundancies.
Yes you are right. I see the point. > There are some examples of that in the existing AXIOM algebras -- > and the problem is well know (at least from discussions with > Stephen Watt.) > Yes, I recall such discussions. > This is a well known technique that has been around for a while. In fact, > it was the status quo in Haskell, until the survey [1] that prompted the > Haskell people to consider associated types, that later evolved into > type families. So, you are taking the opposite route of `improvements' > that we have seen so far :-) See discussions in the literature below. > > [1] http://dl.acm.org/citation.cfm?doid=949305.949317 > [2] http://dl.acm.org/citation.cfm?doid=1086365.1086397 > [3] http://dl.acm.org/citation.cfm?doid=1190315.1190324 > [4] > http://research.microsoft.com/en-us/um/people/simonpj/papers/assoc-types/fun-with-type-funs/typefun.pdf > Thanks for the references. > [...] > > | Note: I had some problems using reduce in this context. > > what was it? > Sorry, thinko. I just forgot the package call. The following compiles: )abbrev category MYAGG MyAggegate MyAggegate(ElementType: Ring): Category == Type with elementType: Ring -- to be defined by each domain toList: % -> List ElementType -- idem sumAll: % -> ElementType -- this one has a default implementation add elementType == ElementType sumAll x == reduce(_+,toList x,0)$ListFunctions2(ElementType,ElementType) -- Here is another example similar to yours except the dependency is only on a value instead of a type. This compiles: (in OpenAxiom): -- )abbrev category MYITUP MyIntegerTuple MyIntegerTuple(): Category == Type with elementSize: NonNegativeInteger -- to be defined by each domain toProd: % -> DirectProduct(elementSize,Integer) sumAll: % -> Integer -- this one has a default implementation add sumAll x == reduce(_+,entries toProd x,0)$ListFunctions2(Integer,Integer) -- (1) -> )co dep4a-gaby.spad Compiling OpenAxiom source code from file /home/page/dep4a-gaby.spad using Spad compiler. MYITUP abbreviates category MyIntegerTuple ... (1) -> )sh MYITUP MyIntegerTuple is a category constructor Abbreviation for MyIntegerTuple is MYITUP This constructor is exposed in this frame. Issue )edit /home/page/dep4a-gaby.spad to see algebra source code for MYITUP ------------------------------- Operations -------------------------------- elementSize : NonNegativeInteger sumAll : % -> Integer toProd : % -> DirectProduct(elementSize,Integer) However I was unable to find a way to compile a domain using this category. E.g. -- )abbrev domain MYITUPD MyIntegerTupleDomain MyIntegerTupleDomain():MyIntegerTuple with sample: () -> % coerce: % -> OutputForm == add Rep == DirectProduct(3,Integer) elementSize == 3 toProd(x) == rep x sample() == per directProduct( [1,2,3] ) coerce(x) == (entries rep x)::OutputForm -- (1) -> )co dep4b-gaby.spad Compiling OpenAxiom source code from file /home/page/dep4b-gaby.spad using Spad compiler. MYITUPD abbreviates domain MyIntegerTupleDomain ------------------------------------------------------------------------ initializing NRLIB MYITUPD for MyIntegerTupleDomain compiling into NRLIB MYITUPD Adding $ modemaps Adding Integer modemaps Adding NonNegativeInteger modemaps Adding PositiveInteger modemaps Adding Rep modemaps compiling exported elementSize : () -> NonNegativeInteger MYITUPD;elementSize;Nni;1 is replaced by 3 ;;; *** |MYITUPD;elementSize;Nni;1| REDEFINED Time: 0.02 SEC. Adding DirectProduct(elementSize,Integer) modemaps compiling exported toProd : % -> DirectProduct(elementSize,Integer) ****** comp fails at level 1 with expression: ****** error in function toProd ((|rep| |x|)) ****** level 1 ****** $x:= (rep x) $m:= (DirectProduct elementSize (Integer)) $f:= ((((|x| # #) (|#| # #) (* # # #) (** # # #) ...))) >> Apparent user error: Cannot coerce x of mode DirectProduct(3,Integer) to mode DirectProduct(elementSize,Integer) Regards, Bill Page. ------------------------------------------------------------------------------ Get a FREE DOWNLOAD! and learn more about uberSVN rich system, user administration capabilities and model configuration. Take the hassle out of deploying and managing Subversion and the tools developers use with it. http://p.sf.net/sfu/wandisco-d2d-2 _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
