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

[Gabriel Dos Reis]

"Bill Page" <address@hidden> writes:

| Gaby,
| 
| On 8/12/07, you wrote:
| > On Sun, 12 Aug 2007, William Sit wrote:
| >
| > | Isn't the problem whether 'Monad has SetCategory with
| > | "*":(%,%)->%' ? My answer would be yes. This should not be
| > | related to equivalence of categories or domains. We
| > | already have seen examples that Integer has with
| > | _*:(Integer, Integer)->Integer. Here, we are not saying
| > | 'Monad is SetCategory with "*":(%,%)->%'.
| >
| 
| Sorry for my confusion. In fact I agree with William. This is not
| directly related to type equivalence. We need something more general
| than type equivalence. We need to know when one category is a
| subcategory of another. The type equivalence rules to which Juergen
| referred must be applied to the parts of the category expressions in
| order to determine this relationship.
| 
| You wrote:
| 
| > > I'm saying that the parameter S of the default package
| > > Monad& -- generated for the default implementation of the
| > > category Monad -- is of the named category Monad.  It is
| > > that parameter S which is being used to instantiate
| > >RepeatedSquaring.  However, RepeatedSquaring expects its
| > >(domain) argument to be of the unnamed category
| > >
| > >    SetCategory with "*": (%,%) -> %
| 
| Your statement of the problem is a little confusing to me since the
| parameter S is the parameter of RepeatedSquaring. But as you say, it's
| type is given by the unnamed category above. You are concerned because
| what is being passed to RepeatedSquaring is a domain of type category
| named Monad. But clearly a domain of type Monad is also is a member of
| 
|    SetCategory with "*": (%,%) -> %
| 
| since Monad is a subcategory of this category - any domain that "has"
| Monad will necessarily provide all of the exports required by
| RepeatedSquaring. RepeatedSquaring requires it's (domain) argument to
| be of type that is a subcategory of this unnamed category.

A few obversations:

    1.  When a function is called, the compiler/interpreter determines
        whether the arguments used to call the function are coercible
        to the type of the formal parameters of the function, when it
        was declared.

       What that means concretely is that when we declare a function
       like

         foo: Double -> Double


       and we attempt foo(4), the compiler/interperter does not start
       looking whether the value 4 "has" sin, cos, and many operations 
       that hold for Doubles.  Rather, it determins whether the value
       4 can be converted the type Double, if yes, it applies that
       conversion and generate call to foo() with the result of the
       of the conversion as argument.

       That looks intuitive enough.  And I suspect we all agree.

   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?

-- Gaby