Re: [Axiom-developer] "has" and "with"

[Gabriel Dos Reis]

On Thu, 16 Aug 2007, Ralf Hemmecke wrote:

| % as the argument of RepeatedSquaring stands for a domain of type Monad().
| Such a domain obviously satisfies
| 
|   SetCategory with {*: (%,%)->%}
| 
| since Monad() has these exports (and more in the Axiom library case).

Please be more precise about "satisfies".  What does it mean?

I understand what it means it terms of "has".

[...]

| Gaby, you have given in
| 
| http://lists.nongnu.org/archive/html/axiom-developer/2007-08/msg00412.html
| 
| how the "add" part in the Monad definition is translated to a private domain.

In fact, there is no nothing private about it.  The rewrite is available
to user.

| That looks perfectly fine to me.
| Bill has already shown that a proper value for the argument of
| RepeatedSquaring as in
| 
| http://wiki.axiom-developer.org/SandBoxMonad
| 
| works fine.
| 
| Gaby, you write there:
| 
|        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.
| 
| Why would the compiler want to "coerce" if all that is needed is to check
| whether S of type Monad has at least the exports that are required by the
| argument type of RepeatedSquaring. 

The compiler is doing that because it treats function calls -- either
to produce a value of a type -- uniformly.  It seems to me that you're 
arguing two non-uniform rules: one for value, and one for types.  Is that
correct? 

-- Gaby