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

[Gabriel Dos Reis]

On Mon, 13 Aug 2007, Bill Page wrote:

| On 8/13/07, Gabriel Dos Reis wrote:
| > ...
| > When compiling the default definition of ** for Monad, the compiler
| > notices that expt comes from RepeatedSquare(S), where S is the
| > parameter of type Monad to Monad&.
| 
| This use of S is confusing to me.

OK, see the message I'll be sending out in a moment.

| The spad code says:
| 
|    import RepeatedSquaring(%)
| 
| The S that I see is the *formal* parameter of RepeatedSquaring. It's type is
| 
|     SetCategory with "*": (%, %) -> %
| 
| as defined in repsqr.spad. But in Monad the parameter % in
| 
|    import RepeatedSquaring(%)
| 
| refers to some domain (currently unknown) that has type Monad.

I see what you mean.  Let me cut-n-paste part of the other message I'm
composing 

   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)


| How can I reconcile that with your statements about S above? Is the
| "S" to which you refer some kind of dummy?

does the above help?


Are you confused by the uses of "x" in the below?

    f(x : Integer): Float == 
       cos(x)$Float

    
    g(x: Float): Float ==
      f(x :: Integer)



| > If compiles all arguments x and n fine.
| > Then it has to compile the package RepeatedSquare(S) -- as if it were
| > a function call, since all instantiations are function calls.  To achieve
| > that it asks the question whether S (of type Monad) is coercible to
| >
| >    SetCategory with "*": (%, %) -> %
| >
| > And the definition of coercible does not permit to return "yes".
| >
| 
| But certainly it must return "yes" in an unmodified version of the
| Spad compiler or (perhaps)  what needs to be coercible is not S of
| type Monad but rather the dummy %. It's type is the category-value of
| Monad:
| 
|   SetCategory with
|        "*": (%,%) -> %
|        rightPower: (%,PositiveInteger) -> %
|        leftPower: (%,PositiveInteger) -> %
|        "**": (%,PositiveInteger) -> %
| 
| which certainly is coercible to
| 
|    SetCategory with "*": (%, %) -> %
| 
| ----------
| 
| Is it possible to trace how coerce is called in an unmodified Spad
| compiler that compiles Monad without an error message?

Oh yes, one gets tons of s-expressions.  I already posted a snipped
of 4000+ line.  I can post more if you want, but not to the list.

-- Gaby