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

[Gabriel Dos Reis]

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