Ok, thanks. On Fri, Aug 19, 2011 at 6:08 PM, Gabriel Dos Reis <[email protected]> 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 <[email protected]> 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. -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To post to this group, send email to [email protected]. To unsubscribe from this group, send email to [email protected]. For more options, visit this group at http://groups.google.com/group/fricas-devel?hl=en.
