Bill Page <[email protected]> writes: | Thanks, Gaby. | | On Fri, Aug 19, 2011 at 4:26 PM, Gabriel Dos Reis <[email protected]> wrote: | > | > | >> Note also that Spad does not work properly with operations returning | > | >> types -- for very deep implementation reasons, one that the Haskell | > | >> people also faced when they added type families (i.e. type-level | > | >> functions, still not accepting values at that level) leading to redesign | > | >> of Haskell type rules and extension of its theoretical foundation. | > | > As an example of my statement: consider a situation where an entity has | > an associated type (say the element type of a container) that is defined | > on case by case basis by each domain. That associated type, in general, | > will be given by a type-level function which, because of the very nature | > of its purpose, should not be a constructor. | > | > )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.) | > | | 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. There are some examples of that in the existing AXIOM algebras -- and the problem is well know (at least from discussions with Stephen Watt.) 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 [...] | Note: I had some problems using reduce in this context. what was it? -- Gaby ------------------------------------------------------------------------------ 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 [email protected] https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
