On Mon, 13 Aug 2007, Bill Page wrote: | On 13 Aug 2007 00:39:45 -0500, Gabriel Dos Reis wrote: | > ... | > 2. When one defines a category with default implementation, like | > Monad, the compiler extracts the "purely categorial" part of | > Monad, e.g. the exports; then it implicitly creates a package | > Monad& with an implicit parameter S of type Monad. E.g., it is | > as if the code was written: | > | > )abbrev package MONAD- Monad& | > Monad&(S: Monad): Public == Private where | > Public ==> with | > "**" : (S, PositiveInteger) -> S | > | > Private ==> add | > import RepeatedSquare(S) | > x ** n == expt(x, n) | > | > | > Now the compiler goes on typecheking the defnition x ** n. | > It sees the use of expt() and find out that the only expt() in | > scope if the one from RepeatedSquare(S). Then it tries | > to instantiate that package -- just like a function call. | > From there, it applies the usual rules: Can I coerce S of | > type Monad to the expected argument type of RepeatedSquare()? | > They answer comes out as "no". Hence the error. | > | > Is that less confusing? | > | | Yes, thank you! But of course that is how packages and domains in Spad | are normally written and this package does in fact compile just fine | in Spad. See: | | http://wiki.axiom-developer.org/SandBoxMonad | | as it should. | | The question of coercing Monad to | | SetCategory with "*": (%, %) -> % | | must be yes.
A question is "why must it be `yes'"? | I guess the question still is how? and why? does it work. Indeed. -- Gaby _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer