Re: [Axiom-developer] "has" and "with" (was curious algebra failure)

[Bill Page]

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. I guess the question still is how? and why? does it work.

Regards,
Bill Page.